Alcune note sul lambda-calcolo

 Rappresentabilita' di funzioni definite ricorsivamente

Abbiamo visto come sia possibile definire nel lambda-calcolo funzioni come la somma ed il prodotto sui numeri naturali.
Nelle note [PS] e' descritto anche come rappresentare i booleani e operatori su di essi. Possiamo rappresentare nel lambda calcolo anche il predicato di uguaglianza tra numeri.
Insomma, nel lambda-calcolo possiamo rappresentare qualsiasi funzione che sia calcolabile tramite un algoritmo (Tesi di Church).

Questo pero' potrebbe risultare non cosi' semplice quando consideriamo funzioni, come il fattoriale, che sono definite tramite un algoritmo ricorsivo.

L'algoritmo per il calcolo del fattoriale sappiamo che si puo' descrivere tramite il seguente programma funzionale:

fact n = if (n=0) then 1 else n*fact(n-1)

Come si puo' rappresentare la funzione fattoriale nel lambda calcolo?
Dalle note [PS] sappiamo che if_then_else si puo' rappresentare, come anche il predicato di uguaglianza, i numeri, il prodotto e la funzione predecessore.
Quindi il fattoriale si dovrebbe rappresentare con il seguente lambda-termine:

\n.if_then_else (iszero n 0) 1 (mult n (fact(pred n)))

Dove pero' al posto di fact dovremmo inserire un lambda-termine!! Quale? Quello stesso che abbiamo costruito! Pero' anche questo conterra' fact, e quindi il procedimento non terminerebbe mai!!
Sembra una strada senza via di uscita...
In realta' esistono dei lambda termini che rappresentano la nozione stessa di ricorsione e che permettono di superare il problema. Si chiamano Operatori di Punto Fisso. Nelle note [PS], per chi fosse interessato, ne e' discritto uno: l'operatore di Turing. Oltre a quello di Turing, ne esistono molti altri, come quello che viene comunemente chiamato Y.
Utilizzando tali operatori si possono rappresentare funzioni definite ricorsivamente. Il fattoriale verrebbe infatti rappresentato dal lambda-termine

Y(\f.\n.if_then_else (iszero n 0) 1 (mult n (f(predn)))

Nel nostro corso non dimostreremo il perche' (gli interessati lo possono studiare nelle note [PS]).
Intuitivamente e' come se dicessimo: nel termine che applichiamo ad Y la ricorsione si fa su f

 Teorema di Church-Rosser e unicita' delle forme normali

Teorema di Church Rosser
Se un termine M si riduce in zero o piu' passi ad un termine P, e si riduce in zero o piu' passi anche ad un termine Q, allora esiste un termine R a cui si riducono in zero o piu' passi sia P che Q.
Formalmente: per ogni M, P e Q tali che M -->>_beta P e M -->>_beta Q, esiste un termine R tale che P -->>_beta R e Q -->>_beta R

Una immediata conseguenza di questo teorema e' il seguente

Corollario
Se un termine ha una forma normale, questa e' unica.

Dimostrazione
Supponiamo, per assurdo, che esista un termine M che abbia due forme normali. Tale cioe' che esistano due termini in forma normale N₁ e N₂ tali che M -->>_beta N₁ e M -->>_beta N₂.
Per il Teorema di Church Rosser deve allora esistere un termine R tale che N₁ -->>_beta R e N₂ -->>_beta R. Siccome pero' N₁ e N₂ sono in forma normale, se N₁ -->>_beta R deve necessariamente essere che arrivo ad R partendo da N₁ con zero passi di riduzione, cioe' R e' identico a N₁! Lo stesso discorso per N₂ -->>_beta R. Questo significa che N₁ e N₂ sono termini identici, e quindi non e' vero che M possa avere due forme normali distinte.


Il teorema di Church-Rosser puo' essere formulato in modo equivalente nel seguente modo:

Se M =_beta N allora esiste R tale che M -->>_beta R e N -->>_beta R


Da questa versione del teorema di Church-Rosser segue immediatamente che la teoria della beta-equivalenza e' consistente (una teoria e' l'insieme di tutti i giudizi derivabili).
Infatti, se prendiamo i lambda termini x e \y.y, per esempio, non e' vero che x =_beta \y.y e' un giudizio valido, altrimenti dovrebbe esistere un termine R tale che x -->>_beta R e \y.y -->>_beta R, ma questo e' impossibile.

Senza utilizzare il teorema di di Church-Rosser non sarebbe affatto semplice dimostrare la consistenza della teoria della beta-equivalenza.