Lambda-calcolo

Negli anni Venti e Trenta del Novecento, logici e matematici come Hilbert, Gödel, Church e Turing cercavano un modello rigoroso di “procedura effettiva” (ossia di algoritmo) per affrontare il cosiddetto Entscheidungsproblem (problema della decisione): esiste un metodo meccanico per decidere la verità o falsità di qualunque enunciato matematico?

Per rispondere, occorreva chiarire cosa significhi calcolare in modo puramente meccanico: come descrivere formalmente una sequenza di operazioni che, dato un valore iniziale, produca un risultato.

Il matematico statunitense Alonzo Church sviluppò allora un formalismo minimale che prendeva come unica base il concetto di funzione matematica, in quanto una funzione può essere rappresentata come un processo che, dato un certo input, restituisce un certo output. La sua intuizione fu di considerare le funzioni non più soltanto come relazioni immutabili tra insiemi, ma come oggetti matematici manipolabili, su cui fondare una nuova branca della matematica: ecco quindi la nascita del $\lambda$-calcolo.

Definizione: $\lambda$-calcolo

Il $\lambda$-calcolo è un sistema formale formulato a partire dagli anni Trenta dal matematico americano Alonzo Church, sviluppato per esprimere formalmente il procedimento di computazione di una funzione matematica espressa per mezzo di un linguaggio formale i cui termini possono essere usati per rappresentare calcoli in modo astratto.

Il $\lambda$-calcolo essenzialmente permette di “calcolare” con le funzioni matematiche così come è possibile calcolare normalmente con i numeri: avendo anticipato così il concetto di linguaggio di programmazione prima dell’avvento stesso dei computer (che arriveranno solo negli anni Quaranta), il $\lambda$-calcolo viene considerato uno dei primi linguaggi di programmazione della storia ma utilizzabile solo “sulla carta” (perché, appunto, non esistevano ancora i computer lol).

Dal $\lambda$-calcolo, inoltre, nasce uno dei primi paradigmi di programmazione della storia: quello funzionale, che prende il nome proprio dal concetto delle funzioni matematiche su cui è costruito.

Per intenderci, guarda questa espressione apparentemente senza senso:

$$\begin{array}{c}\lambda n.n(\lambda f.\lambda a.\lambda x.f((\lambda x.\lambda y.\lambda z.x(yz))ax)\\ ((\lambda n.\lambda f.\lambda x.f(nfx))x))(\lambda x.\lambda y.x)\\ (\lambda f.\lambda x.fx)(\lambda f.\lambda x.fx)\end{array}$$

Sentiti liber* di crederci o no, ma questa espressione, che chiameremo termine, rappresenta il “codice” in $\lambda$-calcolo per calcolare il fattoriale di un numero naturale $n$ qualsiasi.

Ma come fa a essere questo ammasso di lettere casuali un codice? Se sei curios* di saperlo, benvenut* nel magico mondo del $\lambda$-calcolo.

(Attent*! Stai per finire in un rabbit-hole da cui potresti non uscirne più. Io ti ho avvertit*…)

Termini del $\lambda$-calcolo

Prima di arrivare a capire cosa sono gli oggetti principali con cui opera il $\lambda$-calcolo, cioè i termini, vediamo come sono nati.

Astrazioni

Durante il processo di definizione del $\lambda$-calcolo, Alonzo Church decise in primis di modificare la notazione classica della definizione di una funzione:

$$\begin{array}{rl}f:& A\to B\\ & a\mapsto b\end{array}$$

Il signor Church, per rendere la notazione più scorrevole e, soprattutto, il più astratta possibile (in modo da poterci fare operazioni più comodamente), scelse di evitare di indicare per ogni funzione il suo nome (in questo caso $f$) e gli insiemi posti in relazione ($A$ e $B$), valorizzando in particolare proprio la trasformazione che avviene grazie alla funzione ($a\mapsto b$).

La nuova notazione di Church rappresenta le funzioni introducendole con un $\lambda$ (da qui il nome del $\lambda$-calcolo) per indicare l’inizio della definizione di una funzione, seguito dalle due variabili separate da un punto:

$$\lambda a.b$$

Questo modo di definire “astrattamente” una funzione viene detto astrazione.

Definizione: astrazione

Nel $\lambda$-calcolo, un’astrazione (anche detta $\lambda$-astrazione) è una definizione di una funzione anonima, cioè una funzione che non ha un nome ma è identificata direttamente dalla sua regola di trasformazione.

Un’astrazione ha la forma:

$$\lambda x.M$$

dove:

• $x$ è una variabile che rappresenta l’argomento della funzione e
• $M$ è un termine del $\lambda$-calcolo che rappresenta il corpo della funzione.

Applicazioni

Con l’astrazione abbiamo capito come possiamo definire una funzione e il suo comportamento, ma concretamente come facciamo a “utilizzarla” dandole in input un certo numero?

