Codifica di Church

Premessa

Ciao! Se è la prima volta che capiti su questo sito, ti consiglio di consultare la pagina principale di questo cosiddetto Giardino Digitale per scoprire meglio cos’è e come navigarlo.

Lo stato di questa nota è al momento: 🟡 Incompleta.

---

Con l’introduzione a variabili, astrazioni, applicazioni, operazioni come la $\beta$-riduzione e metodi come il currying, abbiamo tutto quel che ci serve per trasformare il $\lambda$-calcolo in un linguaggio di programmazione Turing-completo (tramite l’implementazione di strumenti fondamentali nella programmazione come cicli, tipi di dati basilari e strutture dati più complicate), esattamente come dimostrato nella tesi di Church-Turing.

Per fare ciò, Church ha ideato una sua codifica, la codifica di Church, che permette di esprimere coerentemente (dal punto di vista semantico) tutti i costrutti fondamentali della computazione esclusivamente mediante il $\lambda$-calcolo.

Definizione: codifica di Church

La codifica di Church è una rappresentazione formale dei dati e degli operatori all’interno del $\lambda$-calcolo, in cui ogni valore e ogni operazione vengono espressi unicamente attraverso termini.

1 - Logica booleana e strutture di controllo

Partendo dai classici valori booleani $\text{TRUE}$ e $\text{FALSE}$, Church nella sua codifica decise di definirli seguendo una semplice regola: presi due valori in input $x$ e $y$ (tramite currying), TRUE restituirà il primo valore ($x$) e FALSE il secondo ($y$):

$$\begin{array}{c}\text{TRUE}\stackrel{\text{def}}{=}\lambda x.\lambda y.x\\ \text{FALSE}\stackrel{\text{def}}{=}\lambda x.\lambda y.y\end{array}$$

Definizione: valori booleani nella codifica di Church

Nella codifica di Church, i valori booleani vero e falso sono rispettivamente codificati nei termini $\text{TRUE}$ e $\text{FALSE}$ definiti come segue:

$$\begin{array}{c}\text{TRUE}\stackrel{\text{def}}{=}\lambda x.\lambda y.x\\ \text{FALSE}\stackrel{\text{def}}{=}\lambda x.\lambda y.y\end{array}$$

Questa definizione di $\text{TRUE}$ e $\text{FALSE}$ può sembrare completamente arbitraria e senza senso così da sola, ma se codifichiamo un termine $\text{IF}$ (che rappresenta una struttura di controllo) come

$$\text{IF}\stackrel{\text{def}}{=}\lambda z.z$$

e applichiamo questo termine $\text{IF}$ nel seguente modo:

$$\text{IF}\text{TRUE}MN$$

allora possiamo dimostrare che verrà correttamente restituito il termine $M$ e, se calcoliamo invece il risultato di

$$\text{IF}\text{FALSE}MN$$

otterremo il termine $N$, esattamente come vorremmo che si comportasse una struttura di controllo.

Definizione: struttura di controllo nella codifica di Church

Nella codifica di Church, la struttura di controllo è codificata nel termine $\text{IF}$ definito come segue:

$$\text{IF}\stackrel{\text{def}}{=}\lambda z.z$$

Ora verifichiamo formalmente che l’$\text{IF}$ si comporta come vorremmo.

Verifica della correttezza semantica dell' $\text{IF}$

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

Dati due termini $M,N\in \Lambda$:

1. La $\lambda$-espressione $\text{IF}\text{TRUE}MN$ è convertibile in $M$:

$$\text{IF}\text{TRUE}MN\iff M$$

2. La $\lambda$-espressione $\text{IF}\text{FALSE}MN$ è convertibile in $N$:

$$\text{IF}\text{FALSE}MN\iff N$$

Ovviamente, quando andremo a “programmare” realmente tramite il $\lambda$-calcolo, al posto di $\text{TRUE}$ e $\text{FALSE}$ ci saranno delle espressioni booleane codificate in $\lambda$-calcolo che, appunto, si ridurranno nei valori $\text{TRUE}$ e $\text{FALSE}$.

