Codifica di Church

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.

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.

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}$$

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}$$

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

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

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

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

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

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

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}$$

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

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

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

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

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

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

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$$

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

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

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}$	1​\overset{\text{def}}{=}$\Lambda$f.$\Lambda$x.f1 x=$\Lambda$f.$\Lambda$x.f x	1​ f x=($\Lambda$f.$\Lambda$x.f x) f x=f x
$\underline{2}$	2​\overset{\text{def}}{=}$\Lambda$f.$\Lambda$x.f2 x=$\Lambda$f.$\Lambda$x.f (f x)	2​ f x=($\Lambda$f.$\Lambda$x.f (f x)) f x=f (f x)
$\underline{3}$	3​\overset{\text{def}}{=}$\Lambda$f.$\Lambda$x.f3 x=$\Lambda$f.$\Lambda$x.f (f (f x))	3​ f x=$\Lambda$f.$\Lambda$x.f (f (f x)) f x=f (f (f x)
$\dots$	$\dots$	$\dots$
$\underline{n}$	n​\overset{\text{def}}{=}$\Lambda$f.$\Lambda$x.fn x=$\Lambda$f.$\Lambda$x.n voltef (f (… (f​​ (x))))	n​ f x=$\Lambda$f.$\Lambda$x.n voltef (f (… (f​​ (x)))) f n=n voltef (f (… (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.

Successore naturale

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

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

$\Lambda$a.$\Lambda$f.$\Lambda$x.a f (f x)

Definizione: successore naturale nella codifica di Church

Nella codifica di Church, il successore naturale è codificato nel termine SUCC definito come segue:

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

Ora verifichiamo che SUCC, per come l’abbiamo definito, si comporti come vorremmo.

Verifica della correttezza semantica di SUCC

Dato un numerale di Church n​, vale:

SUCC n​⇔n+1​

Dimostrazione della correttezza semantica di SUCC

SUCC n​​=($\Lambda$a.$\Lambda$f.$\Lambda$x.a f (f x)) ($\Lambda$f.$\Lambda$x.fn x)→β​($\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)→β​$\Lambda$f.$\Lambda$x.($\Lambda$x.fn x)[f/f] (f x)=$\Lambda$f.$\Lambda$x.($\Lambda$x.fn x) (f x)→β​$\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+1​​definizione di SUCC e del numerale di Church n​$\beta$-riduzionesostituzione$\beta$-riduzionesostituzione$\beta$-riduzionesostituzionedefinizione dell’applicazione esponenzialedefinizione del numerale di Church​

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)=(x1​second(x)​​,x2​succ(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​⇔{0​n−1​​n=0n>0​

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​→β​($\Lambda$b.b SUCC a)[m​/a] n​=($\Lambda$b.b SUCC m​) n​→β​(b SUCC m​)[n​/b]=n​ SUCC m​=($\Lambda$f.$\Lambda$x.fn x) SUCC m​→β​($\Lambda$x.fn x)[SUCC/f] m​=($\Lambda$x.SUCCn x) m​→β​(SUCCn x)[m​/x]=SUCCn m​=n volteSUCC (SUCC (… (SUCC​​ m​)))⇔n volte(((m+1)+1)…)+1​​​=m+n​​definizione di ADD$\beta$-riduzionesostituzione$\beta$-riduzionesosituzionedefinizione dei numerali di Church$\beta$-riduzionesostituzione$\beta$-riduzionesostituzioneapplicazione esponenzialesemantica di SUCCaddizione​

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​

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​

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​⇔{TRUEFALSE​n=0n=0​

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∈$\Lambda$, vale:

Y M=M (Y M)

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, 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.