Il mitico Alonzo decise di adottare quindi la seguente notazione: presa un’astrazione $\lambda x.M$, questa viene posta tra parentesi tonde e viene seguita dal numero $n$ che vogliamo sostituire all’argomento dell’astrazione:

$$(\lambda x.M)n$$

Per esempio, data un’astrazione $\lambda x.M$ dove $M$ indica la somma di $1$ a $x$ (quindi $x+1$) e $n$ è uguale a $3$, potremmo scrivere (seppur effettuando in questo caso un abuso di notazione, perché nel $\lambda$-calcolo non è possibile usare direttamente i numeri in questo modo):

$$(\lambda x.x+1)3$$

Ciò ci indica che, alla variabile di input $x$ che rappresenta l’argomento dell’astrazione, noi dobbiamo sostituire il numero $3$, in modo da ottenere come risultato $4$: a questa notazione Church diede il nome di applicazione.

Definizione: applicazione

Nel $\lambda$-calcolo, un’applicazione (anche detta $\lambda$-applicazione) è l’operazione che consiste nell’utilizzare una funzione su un argomento.

Un’applicazione ha la forma:

$$(MN)$$

dove:

• $M$ è un’espressione del $\lambda$-calcolo che rappresenta una funzione e
• $N$ è un’espressione del $\lambda$-calcolo che rappresenta l’argomento su cui la funzione viene applicata.

Termini

Ora che abbiamo definito cosa sono un’astrazione e un’applicazione, potremmo dire che questi due sono gli oggetti fondamentali con cui andremo a operare nel $\lambda$-calcolo: i nostri termini, quindi, possono assumere una di queste forme sintattiche possibili tra un’astrazione, un’applicazione e una semplice variabile.

Definizione: termine nel $\lambda$-calcolo

Nel $\lambda$-calcolo, un termine $T$ (anche detto $\lambda$-termine o $\lambda$-espressione) è una stringa ben formata a partire dalla seguente grammatica espressa in BNF:

$$T::=x\mid (\lambda x.T)\mid (TT)$$

dove:

1. $x$ è una variabile,
2. $(\lambda x.T)$ è un’astrazione con argomento $x$ e corpo $T$ e
3. $(TT)$ è un’applicazione in cui la funzione $T$ viene applicata all’argomento $T$.

Ognuna di queste 3 forme che può assumere un termine è detta forma sintattica.

Esempi di termini

Ecco qualche esempio di termini del $\lambda$-calcolo correttamente espressi:

• $x$ è un termine che rappresenta una semplice variabile $x$.
• $(\lambda x.x)$ è un termine che rappresenta un’astrazione con argomento $x$ e corpo $x$.
• $((\lambda x.(xx))(\lambda y.(yy)))$ è un termine che rappresenta un’applicazione della funzione $(\lambda x.(xx))$ all’argomento $(\lambda y.(yy))$. A loro volta, possiamo analizzare questi “sotto-termini”:
  • $(\lambda x.(xx))$ è un termine che rappresenta un’astrazione con argomento $x$ e corpo $(xx)$. A sua volta:
    • $(xx)$ è un termine che rappresenta un’applicazione della funzione $x$ all’argomento $x$.
  • $(\lambda y.(yy))$ è un termine che rappresenta un’astrazione con argomento $y$ e corpo $(yy)$. A sua volta:
    • $(yy)$ è un termine che rappresenta un’applicazione della funzione $y$ all’argomento $y$.
• $(\lambda f.(\lambda x.(f(fx))))$ è un termine che rappresenta un’astrazione con argomento $f$ e corpo $(\lambda x.(f(fx)))$. A sua volta:
  • $(\lambda x.(f(fx)))$ è un termine che rappresenta un’astrazione con argomento $x$ e corpo $(f(fx))$. A sua volta:
    • $(f(fx))$ è un termine che rappresenta un’astrazione con argomento $f$ e corpo $(fx)$. A sua volta:
      • $(fx)$ è un termine che rappresenta un’applicazione della funzione $f$ all’argomento $x$.

Riscrittura dei termini

È possibile riscrivere i termini eliminando alcune parentesi per migliorare la leggibilità.

Notazione: omissione delle parentesi più esterne di un termine

In un termine è possibile omettere le parentesi più esterne.

Per esempio, un termine $T=(\lambda V.T)$ che rappresenta un’astrazione con argomento $V$ e corpo $T$ si può riscrivere come $T=\lambda V.T$.

Allo stesso modo, un termine $T^{\prime }=(UV)$ che rappresenta un’applicazione della funzione $U$ all’argomento $V$ si può riscrivere come $T^{\prime }=UV$.

Notazione: omissione delle parentesi in un'astrazione