Osservazione: usare l' $\text{IF}$ in un linguaggio zelante

Osserviamo cosa succede se proviamo a usare l’$\text{IF}$ in un linguaggio zelante, ossia usando l’ordine applicativo.

Proviamo per esempio a ridurre la $\lambda$-espressione $\text{IF}\text{TRUE}MN$ usando l’ordine applicativo:

$$\begin{array}{rlr}\text{IF}\text{TRUE}MN& =(\lambda z.z)(\lambda x.\lambda y.x)MN& \text{definizione di IF e TRUE}\\ & {\to }_{\beta }z[(\lambda x.\lambda y.x)MN/z]& \text{β-riduzione}\\ & =(\lambda x.\lambda y.x)MN& \text{sostituzione}\\ & {\to }_{\beta }(\lambda y.x)[MN/x]& \text{β-riduzione}\\ & =\lambda y.MN& \text{sostituzione}\end{array}$$

Arrivati a questo punto, non possiamo ridurre ulteriormente $\lambda y.MN$, ottenendo così un termine che, nel concreto, ci serve poco o niente. Ecco perché si preferisce sempre usare l’ordine normale nell’ambito della codifica di Church.

1.1 - Negazione logica

Avendo codificato i valori booleani $\text{TRUE}$ e $\text{FALSE}$ e un $\text{IF}$ che si comporta come ci aspetteremmo, ora possiamo creare condizioni booleane più elaborate provando a codificare anche gli operatori booleani.

Per esempio, una semplice negazione logica $\text{NOT}$ potrebbe funzionare così: preso in input un argomento $x$, se ($\text{IF}$) $x$ è vero allora restituisce falso (FALSE), altrimenti restituisce vero (TRUE):

$$\text{NOT}\stackrel{\text{def}}{=}\lambda x.\text{IF}x\text{FALSE}\text{TRUE}$$

Definizione: negazione logica nella codifica di Church

Nella codifica di Church, la negazione logica è codificata nel termine $\text{NOT}$ definito come segue:

$$\text{NOT}\stackrel{\text{def}}{=}\lambda x.\text{IF}x\text{FALSE}\text{TRUE}$$

Verifichiamo che semanticamente il $\text{NOT}$ si comporti come ci aspettiamo.

Verifica della correttezza semantica del $\text{NOT}$

1. La $\lambda$-espressione $\text{NOT}\text{TRUE}$ è convertibile in $\text{FALSE}$:

$$\text{NOT}\text{TRUE}\iff \text{FALSE}$$

2. La $\lambda$-espressione $\text{NOT}\text{FALSE}$ è convertibile in $\text{TRUE}$:

$$\text{NOT}\text{FALSE}\iff \text{TRUE}$$

1.2 - Congiunzione logica

Per la congiunzione logica $\text{AND}$, presi in input due argomenti $x$ e $y$, se ($\text{IF}$) $x$ è vero allora restituisce il valore di $y$ (perché da $y$ dipenderà se l’$\text{AND}$ è vero o falso), altrimenti (essendo già $x$ falso) restituisce il valore falso ($\text{FALSE}$):

$$\text{AND}\stackrel{\text{def}}{=}\lambda x.\lambda y.\text{IF}xy\text{FALSE}$$

Definizione: congiunzione logica nella codifica di Church

Nella codifica di Church, la congiunzione logica è codificata nel termine $\text{AND}$ definito come segue:

$$\text{AND}\stackrel{\text{def}}{=}\lambda x.\lambda y.\text{IF}xy\text{FALSE}$$

Verifica della correttezza semantica dell' $\text{AND}$

1. La $\lambda$-espressione $\text{AND}\text{TRUE}\text{TRUE}$ è convertibile in $\text{TRUE}$:

$$\text{AND}\text{TRUE}\text{TRUE}\iff \text{TRUE}$$

2. La $\lambda$-espressione $\text{AND}\text{TRUE}\text{FALSE}$ è convertibile in $\text{FALSE}$:

$$\text{AND}\text{TRUE}\text{FALSE}\iff \text{FALSE}$$

