Lambda calcolo

Da Wikipedia, l'enciclopedia libera.

Il lambda calcolo è un sistema di riscrittura definito formalmente dal matematico Alonzo Church. È stato sviluppato per analizzare formalmente le definizioni di funzioni, le loro applicazioni ed è uno strumento interessante per studiare anche fenomeni di ricorsione. In quanto sistema di riscrittura, esso dà una descrizione dei termini ben formati, che sono le sequenze di simboli riconosciute dal sistema e in grado di essere riscritti da esso. Il lambda calcolo, infatti, definisce un insieme di regole di riscrittura che determinano in maniera precisa come i termini stessi possono essere riscritti. In questo modo, il processo di riscrittura diventa un vero e proprio calcolo. Per tale ragione, nel corso di questa descrizione ci si riferirà al lambda calcolo come il calcolo, quando non ci sia pericolo di ambiguità.

Il lambda calcolo affonda le proprie radici nel concetto di funzione. In matematica si definiscono funzioni particolari associazioni fra gli elementi di un insieme (dominio) e gli elementi di un altro insieme (codominio). Ad esempio, se chiamiamo quadrato la funzione che dato un numero restituisca il suo quadrato, scriviamo:

quadrato : $\mathbb{R} \to \mathbb{R}$ .

per indicare che quadrato mappa elementi dell'insieme dei numeri reali su altri elementi dello stesso insieme.

Se una funzione è in grado di associare un risultato ad un certo argomento che le viene passato, diremo che tale funzione è definita per quel valore passato come argomento. Se una funzione è definita su ogni elemento del dominio, essa è detta totale; in caso contrario, diremo che si tratta di una funzione parziale.

La notazione insiemistica non fornisce informazioni a proposito di come effettivamente si possa passare dagli argomenti ricevuti al risultato ad essi associato. In altre parole, non si descrive come calcolare il risultato (detto anche: valore in uscita) della funzione stessa, a partire dai suoi argomenti (detti anche: valori in ingresso). Il lambda calcolo, così come la Teoria delle Funzioni Ricorsive e la Macchina di Turing, è un formalismo che consente di definire il lato meccanico delle funzioni, ovvero proprio quelle procedure che consentono di produrre dei valori in uscita a partire da certi valori in ingresso.

Di seguito vedremo una descrizione della sintassi del lambda calcolo che procederà per gradi: dopo aver definito come sono fatti i termini del lambda calcolo, introdurremo le regole di riscrittura del calcolo stesso; dopodiché vedremo alcune strategie di riscrittura (anche dette: strategie di riduzione), le quali definiscono un ordine con cui applicare le regole di riscrittura, e come la scelta di una regola piuttosto che un'altra garantisca (o inibisca) determinate proprietà del calcolo.

[modifica] Termini

Chiamiamo termine del lambda calcolo (o più brevemente lambda termine o lambda espressione) qualunque stringa generata dalla seguente grammatica (espressa secondo la cosiddetta forma Backus-Naur):

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

dove assumiamo che Id appartenga a un insieme numerabile (e infinito) di nomi (o identificatori, o variabili).

Parafrasando la descrizione formale data dalla grammatica appena sopra, possiamo dire che 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. Vale la pena specificare che queste interpretazioni (variabile, astrazione e applicazione) sono solo delle scorciatoie, e non hanno alcuna valenza semantica. Di fatto è possibile associare una funzione matematica (con alcune peculiarità) ad ogni lambda termine (in particolare grazie alla Semantica Denotazionale); ciò significa che effettivamente si possono interpretare i lambda termini quali oggetti matematici, in particolare funzioni. In questo contesto, però ci interessa trattare tali espressioni dal solo punto di vista sintattico, come mera manipolazione di simboli. Vanno a questo scopo introdotte le regole di riscrittura del calcolo.

[modifica] Regole di riscrittura

Definiamo come i lambda termini possono essere riscritti.

[modifica] Variabili

