Lambda calcolo

Da Wikipedia, l'enciclopedia libera.
La lettera lambda minuscola, undicesima dell'alfabeto greco è il simbolo del lambda calcolo.

Il lambda calcolo o \lambda-calcolo è un sistema formale definito 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.

La combinazione di semplicità ed espressività ha reso il lambda calcolo uno strumento frequente in diversi campi scientifici. Nell'ambito della matematica e nella filosofia, in particolare nella Teoria della calcolabilità fu sviluppato per lo studio delle funzioni ricorsive come effettivamente calcolabili, visto che il lambda calcolo è un formalismo di calcolo universale, come la Macchina di Turing. Nell'informatica è 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.

Di seguito vedremo una descrizione del calcolo che procederà per gradi: dopo aver definito la sintassi dei termini, introdurremo le regole del calcolo ed i suoi risultati.

Termini[modifica | modifica wikitesto]

Chiamiamo 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 un insieme infinito numerabile di nomi di variabile, o 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) di un altro.

Variabili[modifica | modifica wikitesto]

Dato un generico lambda termine M, chiamiamo \mathrm{Var}(M) l'insieme che contiene tutte le variabili menzionate in M. Tra queste distinguiamo 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:

  1. \mathrm{Libere}(x) = \{ x \};
  2. \mathrm{Libere}(\lambda x . M) = \mathrm{Libere}(M) \setminus \{x\};
  3. \mathrm{Libere}(M N) = \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 . (x y)) = \{z, x, y \};
\textrm{Libere}(\lambda z . \lambda x . (x y)) = \{ y \};
\textrm{Legate}(\lambda z . \lambda x . (x y)) = \{ x , z \} ;

Regole di riscrittura[modifica | modifica wikitesto]

Sostituzione[modifica | modifica wikitesto]

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. Indichiamo 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 è rimpiazzata da N. Un semplice esempio di sostituzione è il seguente:

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

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

  1. x [N / x] \equiv N;
  2. y [N / x] \equiv y, se x \neq y;
  3. (\lambda y . M)[N / y] \equiv \lambda y . M;
  4. (\lambda y . M)[N / x] \equiv \lambda y . (M [N / x] ), se y \neq x e y \notin FV(N);
  5. (\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;
  6. (M_1 M_2)[N / x] \equiv (M_1[N / x])(M_2[N / x]).

Alcuni esempi di sostituzione:

(z x)[(\lambda x . x) / z] \equiv ((\lambda x . x) x);
(\lambda z . (z x))[(\lambda x . x) / z] \equiv (\lambda z . (z x));
(\lambda z . (z x))[(z x)/ x] \equiv \lambda w . ((z x)[w / z][(z x) / x]) \equiv \lambda w . ((w x)[(z x) / x]) \equiv \lambda w . w (z x), 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. Se non eseguissimo tali controlli, l'operazione di sostituzione porterebbe una variabile libera di un termine, ad essere legata, dopo la sostituzione stessa, il che risulta essere anche intuitivamente scorretto.

Alfa conversione[modifica | modifica wikitesto]

\lambda x . M \rightarrow_{\alpha} \lambda y . (M[y / x]).

L'alfa conversione si applica ai termini che sono astrazioni. Presa un'astrazione, possiamo riscriverla sostituendo la variabile astratta (x) con un'altra (y), a patto che, nell'intero sotto-termine, al posto di ogni occorrenza della prima, noi andiamo a scrivere 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 . (x y) \rightarrow_{\alpha} \lambda z . (z y)
\lambda x . (x (\lambda z . (z w))) \rightarrow_{\alpha} \lambda z . (z (\lambda z . (z w)))

Beta riduzione[modifica | modifica wikitesto]

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

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.

Vediamo alcuni esempi di beta riduzione:

(\lambda x . (x x))(\lambda y . y) \rightarrow_{\beta} (\lambda y . y)(\lambda y . y) \rightarrow_{\beta} \lambda y . y
(\lambda x . \lambda y . (x y))(\lambda x . (x x))(\lambda y . y) \rightarrow_{\beta} (\lambda x . (x x))(\lambda y . y) \rightarrow_{\beta} \dots
\rightarrow_{\beta} \lambda y . y

Eta conversione[modifica | modifica wikitesto]

\lambda x . (M x) \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.

Quando diciamo che \lambda x . (M x) e M si comportano allo stesso modo, intendiamo dire che per ogni N: (\lambda x . (M x)) N \rightarrow_{\beta} (M x)[N / x] \rightarrow_{\beta} (M N). In altre parole possiamo anche dire che la [eta-conversione] assiomatizza la dimostrabilità dell'uguaglianza nel \lambda-calcolo estensionale (Barendregt, The Lambda Calculus).

Termini equivalenti[modifica | modifica wikitesto]

Ora estendiamo le regole di conversione a vere e proprie relazioni di equivalenza, ovvero assumiamo di poter riscrivere nel senso delle frecce appena definite (da sinistra verso destra) ed assumiamo che valgano anche le riscritture nella direzione opposta (da destra verso sinistra, quindi). In altre parole, diciamo che vale quanto segue:

  • \lambda x . M \Leftrightarrow_{\alpha} \lambda y . (M[y / x]),
  • \lambda x . (M x) \Leftrightarrow_{\eta} M, se x \notin FV(M).

Le due doppie implicazioni sono chiamate, rispettivamente, Alfa-equivalenza e Eta-equivalenza. Diciamo che due termini t ed s sono Alfa-Eta-equivalenti se vale che:

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

dove \forall i . x_i \in \{ \alpha, \eta \}. In altre parole, essi sono Alfa-Eta-equivalenti se esiste una catena finita di riscritture che impieghi solo le regole di Alfa-equivalenza e di Eta-equivalenza.

Forme normali[modifica | modifica wikitesto]

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, supponiamo 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 (+ x y)), entrambi peraltro direttamente codificabili come lambda termini. Consideriamo ora un termine che somma 2 al suo argomento, ovvero (\lambda x . ((+\ 2\ x)), e passiamogli 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 . (x x), che non fa altro che prendere un termine e restituirne due copie, l'una applicata all'altra. Possiamo dunque definire il termine \omega =_{def} (\delta \delta), e notare che esso riduce a se stesso \omega \rightarrow_{\beta} \omega \rightarrow_{\beta} \dots.

Bibliografia[modifica | modifica wikitesto]

  • (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 [1989], 2003, ISBN 0-521-37181-3. URL consultato il 24 marzo 2014. Libro riguardante il lambda calcolo tipato e quello del secondo ordine.

Voci correlate[modifica | modifica wikitesto]