Lambda calcolo

Il lambda calcolo o λ-calcolo è un sistema formale definito nel 1936 dal matematico Alonzo Church, sviluppato per analizzare formalmente le funzioni e il loro calcolo. Le prime sono espresse per mezzo di un linguaggio formale, che stabilisce quali siano le regole per formare un termine, il secondo con un sistema di riscrittura, che definisce come i termini possano essere ridotti e semplificati.

Descrizione

La combinazione di semplicità ed espressività ha reso il lambda calcolo uno strumento frequente in diversi campi scientifici:

Nell'ambito della matematica e nell'informatica, in particolare nella teoria della calcolabilità fu sviluppato per lo studio delle funzioni ricorsive come effettivamente calcolabili.
Nell'informatica e nella teoria dei linguaggi di programmazione è il principale prototipo dei linguaggi di programmazione di tipo funzionale e della ricorsione.
Nella teoria della dimostrazione, il lambda calcolo tipato è uno dei più usati sistemi formali per la rappresentazione delle dimostrazioni, grazie alla corrispondenza Curry-Howard che mette in relazione dimostrazioni con termini e tipi con formule logiche.
Nella semantica modellistica (branca della linguistica) il lambda calcolo è il formalismo impiegato per la descrizione della composizione del significato all'interno di una frase.

Termini

Si definisce termine del lambda calcolo o, più brevemente, lambda termine o lambda espressione qualunque stringa ben formata a partire dalla seguente grammatica, in forma Backus-Naur:

$T\quad ::=\quad V\quad |\quad \lambda V.T\quad |\quad (T\quad T)$

dove la metavariabile $V$ denota una variabile appartenente a un insieme infinito numerabile di variabili.

Parafrasando la definizione formale, un lambda termine può essere, rispettivamente, un nome di variabile, l'astrazione di un termine rispetto ad una variabile, o l'applicazione di un termine come argomento (o parametro attuale) di un altro.

Variabili

Dato un generico lambda termine $M$ , si definisce $\mathrm {Var} (M)$ l'insieme che contiene tutte le variabili menzionate in $M$ . Tra queste si distinguono due partizioni: l'insieme delle variabili libere, scritto $\mathrm {Libere} (M)$ , e l'insieme delle variabili legate, indicate con $\mathrm {Legate} (M)$ . L'insieme delle variabili libere è definito ricorsivamente come segue:

$\mathrm {Libere} (x)=\{x\}$ ;
$\mathrm {Libere} (\lambda x.M)=\mathrm {Libere} (M)\setminus \{x\}$ ;
$\mathrm {Libere} (MN)=\mathrm {Libere} (M)\cup \mathrm {Libere} (N)$ .

L'insieme delle variabili legate è quindi ottenibile per differenza:

\mathrm {Legate} (M)=Var(M)\setminus \mathrm {Libere} (M)

.

Il punto 2 della definizione implica che il costrutto sintattico dell'astrazione è un legatore di variabile: se $x\in {\textrm {Libere}}(M)$ , allora $x\in {\textrm {Legate}}(\lambda x.M)$ .

Un nome di variabile si dice fresco, relativamente ad un termine, se esso non è compreso tra i nomi di variabile di quello stesso termine.

Alcuni esempi che si ottengono semplicemente applicando le definizioni date sopra:

{\textrm {Var}}(\lambda z.\lambda x.(xy))=\{z,x,y\}

;

{\textrm {Libere}}(\lambda z.\lambda x.(xy))=\{y\}

;

{\textrm {Legate}}(\lambda z.\lambda x.(xy))=\{x,z\}

;

Regole di riscrittura

Sostituzione

Una sostituzione è il rimpiazzo di tutte le occorrenze di un sotto-termine con un altro, all'interno di un terzo termine che rappresenta il contesto della sostituzione stessa. Si indica con $M[N/v]$ la sostituzione del termine $N$ al posto di $v$ all'interno del termine $M$ : ogni occorrenza libera della variabile $v$ in $M$ è sostituita da $N$ . Un semplice esempio di sostituzione è il seguente:

(zx)[\lambda x.x/z]\equiv ((\lambda x.x)x)

.

