Niente appunti o calcolatrici.
Massima SINTETICITA' nelle risposte.
Esercizio 1
(a)
Dato un lambda-termine M, l'insieme { N | esiste P. M => P e P => N }
e' ricorsivo?
la relazione =>
e' la beta-riduzione parallela usata nella dimostrazione del teorema di Confluenza.
Giustificare la risposta.
(b)
Qual e' il risultato delle seguenti sostituzioni?
- \y.x(\x.x)[\y.yx/x]
- y(\z.xz)[\yzy.x/x]
- \y.y(\z.xz)[(\z.y)/y]
(c)
Dimostrare il teorema di unicita' della (eventuale) forma normale di un termine.
Esercizio 2
(a)
Definire in SCHEME il tipo di dato astratto Stack (nella sua versione puramente funzionale).
Definire una funzione SCHEME "perepe" che utilizza tale tipo di dato:
"perepe" prende in input uno Stack e che restituisce lo Stack invertito.
Esempio informale:
| 1 | | 3 |
| 7 | | 7 |
(perepe | 3 | ) ---> | 1 |
----- -----
N.B. NON utilizzare ricorsione di coda.
(b)
Si consideri la seguente funzione F sui numeri interi
F 0 = 0
F x = if x > 0 then 1 + F (1-x) else 1 + F (-1-x)
Che cosa calcola F?
Dimostrarlo formalmente.
Esercizio 3
(a)
Definire in Haskell il tipo di dato Albero ternario etichettato.
Discutere brevemente la soluzione proposta.
(b)
Vogliamo introdurre nello SCHEME un nuovo tipo di espressioni:
(paperoga e1 e2)
La semantica di una paperoga-espressione e' equivalente
a quella di (if e1 e2 5).
Scrivere una o piu' regola nello stile della Semantica Operazionale Strutturata
che descrivano formalmente la semantica di una paperoga-espressione.