Fondamenti di Informatica, 19 Settembre 2013

Non e' ammesso l'uso di alcun testo, appunti, calcolatrici, telefonini o smartphone. 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, comunicarlo immediatamente al docente o all'assistente in aula ed indicarlo chiaramente sull'elaborato che si consegna.

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

Esercizio 1
(a) Cos'e' un modello computazionale? Definire il modello computazionale delle URM.

(b) Scrivere un programma URM che calcoli il massimo di due numeri forniti in input.
Commentare il codice.

(c) I termini

(λxxxx.xx)(λx.xx)(λx.x)y((λx.x)x)

(λb.λa.λc.λd.λx.xx)(λx.xx)(λx.x)z((λw.w)x)

possono essere considerati identici? Giustificare la risposta.

Esercizio 2
(a) Enunciare e dimostrare il Teorema di Deduzione di Herbrand.

(b) Nella logica dei predicati del primo ordine (calcolo dei predicati), si specifichi una segnatura Σ, una struttura A_Σ e le due formule ben formate vere in A_Σ, corrispondenti alle due seguenti affermazioni:

Il quadrato di un numero naturale maggiore di due è maggiore del suo doppio
Alcuni parenti di Carlo sono anche parenti di Bruno, ma non di Alberto

(c) Quella che segue e' una dimostrazione incompleta, in logica proposizionale (calcolo proposizionale), di P, che utilizza l'ipotesi ¬¬P ed il teorema, che supponiamo gia' dimostrato, ¬P→¬P.
Ricopiare e completare tale dimostrazione.

1. .............             (Ak)
2. .............             ipotesi
3. .............             MP(1,2)
4. .............             (A¬)
5. .............             MP(3,4)
6. ¬P→¬P                     teorema
7. .............             MP(5,6)

Ricordiamo che gli assiomi (Ak) e (A¬)sono:
(Ak) α → (β→α)
(A¬) (¬β →¬α)→((¬β →α) →β)

Esercizio 3
Per la Logica di Hoare, definire la nozioni di: Asserzione, Giudizio, Stato, Soddisfazione di un giudizio in uno stato, Validita' di un giudizio.
Definire la nozione di giudizio e validita' anche per la semantica operazionale strutturata.