Una definizione ricorsiva dell'algoritmo di sostituzione è la successiva:

$x[N/x]\equiv N$ ;
$y[N/x]\equiv y$ , se $x\neq y$ ;
$(\lambda y.M)[N/y]\equiv \lambda y.M$ ;
$(\lambda y.M)[N/x]\equiv \lambda y.(M[N/x])$ , se $y\neq x$ e $y\notin FV(N)$ ;
$(\lambda y.M)[N/x]\equiv \lambda z.(M[z/y][N/x])$ , se $y\neq x$ , $y\in FV(N)$ , e $z$ è un nome fresco;
$(M_{1}M_{2})[N/x]\equiv (M_{1}[N/x])(M_{2}[N/x])$ .

Alcuni esempi di sostituzione:

(zx)[(\lambda x.x)/z]\equiv ((\lambda x.x)x)

;

(\lambda z.(zx))[(\lambda x.x)/z]\equiv (\lambda z.(zx))

;

(\lambda z.(zx))[(zx)/x]\equiv \lambda w.((zx)[w/z][(zx)/x])\equiv \lambda w.((wx)[(zx)/x])\equiv \lambda w.w(zx)

, dove

w

è un nome fresco.

I controlli di occorrenza al punto 4 e 5, sono necessari per evitare un fenomeno sgradito chiamato cattura di variabile. Senza tali controlli, l'operazione di sostituzione porterebbe una variabile libera di un termine, a diventare legata per effetto della sostituzione stessa, il che risulta essere anche intuitivamente scorretto.

Alfa conversione

$\lambda x.M\rightarrow _{\alpha }\lambda y.(M[y/x])$ .

L'alfa conversione si applica ai termini che sono astrazioni. Data un'astrazione, è possibile riscriverla sostituendo la variabile astratta ( $x$ ) con un'altra ( $y$ ), a patto che, nell'intero sotto-termine, al posto di ogni occorrenza della prima, si scriva la seconda.

La regola di alfa conversione non si occupa di fare alcuna distinzione fra occorrenze libere o legate delle variabili, dato che l'operazione di sostituzione si occupa già di fare ciò. Alcuni esempi di alfa conversione:

\lambda x.(xy)\rightarrow _{\alpha }\lambda z.(zy)

\lambda x.(x(\lambda z.(zw)))\rightarrow _{\alpha }\lambda z.(z(\lambda z.(zw)))

Beta riduzione

La beta riduzione è la più importante regola di riscrittura del lambda calcolo, visto che implementa il passo di computazione. La sua prescrizione è definita come segue, dove l'eventuale contesto presente è omesso:

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

.

(Sostituire N, alle occorrenze delle variabili legate, in M)

La regola ha come oggetto un'applicazione di una lambda astrazione nella forma $\lambda x.M$ su un secondo termine $N$ . La configurazione sintattica riducibile è appunto chiamata redex, contrazione della inglese "red-ucible ex-pression", a sua volta raramente ricalcato in italiano come "redesso", il suo risultato è chiamato ridotto.

Proseguendo l'analogia con i linguaggi di programmazione, la regola riguarda una funzione applicata ad un argomento. Essa corrisponde pertanto ad un passo di calcolo, che restituisce il corpo della funzione $M$ dove il parametro attuale (effettivo) $N$ viene sostituito al parametro formale $x$ della funzione. In questo contesto dunque la sostituzione rappresenta proprio il passaggio del parametro.

Alcuni esempi di beta riduzione sono:

(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda y.y)(\lambda y.y)\rightarrow _{\beta }\lambda y.y

(\lambda x.\lambda y.(xy))(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }(\lambda x.(xx))(\lambda y.y)\rightarrow _{\beta }\dots \rightarrow _{\beta }\lambda y.y

Eta conversione

$\lambda x.(Mx)\rightarrow _{\eta }M$ , se $x\notin FV(M)$ .

Intuitivamente, l'importanza di questa regola risiede nel fatto che consente di dichiarare identici due lambda termini sulla base del principio che se essi si comportano allo stesso modo (una volta applicati ad un parametro) essi devono quindi essere considerati, per l'appunto, identici.