3. La $\lambda$-espressione $\text{AND}\text{FALSE}\text{TRUE}$ è convertibile in $\text{FALSE}$:

$$\text{AND}\text{FALSE}\text{TRUE}\iff \text{FALSE}$$

4. La $\lambda$-espressione $\text{AND}\text{FALSE}\text{FALSE}$ è convertibile in $\text{FALSE}$:

$$\text{AND}\text{FALSE}\text{FALSE}\iff \text{FALSE}$$

1.3 - Disgiunzione logica

Per la disgiunzione logica $\text{OR}$, presi in input due argomenti $x$ e $y$, se ($\text{IF}$) $x$ è vero allora restituisce vero ($\text{TRUE}$), altrimenti restituisce il valore di $y$ (perché da $y$ dipenderà se l’$\text{OR}$ è vero o falso):

$$\text{OR}\stackrel{\text{def}}{=}\lambda x.\lambda y.\text{IF}x\text{TRUE}y$$

Definizione: disgiunzione logica nella codifica di Church

Nella codifica di Church, la disgiunzione logica è codificata nel termine $\text{OR}$ definito come segue:

$$\text{OR}\stackrel{\text{def}}{=}\lambda x.\lambda y.\text{IF}x\text{TRUE}y$$

Verifica della correttezza semantica dell' $\text{OR}$

1. La $\lambda$-espressione $\text{OR}\text{TRUE}\text{TRUE}$ è convertibile in $\text{TRUE}$:

$$\text{OR}\text{TRUE}\text{TRUE}\iff \text{TRUE}$$

2. La $\lambda$-espressione $\text{OR}\text{TRUE}\text{FALSE}$ è convertibile in $\text{TRUE}$:

$$\text{OR}\text{TRUE}\text{FALSE}\iff \text{TRUE}$$

3. La $\lambda$-espressione $\text{OR}\text{FALSE}\text{TRUE}$ è convertibile in $\text{TRUE}$:

$$\text{OR}\text{FALSE}\text{TRUE}\iff \text{TRUE}$$

4. La $\lambda$-espressione $\text{OR}\text{FALSE}\text{FALSE}$ è convertibile in $\text{FALSE}$:

$$\text{OR}\text{FALSE}\text{FALSE}\iff \text{FALSE}$$

2 - Coppie di termini

Definizione: coppie nella codifica di Church

Nella codifica di Church, le coppie sono codificate nel termine $\text{PAIR}$ definito come segue:

$$\text{PAIR}\stackrel{\text{def}}{=}\lambda x.\lambda y.\lambda z.zxy$$

Il primo elemento della coppia è codificato nel termine $\text{FIRST}$ definito come segue:

$$\text{FIRST}\stackrel{\text{def}}{=}\lambda p.p\text{TRUE}$$

Il secondo elemento della coppia è codificato nel termine $\text{SECOND}$ definito come segue:

$$\text{SECOND}\stackrel{\text{def}}{=}\lambda p.p\text{FALSE}$$

Verifica della correttezza semantica di PAIR, FIRST e SECOND

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

Dati due termini $M,N\in \Lambda$:

1. La $\lambda$-espressione $\text{FIRST (PAIR}MN)$ è convertibile in $\text{M}$:

$$\text{FIRST (PAIR}MN)\iff M$$

2. La $\lambda$-espressione $\text{SECOND (PAIR}MN)$ è convertibile in $N$:

$$\text{SECOND (PAIR}MN)\iff N$$

3 - Numerali di Church

Può sembrare scontato, ma uno strumento importante in ogni linguaggio di programmazione sono i numeri, uno dei tipi di dato più utili in un linguaggio.

Nella sua codifica, Alonzo Church ha deciso di rappresentare ogni numero naturale $n$, detto numerale di Church e rappresentato come $\underline{n}$, come una funzione che mappa una qualsiasi funzione $f$ alla sua composizione per $n$ volte:

$$\underline{n}:f\mapsto f^n$$

