Lambda Calcolo 101

Vedere Assolutamente: https://www.youtube.com/watch?v=ViPNHMSUcog

Perché studiamo il Lambda Calcolo? (Anima e Corpo)

Possiamo vedere le funzioni in due modi diverse:

• Visione Matematica Classica (Anima): Una funzione è una relazione statica tra insiemi. È la semantica.
• Lambda Calcolo (Corpo): Qui la funzione è un processo meccanico di calcolo. Ci interessa la sintassi, ovvero le regole scritte per trasformare un termine in un altro fino ad arrivare al risultato.

Quindi il $\lambda$-calcolo è il “motore” sotto il cofano di linguaggi come Haskell.

Sintassi e Computazione

la BNF (Backus-Naur Form) è il metalinguaggio usato per definire la grammatica rigida di un linguaggio. La grammatica del λ-calcolo puro si riduce a una sola riga:

$$M,N::=x\mid \lambda x.M\mid (MN)$$

Significa che un Termine Lambda (M o N) può assumere solo tre forme:

• Variabile (x): Semplici nomi di elementi (es. x,y,z).
• Astrazione (λx.M): La definizione di una funzione anonima che prende come parametro la variabile x e ha come corpo il termine M.
  • In Haskell: Corrisponde alla sintassi \x -> M.
• Applicazione (M N): La chiamata di una funzione. Significa “applica il primo termine M (la funzione) al secondo termine N (l’argomento)“.

Regole di associazione

• Astrazione associa a destra: $\lambda x_1\dots x_n.M$ equivale a $\lambda x1.(\lambda x_2.(\dots (\lambda x_n.M)\dots ))$
• Applicazione associa a sinistra: $F{N}_1{N}_2...N_n$ equivale a $(\dots (F{N}_1)\dots N_n)$

Computazione (β-regola)

La computazione avviene tramite la $\beta -\text{riduzione}$ (beta-regola): un termine della forma $(\lambda x.M)N$ si dice redex e si riduce sostituendo tutte le occorrenze di x in M con il termine N .

Un termine che non contiene più $\beta \text{-redex}$ è detto in forma normale e rappresenta un valore finale (il risultato della computazione).

Significato Redex

Redex sta per REDucible EXpression (Espressione Riducibile). Quindi, un β-redex significa letteralmente: “Un pezzo di codice che è pronto per essere calcolato tramite la regola beta”.

Variabili libere (free) e legate (bound)

Variabile Legata (Bound): È una variabile che compare nel corpo di una funzione ed è stata dichiarata nella λ di quella funzione. In programmazione, è un parametro locale.

Variabile Libera (Free): È una variabile che viene usata nel corpo, ma non c’è nessun λ che la definisce. In programmazione, è una variabile globale che arriva dall’esterno.

Esempi

Nel termine $x(\lambda x.(\lambda y.yx))$ ho che:

• la prima $x$ è libera
• mentre le y e le $x$ sono legate

Barendregt Name Convention

Osservare che nell’esempio precedente abbiamo lo stesso nome per due variabili diverse ($x\ne x$).

Infatti l termine $x(\lambda x.(\lambda y.yx))$ è equivalente al termine $x(\lambda z.(\lambda y.yz))$ e a tutti i termini in cui rinomino le variabili legate ($\alpha \text{-regola}$/$\alpha \text{-conversione}$).

Per evitare problemi, possiamo assumere tutti i nomi delle variabili legate diversi tra loro e diversi da quelli delle variabili libere.

Combinatori

Poiché nel λ-calcolo puro non esistono tipi di dato predefiniti, i combinatori vengono utilizzati per codificare ogni struttura logica e matematica, dai booleani ai numerii.

Combinatori di Base e Logic

Identità ( $I$)

$I\equiv \lambda x.x$, ovvero: qualsiasi termine applicato a I rimane invariato (I M -> M)

Cancellatori (Bool)

Nel λ-calcolo, un valore booleano è interpretato come una funzione di scelta:

• $K$ (o $T$ per True): $K\equiv \lambda xy.x$ , ovvero: prende due argomenti e restituisce il primo (KMN->M).
• $O$ (o $F$ per False) $O\equiv \lambda xy.y$ , ovvero: prende due argomenti e restituisce il secondo (OMN->N).

Proprio perché i booleani sono “selettori”, il costrutto if-then-elseè una semplice applicazione di funzione. L’espressione if x then M else N viene scritta semplicemente come x M N, infatti:

1. Se x è True ($K$): L’espressione diventa K M N. Per definizione di K, il risultato è M (il ramo then).
2. Se x è False ($O$) L’espressione diventa O M N. Per definizione di O, il risultato è N (il ramo else).

Compositore ( $S$):

$S\equiv \lambda xyz.xz(yz)$ distribuisce l’argomento z sia alla funzione x che alla funzione y.

Un notevole utilizzo è S K K che si comporta esattamente come l’identità $I$ ($SKK\approx I$)

---

Per dimostrare che $SKK\approx I$, dobbiamo applicare un termine generico w a questa combinazione e vedere se otteniamo w come risultato:

1. Espressione iniziale: (SKK) w
2. Applichiamo la definizione di S: (dove x=K,y=K,z=w) (SKK) w -> (K w)(K w).
3. Applichiamo la definizione di K: Ricorda che K applicato a un termine (in questo caso w) restituisce una funzione costante che ignora il suo secondo argomento e restituisce sempre quel termine.
4. Calcolo finale: Nell’espressione (K w)(K w), il primo (K w) agisce come una funzione che riceve il successivo (K w) come secondo argomento, quindi: (K w)(K w) -> w.

Combinatori per la Ricorsione (Punto Fisso)

Per definire funzioni ricorsive generali, il λ-calcolo utilizza il Combinatore di Punto Fisso ($Y$) , tale che $YM\to M(YM)$. I due più noti sono:

• Combinatore di Turing ($YT$): Definito come $\theta \theta$ dove $\theta \equiv \lambda xy.y(xxy)$.
• Combinatore di Curry ($YC$): Definito come $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$.

Duplicatori e Divergenza

Duplicatore ( $\omega$)

$\omega \equiv \lambda x.xx$ , ovvero l’operazione di auto-applicazione

Combinatore $\Omega$

Definito come $(\lambda x.xx)(\lambda x.xx)$ ovvero $\omega \omega$. Rappresenta il loop infinito per eccellenza perché riduce sempre a se stesso senza mai raggiungere una forma normale.

• In Haskell, $\Omega$ e l’auto-applicazione non sono tipabili a causa dell’occurs check, un controllo che impedisce la creazione di tipi infiniti.

Rappresentazione dei Dati

Numerali di Church

I numeri naturali sono rappresentati come iteratori. Ad esempio, il numero n è una funzione che applica n volte un parametro s (successore) a una base z (zero): $n\equiv \lambda sz.s(s(\dots (sz)\dots ))$

Tuple

Una tupla $(M_1,M_2,\dots ,M_k)$ è codificata come $\lambda x.x{M}_1{M}_2\dots M_k$​.

Per estrarre i valori si usano i proiettori ${\pi }_j^k\equiv \lambda x_1\dots x_k.x_j$