Dire che $\lambda x.(Mx)$ e $M$ si comportano allo stesso modo, equivale a dire che per ogni $N$ : $(\lambda x.(Mx))N\rightarrow _{\beta }(Mx)[N/x]\equiv (MN)$ . In altre parole la eta-conversione assiomatizza la dimostrabilità dell'uguaglianza nel $\lambda$ -calcolo estensionale^[1].

Termini equivalenti

Le regole di conversione possono essere estese a vere e proprie relazioni di equivalenza, assumendo di poter riscrivere nel senso delle frecce appena definite (da sinistra verso destra) e che valgano anche le riscritture nella direzione opposta (da destra verso sinistra, quindi). Formalmente, si applicano le seguenti relazioni:

$\lambda x.M\Leftrightarrow _{\alpha }\lambda y.(M[y/x])$ ,
$\lambda x.(Mx)\Leftrightarrow _{\eta }M$ , se $x\notin FV(M)$ .

Le due doppie implicazioni sono chiamate, rispettivamente, alfa-equivalenza e eta-equivalenza. Due termini t ed s si dicono alfa-eta-equivalenti quando è soddifatta la relazione:

$t\Leftrightarrow _{x_{1}}t_{1}\Leftrightarrow _{x_{2}}t_{2}\Leftrightarrow _{x_{3}}\dots \Leftrightarrow _{x_{n}}t_{n}\Leftrightarrow _{x_{n+1}}s\qquad \forall i.x_{i}\in \{\alpha ,\eta \}$ .

In altre parole, due termini sono alfa-eta-equivalenti se esiste una catena finita di riscritture che impieghi solo le regole di alfa-equivalenza e di eta-equivalenza.

Codifiche

Attraverso il λ-calcolo sono state formulate diverse codifiche. Alcuni esempi sono la codifica di Church, e quella di Mogensen-Scott. Esistono anche codifiche che usano il lambda calcolo tipato, come il Sistema F.

Numerazione

La numerazione di Church può esprimere l'insieme dei numeri naturali $\mathbb {N}$ attraverso gli assiomi di Peano. Ogni numero viene espresso come il successivo del precedente, mentre lo zero è l'unico che non è il successivo di alcun numero.

$n:=\lambda sz.s_{0}\circ s_{1}\circ \cdots \circ s_{n}(z)$

Tutti i numeri appartenenti all'insieme dei naturali possono essere espressi analogamente.

$\mathbb {N} \ni {\begin{cases}0:=\lambda sz.z\\1:=\lambda sz.s(z)\\2:=\lambda sz.s(s(z))\\3:=\lambda sz.s(s(s(z)))\\4:=\lambda sz.s(s(s(s(z))))\\\cdots \end{cases}}$

Operazioni aritmetiche

Relativamente alla precedente numerazione dei numeri naturali è possibile esprimere alcune computazioni elencate di seguito.

Funzione	Definizione aritmetica	Definizione secondo Church
Successore	$n+1$	$\lambda wxy.x(wxy)$
Addizione	$x+y$	$\lambda xyfg.xf(yfg)\equiv \lambda xy.x\;SUC\;y$
Moltiplicazione	$x*y$	$\lambda xyf.x(yf)$
Potenza	$x^{y}$	$\lambda xy.y(x)$

Esempi

$SUC\;0=\lambda wxy.x(wxy)(\lambda sz.z)=\lambda xy.x((\lambda sz.z)xy)=\lambda xy.x((\lambda z.z)y)=\lambda xy.x(y)=1$