Prima di andare avanti, definiamo un attimo più formalmente questa notazione “esponenziale” dell’applicazione.

Definizione: applicazione esponenziale

Sia $\Lambda$ l’insieme di termini del $\lambda$-calcolo. Dati due termini $M,N\in \Lambda$ e un $k\in \mathbb{N}$, l’applicazione esponenziale di $M$ per $k$ volte a $N$, denotata con $M^{k}N$, è definita nel seguente modo:

$$M^{k}N\stackrel{\text{def}}{=}\underset{k\text{ volte}}{\underbrace{M(M(\dots (MN)))}}$$

In particolare:

$$M^{0}N\stackrel{\text{def}}{=}N$$

Ritornando ai numerali, per un numero naturale $n$ qualsiasi, data una funzione $f$ e un parametro $x$, verrà restituito il parametro $x$ su cui viene applicata la funzione $f$ per $n$ volte:

$$f^{n}x=\underset{n\text{ volte}}{\underbrace{f(f(\dots (fx)))}}$$

Possiamo quindi formalmente definire i numerali di Church.

Definizione: numerale di Church

Nella codifica di Church, un numerale di Church $\underline{n}$ è un termine che codifica un numero naturale $n$ ed è definito come segue:

$$\underline{n}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{n}x$$

Ecco una breve tabella che riassume il comportamento dei numerali di Church:

Numerale di Church	Definizione del numerale	Utilizzo del numerale
$\underline{0}$	$\underline{0}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{0}x=\lambda f.\lambda x.x$	$\underline{0}fx=(\lambda f.\lambda x.x)fx=x$
$\underline{1}$	$\underline{1}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{1}x=\lambda f.\lambda x.fx$	$\underline{1}fx=(\lambda f.\lambda x.fx)fx=fx$
$\underline{2}$	$\underline{2}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{2}x=\lambda f.\lambda x.f(fx)$	$\underline{2}fx=(\lambda f.\lambda x.f(fx))fx=f(fx)$
$\underline{3}$	$\underline{3}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{3}x=\lambda f.\lambda x.f(f(fx))$	$\underline{3}fx=\lambda f.\lambda x.f(f(fx))fx=f(f(fx)$
$\dots$	$\dots$	$\dots$
$\underline{n}$	$\underline{n}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{n}x=\lambda f.\lambda x.\underset{n\text{ volte}}{\underbrace{f(f(\dots (f}}x)))$	$\underline{n}fx=\lambda f.\lambda x.\lambda f.\lambda x.\underset{n\text{ volte}}{\underbrace{f(f(\dots (f}}x)))=\underset{n\text{ volte}}{\underbrace{f(f(\dots (f}}x)))$

Osservazione: numerali di Church come codifica unaria dei numeri naturali

I numerali di Church costituiscono una codifica unaria dei numeri naturali, ossia rappresentano un numero n come n applicazioni di una funzione.

La codifica unaria ha il vantaggio della semplicità concettuale e della chiarezza semantica, ma non è efficiente nei casi pratici per numeri grandi, proprio perché ogni numero è “codificato” con un numero di applicazioni proporzionale al valore numerico.

3.1 - Successore naturale

Nell’ambito dei numerali di Church, introduciamo un operatore, $\text{SUCC}$, che ci permette di ottenere il successore di un certo numerale $\underline{n}$ (es. $\text{SUCC}\underline{3}=\underline{4}$).

Per far ciò, partiamo dalla definizione del numerale di Church ($\underline{n}\stackrel{\text{def}}{=}\lambda f.\lambda x.f^{n}x$): prendendo in input un numerale $a$ ($\lambda a$), gli applichiamo un’altra volta ancora $f$:

$$\lambda a.\lambda f.\lambda x.af(fx)$$

Definizione: successore naturale nella codifica di Church

Nella codifica di Church, il successore naturale è codificato nel termine $\text{SUCC}$ definito come segue:

$$\text{SUCC}\stackrel{\text{def}}{=}\lambda a.\lambda f.\lambda x.af(fx)$$

Ora verifichiamo che $\text{SUCC}$, per come l’abbiamo definito, si comporti come vorremmo.

Verifica della correttezza semantica di $\text{SUCC}$

Dato un numerale di Church $\underline{n}$, vale:

$$\text{SUCC}\underline{n}\iff \underline{n+1}$$

Dimostrazione della correttezza semantica di $\text{SUCC}$

SUCC n=($\Lambda$a.$\Lambda$f.$\Lambda$x.a f (f x)) ($\Lambda$f.$\Lambda$x.fn x)\toβ($\Lambda$f.$\Lambda$x.a f (f x))[($\Lambda$f.$\Lambda$x.fn x)/a]=$\Lambda$f.$\Lambda$x.$\Lambda$f.$\Lambda$x.fn x) f (f x)\toβ$\Lambda$f.$\Lambda$x.($\Lambda$x.fn x)[f/f] (f x)=$\Lambda$f.$\Lambda$x.($\Lambda$x.fn x) (f x)\toβ$\Lambda$f.$\Lambda$x.(fn x)[(f x)/x]=$\Lambda$f.$\Lambda$x.fn (f x)=$\Lambda$f.$\Lambda$x.fn+1 x=SUCC n+1definizione di SUCC e del numerale di Church n$\beta$-riduzionesostituzione$\beta$-riduzionesostituzione$\beta$-riduzionesostituzionedefinizione dell’applicazione esponenzialedefinizione del numerale di Church

