[$lambda$-calcolo] Combinatore di Punto Fisso

[hamming_burst]

Propongo un piccolo esercizio di Informatica Teorica (Lambda-calcolo)

Teorema:

$EETheta\ lambda$-espressione$\ ,\ AAg\ $variabile qualunque

con:

$Theta -= (lambdaomegaf.f(omega\ omega\ f))\ (lambdaomegaf.f(omega\ omega\ f))$

definito come il combinatore di Punto Fisso (di Turing).

allora: [size=125]$Thetag -=_{beta}\ g(Thetag)$[/size]


1. dimostrare l'uguaglianza.

c'è un piccolo trucco per dimostrare che sono componenti di una equivalenza ($beta$-uguaglianza), ed è questa la cosa interessante.
Basta conoscere l'applicazione della $beta$-riduzione (o la sola sostituzione con qualche accorgimento) e le strategie di riduzione. Il resto viene da se.


2. il combinatore di Punto Fisso riportato sopra può essere espresso con altre $lambda$-espressioni, perciò non è unico.
Un altro esempio é quello proposto da Curry:

Y $-= lambdaf.((lambdax.f(x\ x))\ (lambdax.f(x\ x)))$ (con $lambda$-termini chiusi)

dimostrare che anche questa espressione gode della proprietà di Punto Fisso.


Se volete provare

[hamming_burst]

1.

Teorema:

$EETheta\ lambda$-espressione$\ ,\ AAg\ $variabile qualunque

con:

$Theta -= (lambdaomegaf.f(omega\ omega\ f))\ (lambdaomegaf.f(omega\ omega\ f))$

definito come il combinatore di Punto Fisso (di Turing).

allora: [size=125]$Thetag -=_{beta}\ g(Thetag)$[/size]

Proof:

\[\Theta\ g = ((\lambda\omega.\lambda f.f\ (\omega \omega\ f))\ (\lambda\omega.\lambda f.f\ (\omega \omega\ f)))\ g \]
\[\sideset{^\beta}{^1}\downarrow\]
\[(\lambda f.f\ ((\lambda\omega.\lambda f.f\ (w\ w\ f))\ (\lambda\omega.\lambda f.f\ (w\ w\ f))\ f))\ g = (\lambda f.f\ (\Theta\ f))\ g\]
\[\sideset{^\beta}{^2}\downarrow\]
\[g\ ((\lambda\omega.\lambda f.f\ (\omega \omega\ f))\ (\lambda\omega.\lambda f.f\ (\omega \omega\ f))\ g) = g\ (\Theta\ g)\]
\[\sideset{^\beta}{^3}\downarrow\]
\[\text{non-term}\]

abbiamo un loop infinito. Ma possiamo notare una riduzione familiare al $2-\beta-$step: la nostra equivalenza. Come facciamo a dimostrare effettivamente i due lati dell'uguaglianza? il lato sinistro lo abbiamo prodotto e si nota una forma familiare, proviamo con il lato destro e vedere se effettivamente è vero che applicando la funzione ritorna l'uguaglianza:

\[\text{non-term}\]
\[\sideset{_\beta}{_2}\uparrow\]
\[(\lambda f.f\ ((\lambda\omega.\lambda f.f\ (w\ w\ f))\ (\lambda\omega.\lambda f.f\ (w\ w\ f))\ f))\ g = (\lambda f.f\ (\Theta\ f))\ g\]
\[\sideset{_\beta}{_1}\uparrow\]
\[g\ (((\lambda\omega.\lambda f.f\ (\omega \omega\ f))\ (\lambda\omega.\lambda f.f\ (\omega \omega\ f)))\ g) = g\ (\Theta\ g)\]


Perciò:
\(\Theta\ g = ((\lambda\omega.\lambda f.f\ (\omega \omega\ f))\ (\lambda\omega.\lambda f.f\ (\omega \omega\ f)))\ g =\)
\(\lambda f.f\ ((\lambda\omega.\lambda f.f\ (w\ w\ f))\ (\lambda\omega.\lambda f.f\ (w\ w\ f))\ f))\ g = (\lambda f.f\ (\Theta\ f))\ g = g\ (\Theta\ g)\)

C.V.D.

NOTA:
la forma del combinatore di Turing si dice fortemente normalizzabile, è derivata dal fatto sopra, cioè che si riduce sempre nella $\beta$-uguaglianza. Altre forme sono più deboli come quella di Curry, dal fatto che dipendono dalle astrazioni o applicazioni in gioco.

Lascio il 2. a chi vuole risolverlo, la dimostrazione è simile.