$1\;ADD\;2=\lambda fg.(\lambda sz.s(z))f((\lambda sz.s(s(z)))fg)=\lambda fg.(\lambda z.f(z))(f(f(g))=\lambda fg.f(f(f(g)))=3$

$1\;MUL\;3=(\lambda sz.s(z))(\lambda xyf.x(yf))(\lambda sz.s(s(s(z))))=\lambda f.(\lambda sz.s(z))((\lambda z.f(f(f(z)))))=\lambda f.\lambda z.f(f(f(z)))=3$

Logica di Boole

La logica booleana o algebra di Boole, è una formalizzazione della logica che si basa su due valori, cioè vero e falso, esprimibili come di seguito.

$V:=\lambda vf.v=\lambda v.\lambda f.v$

$F:=\lambda vf.f=\lambda v.\lambda f.f$

Da notarsi che la funzione $F$ rappresenta sia il valore zero che falso.

Operazioni logiche

Di seguito, verranno espresse alcune delle più semplici operazioni relative alla logica booleana.

Funzione Logica	Simbolo	Definizione
E (AND)	$\land$	$\lambda p.\lambda p'.p\,p'p$
O (OR)	$\lor$	$\lambda p.\lambda p'.p\,p\,p'$
NON (NOT)	$\neg$	$\lambda p.p\,F\,V$

Esempi

$V\;AND\;F=(\lambda vf.v)(\lambda pp'.p\,p'p)(\lambda vf.f)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=\lambda f.\lambda f.f=\lambda vf.f=Falso$

$V\;OR\;V=(\lambda vf.v)(\lambda pp'.p\,p\,p')(\lambda vf.v)=(\lambda vf.v)(\lambda vf.v)(\lambda vf.v)=\lambda vf.v=Vero$

$NOT\;V=(\lambda p.p(\lambda vf.f)(\lambda vf.v))(\lambda vf.v)=(\lambda vf.v)(\lambda vf.f)(\lambda vf.v)=(\lambda f.\lambda vf.f)(\lambda vf.v)=\lambda vf.f=Falso$

Forme normali

Un termine del lambda calcolo si trova in forma normale se esso non è riscrivibile per mezzo della regola di beta riduzione. Se la beta riduzione rappresenta un passo di computazione di un lambda termine che descrive un programma, allora la sua chiusura transitiva ne rappresenta una qualsiasi computazione. Quando una riduzione è finita e massimale, il termine ridotto in forma normale rappresenta il risultato finale della computazione.

Per esempio, si supponga di arricchire il calcolo aggiungendovi i numeri naturali (semplicemente denotati come $1,2,\ldots$ ) e l'operazione di addizione binaria su di essi (scritta in forma prefissa come $(+xy)$ ), entrambi peraltro direttamente codificabili come lambda termini. Si consideri ora un termine che somma $2$ al suo argomento, ovvero $(\lambda x.((+\ 2\ x))$ e si usi come argomento il valore $5$ . Tale applicazione converge a forma normale $7$ , infatti: $(\lambda x.((+\ 2\ x))5)\rightarrow _{\beta }(+\ 2\ 5)\rightarrow _{\beta }7\not \rightarrow _{\beta }$ .

Non tutti i lambda termini hanno forma normale e la beta riduzione non ha sempre lunghezza finita. Questo fenomeno rappresenta il fatto che il calcolo di un programma può procedere indefinitamente e divergere e permette di rappresentare funzioni parziali.

L'esempio classico di divergenza è costruibile a partire dal termine duplicatore $\delta =_{def}\lambda x.(xx)$ , che non fa altro che prendere un termine e restituirne due copie, l'una applicata all'altra. È possibile dunque definire il termine $\omega =_{def}(\delta \delta )$ , e notare che esso riduce a se stesso $\omega \rightarrow _{\beta }\omega \rightarrow _{\beta }\dots$ .

Note

^ Barendregt, The Lambda Calculus

Bibliografia

(EN) Henk P. Barendregt, The Lambda Calculus, its Syntax and Semantics - Studies in Logic Volume 40, College Publication, London, 2012. ISBN 978-1-84890-066-0. Questo libro è una fonte enciclopedica per quanto riguarda il lambda calcolo non tipato. In esso sono presenti moltissime definizioni e dimostrazioni, ma pochissime spiegazioni sul significato e sull'interpretazione dei risultati presentati.
Maurizio Gabbrielli e Simone Martini, Linguaggi di programmazione: principi e paradigmi, 2ª edizione, Milano, McGraw-Hill, 2011. ISBN 978-88-386-6573-8.
(EN) Jean-Yves Girard, Proofs and Types, Paul Taylor and Yves Lafont, Cambridge University Press, 2003 [1989], ISBN 0-521-37181-3. URL consultato il 24 marzo 2014. Libro riguardante il lambda calcolo tipato e quello del secondo ordine.