In un termine $T=\lambda V.T^{\prime }$ che rappresenta un’astrazione con argomento $V$ e corpo $T$ si possono eliminare le parentesi più esterne del sotto-termine $T^{\prime }$.

Per esempio, un termine $T=\lambda V.(X(\lambda y.Z))$ si può riscrivere come $T=\lambda V.X(\lambda y.Z)$. Semplicemente, se non sono presenti delle parentesi, tutto quello a destra del punto viene considerato come il corpo dell’astrazione (che in questo caso corrisponderebbe a $X(\lambda y.Z)$).

Notazione: omissione delle parentesi in un'applicazione

In un termine $T=UV$ che rappresenta un’applicazione della funzione $U$ all’argomento $V$ si possono eliminare le parentesi più esterne della funzione $U$.

Per esempio, un termine $T=(M_1{M}_2)(M_3{M}_4)$ si può riscrivere come $T=M_1{M}_2(M_3{M}_4)$, ma NON come $T=M_1{M}_2{M}_3{M}_4$​ perché $(M_3{M}_4)$ è l’argomento dell’applicazione.

Esercizio 1 sulla riscrittura dei termini

Rimuovere il più possibile le parentesi, senza cambiare il significato, del seguente termine:

$$(\lambda x.((xx)x))$$

Soluzione

È possibile innanzitutto rimuovere le parentesi più esterne del termine:

$$\lambda x.((xx)x)$$

A questo punto, avendo un’astrazione con argomento $x$ e corpo $((xx)x)$, è possibile rimuovere le parentesi nel corpo:

$$\lambda x.(xx)x$$

Il corpo $(xx)$ x è un’applicazione della funzione $(xx)$ all’argomento $x$, quindi possiamo rimuovere le parentesi della funzione:

$$\lambda x.xxx$$

Variabili libere e legate in un termine

Prima di cominciare a effettuare operazioni con i termini, ci serve definire un ultimo concetto che ci permette di capire quale valore hanno le variabili all’interno dei termini stessi: per esempio, nell’astrazione $\lambda x.M$ e nell’applicazione $xM$ la variabile $x$ non ha lo stesso “peso”, perché nel primo caso è “legata” al termine $M$ (essendo un argomento di quella funzione), mentre nel secondo caso è “libera” e non ha alcun particolare legame con $M$.

Fare questa distinzione è importante perché, svolgendo operazioni sui termini, dobbiamo assicurarci che il loro significato non venga modificato andando a toccare quelle variabili “legate”.

Definiamo formalmente quindi questa differenza.

Definizione: variabili libere e legate

L’insieme delle variabili libere di un termine $T$, denotate con $\text{fv}(T)$ (dall’inglese free variables), è definito induttivamente sulla struttura di $T$ come segue:

• Quando il termine $T$ è una variabile $x$:

  $$\text{fv}(T)=\text{fv}(x)\stackrel{\text{def}}{=}\{x\}$$

• Quando il termine $T$ è un’astrazione $\lambda x.M$:

  $$\text{fv}(T)=\text{fv}(\lambda x.M)\stackrel{\text{def}}{=}\text{fv}(M)\setminus \{x\}$$

• Quando il termine $T$ è un’applicazione $MN$:

  $$\text{fv}(T)=\text{fv}(MN)\stackrel{\text{def}}{=}\text{fv}(M)\cup \text{fv}(N)$$

Una variabile contenuta in $T$ si dice libera se è presente in $\text{fv}(T)$, legata altrimenti.

Esempi di variabili libere e legate

Ecco qualche esempio di variabili libere e legate in diversi termini:

• $x$: la variabile $x$ è libera perché non è vincolata da alcuna astrazione:

  $$\text{fv}(x)=\{x\}$$

• $\lambda x.x$: la variabile $x$ è legata perché è vincolata dall’astrazione (essendo un suo argomento):

  $$\begin{array}{rl}\text{fv}(\lambda x.y)& =\text{fv}(x)\setminus \{x\}\\ & =\{x\}\setminus \{x\}\\ & =\varnothing \end{array}$$

• $\lambda x.y$: la variabile $x$ è legata perché è vincolata dall’astrazione (essendo un suo argomento), ma la variabile $y$ no:

  $$\begin{array}{rl}\text{fv}(\lambda x.y)& =\text{fv}(y)\setminus \{x\}\\ & =\{y\}\setminus \{x\}\\ & =\{y\}\end{array}$$

• $\lambda x.\lambda y.yzx$: le variabili $x$ e $y$ sono legate perché vincolate dalle rispettive astrazioni (essendo loro argomenti), ma la variabile $z$ no:

$$\begin{array}{rl}\text{fv}(\lambda x.\lambda y.yzx)& =\text{fv}(\lambda y.yzx)\setminus \{x\}\\ & =(\text{fv}(yzx)\setminus \{y\})\setminus \{x\}\\ & =((\text{fv}(y)\cup \text{fv}(z)\cup \text{fv}(x))\setminus \{y\})\setminus \{x\}\\ & =((\{y\}\cup \{z\}\cup \{x\})\setminus \{y\})\setminus \{x\}\\ & =(\{y,z,x\}\setminus \{y\})\setminus \{x\}\\ & =\{z,x\}\setminus \{x\}\\ & =\{z\}\end{array}$$

Osservazione: variabili libere e legate come visibilità nei linguaggi di programmazione

La distinzione tra variabili libere e legate è utile a farci capire, trasportando questo concetto sui linguaggi di programmazione, a capire qual è la visibilità delle variabili che usiamo:

• Le variabili legate possono essere pensate come variabili “locali” della funzione, utilizzabili unicamente all’interno di quella funzione e senza bisogno di altre informazioni dall’esterno per capire a cosa servono.
• Le variabili libere possono essere pensate come variabili “globali” della funzione, usate al suo interno ma in realtà dichiarate all’esterno della funzione e, quindi, il loro valore dipende dal contesto in cui si trova la funzione.

Definizione: cattura di una variabile libera

Una cattura è l’operazione con cui una variabile libere diventa legata.

Combinatori

Un concetto strettamente collegato a quello di variabili libere e che ci tornerà utile più tardi è quello dei combinatori.

Definizione: combinatore

Un combinatore (o termine chiuso) è un termine $T$ senza variabili libere:

$$\text{fv}(T)=\varnothing$$

Relazioni tra termini

Sostituzione

Come abbiamo visto, un’applicazione $MN$ rappresenta essenzialmente la sostituzione delle variabili contenute in $M$ con i valori di $N$. Ma ciò non è un’operazione banale: le uniche variabili sostituibili sono quelle libere e questa è una cosa di cui bisogna tener conto per evitare catture. Definiamo quindi correttamente come deve funzionare una sostituzione in un termine.

Definizione: sostituzione

Nel $\lambda$-calcolo, una sostituzione è un’operazione binaria tra due termini $T$ ed $N$ in cui una variabile libera $y$ di $T$ viene sostituita con $N$. Viene denotata come $T[N/y]$ ed è definita induttivamente sulla struttura di $T$ come segue:

• Quando il termine $T$ è una variabile $x$:

  $$T[N/y]=x[N/y]\stackrel{\text{def}}{=}\{\begin{array}{ll}N& x=y\\ x& x\ne y\end{array}$$

• Quando il termine $T$ è un’astrazione $\lambda x.M$:

  $$T[N/y]=(\lambda x.M)[N/y]\stackrel{\text{def}}{=}\{\begin{array}{ll}\lambda x.M& x=y\\ \lambda x.M[N/y]& x\ne y\wedge x\notin \text{fv}(N)\\ \lambda z.M[z/x][N/y]& x\ne y\wedge x\in \text{fv}(N)\end{array}$$

  con $z\in \text{Var}\setminus (\text{fv}(M)\cup \text{fv}(N))$

• Quando il termine $T$ è un’applicazione $M_1{M}_2$​:

  $$T[N/y]=(M_1{M}_2)[N/y]\stackrel{\text{def}}{=}{M}_1[N/y]M_2[N/y]$$

$\alpha$-conversione

Abbiamo detto che le funzioni matematiche sono quindi un modo per rappresentare in maniera generica una relazione tra due insiemi.

Per esempio, la relazione che associa a ogni numero naturale $x$ il suo quadrato $x^2$ (anch’esso nell’insieme dei numeri naturali $\mathbb{N}$) possiamo rappresentarla con la funzione

$$\begin{array}{rl}f:& \mathbb{N}\to \mathbb{N}\\ & x\mapsto x^2\end{array}$$

Ma al posto di $x$ potremmo usare un’altra variabile per descrivere la funzione mantenendo invariato il suo significato, per esempio $y$:

$$\begin{array}{rl}f:& \mathbb{N}\to \mathbb{N}\\ & y\mapsto y^2\end{array}$$

Oppure anche un simbolo che non è una lettera, come il simbolo $\star$ (si legge star, ossia stella):

$$\begin{array}{rl}f:& \mathbb{N}\to \mathbb{N}\\ & \star \mapsto {\star }^2\end{array}$$

Queste tre rappresentazioni sono perfettamente equivalenti e, nell’ambito del $\lambda$-calcolo, Alonzo Church decise di chiamare il processo di rinominare le variabili di una funzione con il nome di $\alpha$-conversione.

Definizione: $\alpha$-conversione

L’$\alpha$-conversione, denotata con ${\equiv }_{\alpha }$​, è una relazione binaria tra due astrazioni $\lambda x.M$ e $\lambda y.M$ che permette di rinominare la variabile legata $x$ in un’altra variabile legata $y$ senza alterare il significato del termine:

$$y\notin \text{fv(M)}⟺\lambda x.M{\equiv }_{\alpha }\lambda y.M[y/x]$$

Le due astrazioni $\lambda x.M$ e $\lambda y.M$ si dicono $\alpha$-equivalenti.

$\beta$-riduzione

In matematica abbiamo che, data per esempio una funzione $f(x)=x^2+2x+1$, allora $f(5)=5^2+2\cdot 5+1=36$.

Nell’ambito del $\lambda$-calcolo, applicare un’astrazione $\lambda x.M$ a un argomento $N$ significa valutare il corpo della funzione $M$ in cui ogni occorrenza della variabile libera $x$ è stata sostituita da $N$. Per intenderci, nell’esempio di prima abbiamo valutato $f(x)$ applicandola all’argomento $5$.

Questa idea è alla base della $\beta$-riduzione.

Definizione: $\beta$-riduzione

La $\beta$-riduzione, denotata con ${\to }_{\beta }$​, è l’operazione che permette di sostituire in un’applicazione $(\lambda x.M)N$ l’argomento $x$ dell’astrazione con l’argomento $N$:

$$(\lambda x.M)N{\to }_{\beta }M[N/x]$$

In particolare, diciamo che:

• $(\lambda x.M)N$ è un $\beta$-redex (da reducible expression, in italiano espressione riducibile) o, in alcuni casi, ricalcato in italiano come redesso e
• $M[N/x]$ è il suo ridotto.

L’operazione inversa, cioè quella che dal ridotto ci fa risalire al redesso, viene detta $\beta$-espansione e viene denotata con ${\leftarrow }_{\beta }$​:

$$M[N/x]{\leftarrow }_{\beta }(\lambda x.M)N$$

Esempi di $\beta$-riduzione

Ecco qualche esempio di $\beta$-riduzione correttamente svolta:

$$\begin{array}{rl}(\lambda x.x)M& {\to }_{\beta }x\end{array}$$ $$\begin{array}{rl}(\lambda x.xx)(\lambda y.y)& {\to }_{\beta }(\lambda y.y)(\lambda y.y)\\ & {\to }_{\beta }\lambda y.y\end{array}$$ $$\begin{array}{rl}(\lambda f.\lambda x.f(fx))M& {\to }_{\beta }\lambda x.M(Mx)\end{array}$$ $$\begin{array}{rl}(\lambda f.\lambda g.\lambda x.f(gx))MN& {\to }_{\beta }(\lambda g.\lambda x.M(gx))N\\ & {\to }_{\beta }\lambda x.M(Nx)\end{array}$$ $$\begin{array}{rlr}(\lambda x.\lambda y.x)MN& {\to }_{\beta }(\lambda y.M)N& \\ & {\to }_{\beta }M& \text{β-riduzione}\end{array}$$

$\eta$-riduzione

Prendiamo un esempio di $\beta$-riduzione:

$$\begin{array}{rl}(\lambda x.Mx)N& {\to }_{\beta }MN\end{array}$$

Dal momento che l’applicazione della funzione $(\lambda x.Mx)$ all’argomento $N$ e l’applicazione della funzione $M$ all’argomento $N$ generano in entrambi i casi $MN$, per il principio di estensionalità delle funzioni potremmo dire che $(\lambda x.Mx)$ e $M$ sono due funzioni equivalenti, quindi l’una deve essere trasformabile nell’altra attraverso una $\beta$-riduzione.

Tuttavia, però, non in tutti i casi può valere la $\beta$-riduzione che da $(\lambda x.Mx)$ ci porta a $M$ o viceversa (attenzione: per poter applicare la $\beta$-riduzione e ottenere $M$ ci serve avere $(\lambda x.M)x$ che non è equivalente a $(\lambda x.Mx)$!):

$$\begin{array}{r}(\lambda x.Mx)/{\to }_{\beta }M\\ M/{\to }_{\beta }(\lambda x.Mx)\end{array}$$

Ciò ci fa pensare che, per continuare a far valere correttamente il principio di estensionalità delle funzioni, la $\beta$-riduzione da sola non ci basta (come, per esempio, in questi casi appena visti): abbiamo bisogno di introdurre quindi una nuova operazione, la $\eta$-riduzione.

Definizione: $\eta$-riduzione

L’$\eta$-riduzione, denotata con ${\to }_{\eta }$​, è l’operazione che permette di ridurre un’astrazione $\lambda x.Mx$ nel termine $M$:

$$\lambda x.Mx{\to }_{\eta }M$$

In particolare, diciamo che:

• $\lambda x.Mx$ è un $\eta$-redex (da reducible expression, in italiano espressione riducibile) o, in alcuni casi, ricalcato in italiano come redesso e
• $M$ è il suo ridotto.

L’operazione inversa, cioè quella che dal ridotto ci fa risalire al redesso, viene detta $\eta$-espansione e viene denotata con ${\leftarrow }_{\eta }$:

$$M{\leftarrow }_{\eta }\lambda x.Mx$$

Riduzione singola e multipla

Durante lo svolgimento di $\beta$-riduzioni ed $\eta$-riduzioni è comodo alcune volte “generalizzare” il concetto di riduzione senza specificare quale delle due si sta applicando: per questo motivo, chiamiamo riduzione singola, denotata con →, l’uso generale di una delle due riduzioni tra la $\beta$-riduzione e l’$\eta$-riduzione.

Definizione: riduzione singola

Una riduzione singola (o, più semplicemente, riduzione), denotata con $\to$, è un singolo passo di $\beta$-riduzione o di $\eta$-riduzione.

$M$ si dice riducibile in $N$.

Avendo definito formalmente la riduzione singola, possiamo ora generalizzare ulteriormente più passi di riduzione in una sola operazione, senza avere la necessità di esplicitarli tutti: definiamo quindi la riduzione multipla.

Definizione: riduzione multipla

Una riduzione multipla, denotata con $\Rightarrow$ (o, in alcuni casi, con ${\to }^{\star }$), è una chiusura riflessiva e transitiva della relazione di riduzione singola, ossia la più piccola relazione tale che:

• Riflessività (zero passi sono ammessi): $M⟹M$.
• Un passo è ammesso: $(M\to N)⟹(M\Rightarrow N)$.
• Transitività (più passi sono ammessi): $(M\Rightarrow N\wedge N\Rightarrow O)⟹(M\Rightarrow O)$.

$M$ si dice riducibile in zero o più passi in $N$.

Convertibilità

La riduzione multipla è una relazione tra due termini che può essere interpretata come una sorta di “equivalenza” tra di essi: se abbiamo che $M\Rightarrow N$, allora possiamo dedurre che in qualche modo dal termine $M$ si può arrivare al termine $N$, seppur con più di qualche passaggio di riduzione singola. Viceversa, facendo lo stesso discorso per le espansioni, cioè $\beta$-espansione ed $\eta$-espansione, si potrebbe dire che da $N$ possiamo risalire a $M$. Insomma, si potrebbe dire che $M$ ed $N$ sono uguali semanticamente, cioè rappresentano la stessa funzione.

A questa intercambiabilità tra termini collegati da una riduzione multipla diamo il nome di convertibilità.

Definizione: convertibilità

Sia $\Lambda$ l’insieme di termini del $\lambda$-calcolo. La relazione binaria $\iff \subseteq \Lambda \times \Lambda$ è detta convertibilità ed è definita come segue:

$$\forall M,N\in \Lambda (M\iff N⟺(M\Rightarrow N\vee N\Rightarrow M))$$

Forma normale e strategie di riduzione

Osservazione: $\beta$-riduzioni che non terminano

Consideriamo il seguente esempio di $\beta$-riduzione:

$$\begin{array}{rl}(\lambda x.xx)(\lambda y.yy)& {\to }_{\beta }(\lambda y.yy)(\lambda y.yy)\\ & {\to }_{\beta }(\lambda y.yy)(\lambda y.yy)\\ & \dots \end{array}$$

Come possiamo notare, ogni passo di $\beta$-riduzione non ci permette di ridurre ulteriormente il termine ma ci fa ritornare puntualmente allo stato in cui è nella forma $(\lambda x.xx)(\lambda y.yy)$: da ciò possiamo evincere che la $\beta$-riduzione in alcuni casi può anche non terminare mai.

Questo particolare termine $(\lambda x.xx)(\lambda y.yy)$ è un combinatore (perché ha solo variabili legate) e scopriremo più tardi che è un combinatore molto famoso, ossia il combinatore di punto fisso $Y$.

Intanto, ai termini che prima o poi arrivano a un certo punto in cui non possono essere più ridotti diciamo che sono in forma normale.

Definizione: forma normale

Nel $\lambda$-calcolo, un termine $M$ si dice che è in forma normale e si denota con $M\nrightarrow$ se non può più essere ridotto, ovvero se non esiste un altro termine $N$ tale che $M\to N$:

$$\forall M\in \Lambda ((M\nrightarrow )⟺\nexists N\in \Lambda (M\to N))$$

dove $\Lambda$ è l’insieme di termini del $\lambda$-calcolo.

Confluenza

Teorema della confluenza

Sia $\Lambda$ l’insieme di termini del $\lambda$-calcolo. Dati tre termini $M,N_1,N_2\in \Lambda$, con $M\Rightarrow N_1$ e $M\Rightarrow N_2$​, allora esiste un termine $N\in \Lambda$ tale che $N_1\Rightarrow N$ e $N_2\Rightarrow N$.

$$\forall M,N_1,N_2\in \Lambda ((M\Rightarrow N_1\wedge M\Rightarrow N_2)⟹\exists N\in \Lambda (N_1\Rightarrow N\wedge N_2\Rightarrow N))$$

Corollario del teorema della confluenza

La forma normale di un termine $M$, se esiste, è unica (a meno di $\alpha$-conversioni).

In termini matematici, per ogni termine $M$, se esistono due termini $N_1$ ed $N_2$​ in forma normale ($N_1\nrightarrow$ e $N_2\nrightarrow$) nei quali $M$ può essere ridotto ($M\Rightarrow N_1$ e $M\Rightarrow N_2$​), allora $N_1$ ed $N_2$​ sono $\alpha$-equivalenti ($N_1{\equiv }_{\alpha }{N}_2$​):

$$\forall M\in \Lambda ,\exists N_1,N_2\in \Lambda \left(\right((M\Rightarrow N_1\nrightarrow )\wedge (M\Rightarrow N_2\nrightarrow ))⟹(N_1{\equiv }_{\alpha }{N}_2))$$

dove $\Lambda$ è l’insieme di termini del $\lambda$-calcolo.

Strategie di riduzione

Definizione: ordine applicativo

L’ordine applicativo è una strategia di riduzione in cui applicare una funzione a un argomento significa prima valutare l’argomento e poi sostituire il valore ottenuto nel corpo della funzione. In altre parole, in un termine del tipo

$$(\lambda x.x)((\lambda y.y)z)$$

viene scelto il $\beta$-redex più a sinistra e più interno, ossia in questo caso $(\lambda y.y)z$:

$$(\lambda x.x)((\lambda y.y)z){\to }_{\beta }(\lambda x.x)z$$

I linguaggi funzionali che utilizzano l’ordine applicativo sono detti linguaggi zelanti (in inglese eager languages).

Definizione: ordine normale

L’ordine normale è una strategia di riduzione in cui applicare una funzione a un argomento significa sostituire l’argomento nel corpo della funzione. In altre parole, in un termine del tipo

$$(\lambda x.x)((\lambda y.y)z)$$

viene scelto il $\beta$-redex più a sinistra e più esterno, ossia in questo caso l’intero termine:

$$(\lambda x.x)((\lambda y.y)z){\to }_{\beta }(\lambda y.y)z$$

I linguaggi funzionali che utilizzano l’ordine applicativo sono detti linguaggi pigri (in inglese lazy languages).

Osservazione: cosa scegliere tra ordine applicativo e ordine applicativo

Le due strategie di riduzione viste, ossia l’ordine applicativo e l’ordine normale, non sono equivalenti, e spesso conviene usare una al posto dell’altra.

Prendiamo come esempio il seguente termine:

$$(\lambda x.y)((\lambda z.z)(\lambda z.z))$$

Se eseguito con l’ordine applicativo, otteniamo le seguenti $\beta$-riduzioni:

$$\begin{array}{rl}(\lambda x.y)((\lambda z.z)(\lambda z.z))& {\to }_{\beta }(\lambda x.y)(\lambda z.z)\\ & {\to }_{\beta }y\end{array}$$

Se invece viene eseguito con l’ordine normale, otteniamo la seguente $\beta$-riduzione:

$$\begin{array}{rl}(\lambda x.y)((\lambda z.z)(\lambda z.z))& {\to }_{\beta }y\end{array}$$

Notiamo quindi che in questo caso l’ordine normale conviene, perché in questo modo l’argomento $x$ non viene proprio valutato.

Al contrario, consideriamo il seguente termine:

$$(\lambda x.xx)((\lambda y.y)(\lambda z.z))$$

Se eseguito con l’ordine applicativo, otteniamo le seguenti $\beta$-riduzioni:

$$\begin{array}{rl}(\lambda x.xx)((\lambda y.y)(\lambda z.z))& {\to }_{\beta }(\lambda x.xx)(\lambda z.z)\\ & {\to }_{\beta }(\lambda z.z)(\lambda z.z)\\ & {\to }_{\beta }\lambda z.z\end{array}$$

Se invece viene eseguito con l’ordine normale, otteniamo le seguenti $\beta$-riduzioni:

$$\begin{array}{rl}(\lambda x.xx)((\lambda y.y)(\lambda z.z))& {\to }_{\beta }((\lambda y.y)(\lambda z.z))((\lambda y.y)(\lambda z.z))\\ & {\to }_{\beta }(\lambda z.z)((\lambda y.y)(\lambda z.z))\\ & {\to }_{\beta }(\lambda y.y)(\lambda z.z)\\ & {\to }_{\beta }\lambda z.z\end{array}$$

Possiamo notare come invece, in questo caso, convenga usare l’ordine applicativo perché l’argomento $x$ viene usato due volte e in quest’ultimo caso viene valutato entrambe le volte in due step diversi.

Normalizzazione

Teorema della normalizzazione

Dati due termini $M,N$, se $M$ è convertibile in $N$ (cioè $M\iff N$) ed $N$ è in forma normale ($N\nrightarrow$), allora esiste una riduzione multipla composta da $\beta$-riduzioni in ordine normale (che indichiamo con ${\Rightarrow }_{\text{no}}$) che porta da $M$ a $N$:

$$(M\iff N\wedge N\nrightarrow )⟹(M{\Rightarrow }_{\text{no}}N)$$

Osservazione: teorema della normalizzazione non vale per l'ordine applicativo

Il teorema della normalizzazione vale solo se le $\beta$-riduzioni vengono eseguite secondo l’ordine normale, mentre non vale se si usa l’ordine applicativo. Un esempio di ciò è dato dal seguente termine:

$$(\lambda x.y)((\lambda x.xx)(\lambda x.xx))$$

Se eseguito con l’ordine applicativo, abbiamo:

$$\begin{array}{rl}(\lambda x.y)((\lambda x.xx)(\lambda x.xx))& {\to }_{\beta }(\lambda x.y)(xx)[(\lambda x.xx)/x]\\ & =(\lambda x.y)((\lambda x.xx)(\lambda x.xx))\\ & \dots \end{array}$$

Possiamo notare che il termine, con questa strategia di riduzione, non raggiunge mai la sua forma normale. Al contrario, con l’ordine normale abbiamo:

$$\begin{array}{rl}(\lambda x.y)((\lambda x.xx)(\lambda x.xx))& {\to }_{\beta }y[((\lambda x.xx)(\lambda x.xx))/x]\\ & =y\end{array}$$

Con l’ordine normale raggiungiamo subito la forma normale.

Currying

Abbiamo notato che nelle astrazioni possiamo passare come parametri una singola variabile, il che sembra abbastanza limitante se abbiamo bisogno di usare funzioni che necessitano più parametri.

Possiamo tuttavia usare un piccolo trucchetto sfruttando le funzioni di ordine superiore. Prendendo per esempio due variabili $x$ e $y$ che devono essere passate come parametri alla stessa funzione $x+y$, possiamo creare un’astrazione che ha come parametro $x$ e nel suo corpo prende un’altra astrazione che ha come parametro $y$ e come corpo $x+y$:

$$\lambda x.\lambda y.x+y$$

In questo modo, applicando a quest’astrazione i due valori per i parametri $x$ e $y$ (per esempio, passiamo rispettivamente i valori $2$ e $3$), tramite la $\beta$-riduzione possiamo verificare che otterremo proprio quel che vogliamo:

$$\begin{array}{rl}(\lambda x.\lambda y.x+y)23& {\to }_{\beta }(\lambda y.x+y)[2/x]3\\ & =(\lambda y.2+y)3\\ & {\to }_{\beta }(2+y)[3/y]\\ & =2+3\\ & =5\end{array}$$

Questo metodo di passare molteplici parametri alla stessa astrazione venne chiamato currying, in onore del matematico Haskell Curry per il suo apporto al $\lambda$-calcolo.

Definizione: currying

Il currying è una tecnica che permette di applicare a un’astrazione con corpo $L$ più valori $M,N,\dots ,O$ per ognuno dei suoi argomenti $x,y,\dots ,z$:

$$(\lambda x.\lambda y.\dots .\lambda o.L)MN\dots O\iff L[M/x][N/y]\dots [O/z]$$

---

Fonti

• 🏫 Corso di Laurea in Informatica (L-31 R) presso l’Università di Torino:
  • Corso di Linguaggi e Paradigmi di Programmazione, A.A. 2020-21 (pagina Moodle):
    • Prof. Luca Padovani, slide del corso:
      • Introduzione ai paradigmi di programmazione e breve storia dei linguaggi funzionali.
      • Sintassi del $\lambda$-calcolo.
      • Semantica operazionale del $\lambda$-calcolo.
      • Confluenza e strategie di riduzione.
    • Prof. Luca Padovani, videoregistrazioni del corso:
      • Introduzione ai paradigmi di programmazione e breve storia dei linguaggi funzionali.
      • Sintassi del $\lambda$-calcolo.
      • Semantica operazionale del $\lambda$-calcolo.
      • Confluenza e strategie di riduzione.
  • Corso di Linguaggi e Paradigmi di Programmazione, A.A. 2025-26 (pagina Moodle):
    • Prof. Viviana Bono, lezioni del corso.
• 📹 Eyesomorphic, Programming with Math | The Lambda Calculus su YouTube.
• 🌐 Lambda-calcolo su Wikipedia in lingua italiana, URL consultato l’ultima volta e archiviato il 25 novembre 2025.
• 🌐 Simply typed lambda calculus su Wikipedia in lingua inglese, URL consultato l’ultima volta e archiviato il 25 novembre 2025.
• 🧠 Consultazione di ChatGPT.