Lambda calcolo

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

Il lambda calcolo o λ-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:

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 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[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] \equiv (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.

Codifiche[modifica | modifica wikitesto]

Nel λ-calcolo sono state formulate diverse codifiche. Una delle prime, fu ovviamente quella formulata dallo stesso ideatore del linguaggio, Alonzo Church e che quindi prese il nome di Codifica di Church. La codifica esprimeva nel linguaggio, l'aritmetica relativa all'insieme dei numeri naturali \mathbb{N}, la logica booleana e altri tipi di informazioni. Da notarsi che questa codifica non è l'unica esistente, ad esempio è stata formulata anche quella di Mogensen-Scott. Esistono, poi, altre codifiche che però usano il lambda calcolo tipato, come il Sistema F.

Numerazione[modifica | modifica wikitesto]

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

n := \lambda s z. s_0 \circ s_1 \circ \cdots \circ s_n (z)

Tutti i numeri appartenenti all'insieme dei numeri naturali, dunque, possono essere espressi in questo modo.

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

Funzioni aritmetiche[modifica | modifica wikitesto]

Nel precedente paragrafo è stata formulata l'enumerazione dei numeri dell'insieme \mathbb{N}, in questa sezione, verranno trattate alcune tra le principali funzioni dell'aritmetica.

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[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

La logica booleana o algebra di Boole, è una formalizzazione della logica che si basa su due valori, cioè vero e falso, ideata dal logico e matematico britannico George Boole, da cui prende il nome.

Valori di verità[modifica | modifica wikitesto]

Come scritto precedentemente, la logica booleana, si basa su due valori di verità, vero e falso. Esse sono esprimibili secondo la codifica di Church, nel modo seguente:

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.

Funzioni logiche[modifica | modifica wikitesto]

Sono state definite i valori della logica booleana, di seguito, verranno espresse delle funzioni per poter elaborare le precedenti funzioni.

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

Esempi[modifica | modifica wikitesto]

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[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, 2003 [1989], 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]