Fondamenti di Informatica, 4 Ottobre 2012

Non e' ammesso l'uso di alcun testo, appunti o calcolatrici. Le risposte vanno scritte nel foglio di bella copia. Si raccomanda la massima SINTETICITA'. L'eccessiva verbosita' verra' considerata negativamente.
Occorre essersi prenotati sul portale studenti del nostro ateneo. Se cio' non e' stato fatto, comunicatelo immediatamente al docente o all'assistente in aula.

I risultati verranno indicati nella pagina web del corso. Date ed orari degli orali, sul Forum.

Esercizio 1
(a) Cos'e' un sistema formale? Quando un sistema formale si dice Consistente? Quando un insieme di formule ben formate di un sistema formale e' una Teoria? Cos'e' la Teoria pura di un sistema formale? Una teoria pura e' una teoria? Perche'?

(b) Nella seguente deduzione per ¬α → α |-_P₀ α scrivere cosa va inserito al posto di '??' e correggere i due errori presenti, giustificando le correzioni fatte.

1.  (¬α → ¬α) → ((¬α → α) → α)         A¬
2.   ¬α → ¬α                           Proposizione 3.1
3.  (¬α → α) → α                       ??
4.   ¬α → α                            ipotesi
5.   ¬α                                ipotesi

Dimostrare ¬α → α |- α anche nel sistema di deduzione naturale.

(c) Dimostrare il teorema di deduzione di Herbrand per la logica proposizionale alla Hilbert.
Ricordiamo che gli assiomi per la logica proposizionale sono:

α → (β → α)
α → (β → γ) → ((α → β) → (α → γ))
(¬ β → ¬ α) → ((¬ β → α) → β)

Esercizio 2
(a) Definire informalmente e formalmente la nozione di α-conversione nel λ-calcolo.
(b) Eseguire le seguenti sostituzioni, descrivendo brevemente il processo seguito.

x(λyx.x)[(yz)/x]
x(λyx.zx) [(λy.y)/x, x/z]

(c) Enunciare il Teorema di Church-Rosser per il λ-calcolo e dimostrare che se un termine ha forma normale questa e' unica.

Esercizio 3
Dimostrare che nella codifica in complemento a due dei numeri interi la rappresentazione dei numeri positivi ha "0" come cifra piu' a sinistra, mentre quella dei numeri negativi "1".