(\x.z\z.y\y.xyz) [zy/x,xz/y]
(b)
Dimostrare la consistenza (consistency) della teoria della beta-conversione
come corollario del teorema di Church-Rosser.
(c)
Fornire la definizione di funzione lambda-definibile.
Dimostrare che la funzione successore sui numeri naturali e' lambda-definibile.
Esercizio 2
(a)
Si consideri la seguente funzione definita per ricorsione:
f(n) = f(n+1)+1 se 0 <= n < 100
f(n) = n altrimenti
Scrivere una funzione Scheme freak che calcoli f,
e si dimostri formalmente, per induzione ben
fondata, che
(freak n) = 100 + |100 - n|
(b)
Una lista gallega e' una lista di numeri in cui tutti i numeri pari sono
messi in ordine decrescente, mentre i dispari sono in ordine crescente.
Es. (8 5 9 6 13 2) e' gallega, mentre (8 5 3 6 13 2) e (8 5 9 10 13 2) non lo sono.
Scrivere una funzione SCHEME, gaita, che, preso un numero n ed una lista gallega ls,
``inserisca'' n in ls nella posizione che sia piu' a sinistra possibile, ma tale che
la lista ottenuta risulti ancora gallega.
Es. (gaita 7 (8 5 6 2) ) --> (8 5 7 6 2)
(gaita 4 (8 5 6 2 9 15) ) --> (8 5 6 4 2 9 15)
Esercizio 3
(a)
Le seguente definizioni HASKELL
f n = n:(f(n+1))
nums = f 0
corrispondono, in SCHEME, a
(define (f n) (cons n (f (+ n 1))))
(define nums (f 0))
Che cosa "dovrebbe" fare f? e cosa e' nums?
Perche' in Haskell possiamo utilizzare f e nums (fornire possibilmente
un esempio di uso), mentre in SCHEME non ci possiamo fare in pratica niente?
Perche' comunque, anche se poi non ci possiamo fare un fico secco, SCHEME permette
lo stesso di definire la funzione f senza darci segnali di errore?
(b)
Mostrare la situazione dei frame al termine della valutazione della
seguente espressione Scheme.
(let ((a (lambda (x) x)))
(let ((b a))
((b a) 1) ) )