Dato un generico lambda termine T, chiamiamo Var(T) l'insieme che contiene tutte le variabili menzionate in T. Chiamiamo Libere(T) l'insieme che contiene le sole variabili libere di T. Chiamiamo infine Legate(T), l'insieme con tutte le variabili cosiddette legate.

L'insieme di tutte le variabili semplicemente raccoglie tutti i nomi di variabile presenti in un lambda termine.

L'insieme delle variabili libere è così definito:

$Libere(x) = {x}$ ;
$Libere(λ x . M) = Libere(M) - {x}$ ;
$\textrm{Libere}(M N) = \textrm{Libere}(M) \cup \textrm{Libere}(N)$ .

L'insieme delle variabili legate è composto da quelle variabili che non sono libere, e quindi si ottiene come semplice differenza tra i due insiemi sopra definiti: Legate(T) = Var(T) - Libere(T).

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:

Var(λ z .λ x .(x y)) = {z, x, y}

;

Libere(λ z .λ x .(x y)) = {y}

;

Legate(λ z .λ x .(x y)) = {x, z}

;

[modifica] Sostituzione

Un concetto fondamentale è quello di sostituzione. Chiamiamo 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:

$T 1 [T 2 / T 3]$

la sostituzione del termine $T 2$ al posto di $T 3$ all'interno del termine $T 1$ , il quale funge da contesto. 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:

$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 y . (M [N[z / y] / 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:

$(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 z . ((z x)[(z x)[w / z] / x]) \equiv \lambda z . ((z x)[(w x) / x]) \equiv \lambda z . z (w 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 intuitivamente scorretto (la ragione per cui diciamo ciò sarà più evidente una volta capito come vengono utilizzati i lambda termini per computare).

[modifica] 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, 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)))$

[modifica] Beta riduzione

$(\lambda x . M) N \Rightarrow_{\beta} M [N / x]$ .

La beta riduzione è analoga all'operazione di applicazione di una funzione matematica ai suoi argomenti: il termine sulla destra rappresenta l'argomento (o parametro), mentre il termine più a sinistra rappresenta la funzione stessa che viene applicata.

Vale la pena notare che un termine, per poter essere applicato (o beta-ridotto), deve essere una lambda-astrazione, mentre non viene fatta alcuna assunzione riguardo la forma del termine argomento. 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 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$

[modifica] Eta conversione

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

Quanto diciamo che $λ x .(M x)$ e $M$ si comportano allo stesso modo, intendiamo dire che: $\forall 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 $λ$ -calcolo estensionale (Barendregt, The Lambda Calculus).

[modifica] Termini equivalenti

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.

[modifica] Forme normali

Diciamo che un termine del lambda calcolo si trova in forma normale se esso non è riscrivibile per mezzo della regola di Beta-riduzione.

Intuitivamente, un termine in forma normale è un oggetto che il calcolo non può semplificare ulteriormente; al più lo si può riscrivere in un termine equivalente. Nel lambda calcolo, quindi, una funzione calcolabile è (rappresentata da) una qualche lambda espressione in grado di riscriversi fino a raggiungere un termine in forma normale. Viceversa, esistono termini che generano una successione infinita di riscritture senza mai raggiungere una forma normale, e che quindi rappresentano funzioni non calcolabili. Un esempio di espressione non calcolabile è la seguente:

$\lambda y . (y y) \lambda y . (y y) \Rightarrow_{\beta} \lambda y . (y y) \lambda y . (y y) \Rightarrow_{\beta} \dots :$

Poiché il termine $D = d e f λ y .(y y)$ non fa altro che prendere un termine e scriverne due copie, esso è spesso noto col termine di duplicatore.

Immaginiamo ora di poter esprimere nel lambda calcolo i numeri naturali e l'operazione di somma come definita solitamente in algebra, cosa per altro possibile. Quello seguente è un esempio di funzione calcolabile:

$(\lambda x . x + 2) 5 \Rightarrow_{\beta} 5 + 2 \Rightarrow_{\beta} (5 + 1) + 1 \Rightarrow_{\beta} 6 + 1 \Rightarrow_{\beta} 7$ .