3.2 - Predecessore naturale

Vogliamo ottenere una funzione PRED tale che:

PRED n=n-1

con PRED 0=0.

Prendendo ispirazione da SUCC, definito come

SUCC\overset{\text{def}}{=}$\Lambda$a.$\Lambda$f.$\Lambda$x.a f (f x)

possiamo notare che, per calcolare il successoreLINK di un numero naturale, basta aggiungergli un’applicazione. Viceversa, per calcolare il suo predecessoreLINK, dovremo togliere un’applicazione.

Tuttavia, nel $\lambda$-calcolo, non è possibile togliere applicazioni a una funzione di Church. Occorre quindi un espediente funzionale.

L’idea di Church è questa: quando applichiamo una funzione f per n volte, vogliamo tener traccia non solo dell’ultimo risultato, ma anche del penultimo. Se riuscissimo a costruire una sequenza di coppie

(0,0),(0,1),(1,2),(2,3),…,(n-2,n-1),(n-1,n)

alla fine potremmo restituire il primo elemento della coppia finale per ottenere n-1.

Perciò, costruiamo una funzione “iteratrice” next(x) che parte da x=(0,0) e ad ogni passo aggiorna la coppia in questo modo:

next(x)=(x1second(x),x2succ(second(x)))

Così facendo, la funzione next(x) funzionerà nel seguente modo:

x	x1=second(x)	x2=succ(second(x))	next(x)=(x1,x2)
(0,0)	second((0,0))=0	succ(second((0,0)))=succ(0)=1	next((0,0))=(0,1)
(0,1)	second((0,1))=1	succ(second((0,1)))=succ(1)=2	next((0,1))=(1,2)
(1,2)	second((1,2))=2	succ(second((1,2)))=succ(2)=3	next((1,2))=(2,3)
(2,3)	second((2,3))=3	succ(second((2,3)))=succ(3)=4	next((2,3))=(3,4)
…	…	…	…
(n-2,n-1)	second((n-2,n-1))=n-1	succ(second((n-2,n-1)))=succ(n-1)=n	next((n-2,n-1))=(n-1,n)
(n-1,n)	second((n-1,n))=n	succ(second((n-1,n)))=succ(n)=n+1	next((n-1,n))=(n,n+1)

Osserviamo che dopo n passi di next(x), la prima componente (x1) è esattamente n-1 (per n>0).

Nel $\lambda$-calcolo traduciamo questa funzione next(x) come:

NEXT\overset{\text{def}}{=}$\Lambda$p.PAIR (SECOND p) (SUCC (SECOND p))

La nostra $\lambda$-espressione PRED dovrà quindi prendere la prima componente (FIRST) della coppia generata all’n-esima iterazione di NEXT:

PRED\overset{\text{def}}{=}$\Lambda$n.FIRST (n NEXT (PAIR 0 0))

Definizione: predecessore naturale nella codifica di Church

Nella codifica di Church, il predecessore naturale è codificato nel termine PRED definito come segue:

PRED\overset{\text{def}}{=}$\Lambda$n.FIRST (n NEXT (PAIR 0 0))

dove

NEXT\overset{\text{def}}{=}$\Lambda$p.PAIR (SECOND p) (SUCC (SECOND p))

Verifica della correttezza semantica di PRED

Dato un numerale di Church n:

1. Il successore della coppia (n-1,n) è (n,n+1):

NEXT (PAIR n-1 n)⇔PAIR n n+1

2. Il predecessore di 0 è 0 e il predecessore di n è n-1:

PRED n⇔{0n-1n=0n>0

3.3 - Addizione

Definizione: addizione nella codifica di Church

Nella codifica di Church, l’addizione è codificata nel termine ADD definito come segue:

ADD\overset{\text{def}}{=}$\Lambda$a.$\Lambda$b.b SUCC a

Verifica della correttezza semantica di ADD

Dati due numerali di Church m e n, vale:

ADD m n⇔m+n

Dimostrazione della correttezza semantica di ADD

ADD m n=($\Lambda$a.$\Lambda$b.b SUCC a) m n\toβ($\Lambda$b.b SUCC a)[m/a] n=($\Lambda$b.b SUCC m) n\toβ(b SUCC m)[n/b]=n SUCC m=($\Lambda$f.$\Lambda$x.fn x) SUCC m\toβ($\Lambda$x.fn x)[SUCC/f] m=($\Lambda$x.SUCCn x) m\toβ(SUCCn x)[m/x]=SUCCn m=n volteSUCC (SUCC (… (SUCC m)))⇔n volte(((m+1)+1)…)+1=m+ndefinizione di ADD$\beta$-riduzionesostituzione$\beta$-riduzionesosituzionedefinizione dei numerali di Church$\beta$-riduzionesostituzione$\beta$-riduzionesostituzioneapplicazione esponenzialesemantica di SUCCaddizione

3.4 - Moltiplicazione

Definizione: moltiplicazione nella codifica di Church

Nella codifica di Church, la moltiplicazione è codificata nel termine MUL definito come segue:

MUL\overset{\text{def}}{=}$\Lambda$a.$\Lambda$b.b (ADD a) 0

3.5 - Esponenziazione

Definizione: esponenziazione nella codifica di Church

Nella codifica di Church, l’esponenziazione è codificata nel termine EXP definito come segue:

EXP\overset{\text{def}}{=}$\Lambda$a.$\Lambda$b.b (MUL a) 1

3.6 - Test per zero

Definizione: test per zero nella codifica di Church

Nella codifica di Church, il test per zero è codificato nel termine ISZERO definito come segue:

ISZERO\overset{\text{def}}{=}$\Lambda$a.a ($\Lambda$x.FALSE) TRUE

Verifica della correttezza semantica di ISZERO

Dato un numerale di Church n, se n=0 allora ISZERO n restituisce TRUE, altrimenti FALSE:

ISZERO n⇔{TRUEFALSEn=0n=0

4 - Punti fissi e funzioni ricorsive

Ora che abbiamo le operazioni aritmetiche per calcolare con i numerali di Church, possiamo cimentarci nella codifica di una prima funzione ricorsiva nel $\lambda$-calcolo: il fattoriale.

Il fattoriale di un numero naturale n, tradizionalmente, nella sua definizione ricorsiva si esprime come il n moltiplicato per il fattoriale del suo predecessore n-1 (con il fattoriale di 0 uguale a 1):

n!={1n∗(n-1)!n=0n>0

Come primo tentativo, potremmo tradurre questa definizione ricorsiva del fattoriale nella codifica di Church così:

FACT\overset{\text{def}}{=}$\Lambda$a.IF (ISZERO a) 1 (MUL a (FACT (PRED a)))

Tuttavia, ciò non ci soddisfa perché il termine FACT compare pure a destra. Proviamo però ad astrarre ulteriormente questo termine passandogli il FACT nella sua definizione come argomento:

FACT\overset{\text{def}}{=}($\Lambda$f.$\Lambda$a.IF (ISZERO a) 1 (MUL a (f (PRED a)))) FACT

(Ovviamente possiamo notare che, tramite un semplice passaggio di $\beta$-riduzione, sostituiamo f con FACT e torniamo alla situazione iniziale.)

Assegniamo momentaneamente al termine “ausiliare” AUX tutto quell’ambaradan a cui va poi applicato ricorsivamente FACT:

AUX\overset{\text{def}}{=}$\Lambda$f.$\Lambda$a.IF (ISZERO a) 1 (MUL a (f (PRED a)))

In qualche modo, una definizione “accettabile” del fattoriale che vogliamo ottenere avrà una forma del tipo:

FACT\overset{\text{def}}{=}AUX AUX AUX …

Ma a noi serve avere una definizione finita per poter operare con questo termine e ottenere il risultato che vogliamo. È per questo che ci torna utile il concetto di punto fisso di una funzione che ci permetterà di definirla in maniera finita.

Non preoccuparti, a breve sarà tutto più chiaro, ma intanto beccati questa definizione di un punto fisso nel $\lambda$-calcolo espresso mediante questo particolare combinatore scoperto da Haskell Curry: il combinatore di punto fisso.

Definizione: combinatore di punto fisso Y

Il combinatore di punto fisso (anche detto combinatore di Curry perché scoperto da Haskell Curry) Y è un combinatore definito nel seguente modo:

Y\overset{\text{def}}{=}$\Lambda$f.($\Lambda$x.f(x x)) ($\Lambda$x.f(x x))

Possiamo dimostrare che questo combinatore di punto fisso Y si comporta semanticamente proprio come un punto fisso.

Verifica della correttezza semantica del combinatore di punto fisso Y

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

Dato un termine M\in$\Lambda$, vale:

Y M=M (Y M)

4.1 - Fattoriale

Il combinatore di punto fisso Y è uno strumento molto potente: ci permette, infatti, di implementare il concetto di ricorsione in un linguaggio, quello del $\lambda$-calcolo, che formalmente non ce l’ha.

Ciò infatti è possibile perché, ogni termine M a cui viene applicato il combinatore di punto fisso Y, diventa a sua volta l’argomento della $\lambda$-espressione di partenza:

Y M=M (Y M)=M (M (Y M))=M (M (M (Y M)))=…

Riprendendo quel termine “ausiliare” di prima, che abbiamo espresso come

AUX\overset{\text{def}}{=}$\Lambda$f.$\Lambda$a.IF (ISZERO a) 1 (MUL a (f (PRED a)))

possiamo renderci ora conto che, passandogli come argomento al posto della f il combinatore di punto fisso Y, ci aiuta a definire in maniera finita la funzione fattoriale nel $\lambda$-calcolo.

Definizione: fattoriale nella codifica di Church

Nella codifica di Church, il fattoriale è codificato nel termine FACT definito come segue:

FACT\overset{\text{def}}{=}($\Lambda$f.$\Lambda$a.IF (ISZERO a) 1 (MUL a (f (PRED a)))) Y

Sì, ma siamo sicuri che quella che abbiamo appena scritto non sia una cazzata colossale e che effettivamente la ricorsione funzioni? Verifichiamolo.

Verifica della ricorsione nel fattoriale nella codifica di Church

Il termine FACT è convertibile nel seguente modo:

FACT⇔$\Lambda$a.IF (ISZERO a) 1 (MUL a (FACT (PRED a)))

---

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:
      • Programmare nel $\lambda$-calcolo.
  • 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, archiviato sulla Wayback Machine in data 25 novembre 2025.
• 🌐 Simply typed lambda calculus su Wikipedia in lingua inglese, archiviato sulla Wayback Machine in data 25 novembre 2025.