lambda-calcolo

lambda-calcolo

lambda-calcolo o λ-calcolo o L-calcolo, modello di calcolo introdotto negli anni Trenta del secolo scorso da A. Church allo scopo di rappresentare formalmente il procedimento di computazione di una funzione matematica. Si basa su un linguaggio formale i cui elementi costitutivi sono i termini o lambda-termini, i quali hanno lo scopo di rappresentare variabili e funzioni. Nel λ-calcolo è possibile definire un procedimento di trasformazione o riduzione di un termine in un altro termine a esso equivalente, ma riscritto in una forma più semplice. Se un termine corrisponde a una funzione, il procedimento di riduzione del termine, che può essere iterato, corrisponde al calcolo della funzione stessa; in questo senso si dice che è possibile rappresentare nell’ambito del λ-calcolo il calcolo di una classe di funzioni. È possibile dimostrare che le funzioni rappresentabili nel λ-calcolo sono tutte e sole le → funzioni ricorsive, le quali sono calcolabili anche con il modello della macchina universale di → Turing e ciò costituisce un argomento a sostegno della tesi di → Church.

Come premessa al λ-calcolo vanno considerate due osservazioni che sono alla base delle due regole fondamentali di astrazione e di applicazione in esso introdotte. Scrivere sinx vuol dire considerare la funzione sin applicata all’elemento x: la funzione ha un nome (sin) che la individua nella sua scrittura formale, a differenza per esempio della funzione x ². La λ-notazione per queste due funzioni è rispettivamente λxsinx e λxx ² avendo così indicato la variabile su cui si opera e successivamente il come si opera: in questa caratteristica risiede la regola dell’astrazione. Per quanto riguarda invece la regola dell’applicazione occorre osservare che usualmente l’espressione ƒ(x) è interpretata considerando la funzione ƒ come “fissa” e l’oggetto x come variabile; tuttavia l’espressione ƒ(x) può avere significato anche considerando x fisso e ƒ variabile. Per ovviare a questo si conviene di introdurre la scrittura (ƒ )x per indicare l’applicazione di ƒ a x. La λ-notazione permette così di trattare segni in modo indistinto essendo la loro specificità e il loro diverso ruolo implicitamente attribuiti dalla costruzione delle sequenze in cui essi compaiono. L’insieme degli oggetti con cui il λ-calcolo opera è, quindi, genericamente indicato come insieme di termini, detti anche lambda-termini, costruiti a partire da un insieme numerabile di variabili mediante l’applicazione delle regole seguenti:

• ogni variabile è un termine;

• regola di astrazione: se t è un termine e x è una variabile, allora anche λxt è un termine costruito per astrazione della variabile x dal termine t. In sostanza, con questa regola il termine t viene considerato come funzione della variabile x;

• regola di applicazione: se u e v sono due termini, allora anche (u)v è un termine costruito per applicazione del termine u al termine v. Questa regola di costruzione corrisponde all’applicazione di una funzione a una variabile o a un’altra funzione;

• i termini sono tutti e soli quelli costruiti con le tre regole precedenti.

Per esempio, l’espressione (λxt)u è un lambda-termine perché è “ben formato” secondo le regole precedenti. Esso rappresenta l’applicazione della funzione t, di variabile x, al termine u.

Una variabile x può comparire più volte in un termine e ogni presenza della variabile x è detta occorrenza. Si dice che una variabile x ha una occorrenza vincolata (o occorrenza legata) se compare nel campo di azione del simbolo λ, cioè se appare in un termine del tipo λxt; se invece la variabile compare al di fuori di un termine di questo tipo, allora si dice che ha una occorrenza libera. Per esempio, nel termine (λxx)x la variabile x compare tre volte, le prime due sono occorrenze vincolate mentre l’ultima è un’occorrenza libera. Una variabile libera in un termine t è una variabile avente almeno un’occorrenza libera in t, altrimenti la variabile si dice vincolata o legata. Per esempio, nel termine λx(u)x la variabile x è legata, mentre nel termine (λx(u)x)x la variabile x è libera perché appare anche fuori del campo di azione del simbolo λ, cioè ha una occorrenza libera. Un termine senza variabili libere si dice termine chiuso; se invece c’è almeno una variabile libera allora si dice termine aperto.

Le occorrenze libere di una variabile rivestono un ruolo importante perché possono essere sostituite da altri termini dando luogo a un meccanismo di trasformazione dei lambda-termini che corrisponde a un procedimento di calcolo delle funzioni. In particolare, in un termine u ogni occorrenza libera di una variabile x può essere sostituita da un altro termine t e tale sostituzione è indicata simbolicamente con u[t |x]. È importante sottolineare che la sostituzione deve avvenire in modo che nessuna variabile libera nel termine diventi legata nel termine u; è necessario cioè evitare che avvenga la cosiddetta cattura della variabile e per evitare ciò occorre ridenominare le variabili legate di u in modo che non coincidano con le variabili libere di t. Per esempio, se u = λx(x)y e t = x, allora nell’applicare la sostituzione u[t |y] bisogna rinominare la variabile x nel termine u e riscrivere per esempio u = λz(z)y. In questo modo dalla sostituzione risulta u[t |y] = λz(z)x e la variabile x che era libera nel termine t è rimasta libera anche dopo la sostituzione. La regola che permette di ridenominare le variabili legate è detta α-conversione ed esprime il fatto che non è importante il nome delle variabili legate (per esempio λxsinx si converte in λysiny). Il passo elementare di calcolo consiste nel passare da un termine del tipo (λxt)u, in cui t è una funzione di variabile x applicata a u, al termine t[u |x], in cui u è stato sostituito al posto di x in t: cioè la funzione t è calcolata in u. (Il primo dei due termini è detto redesso, da “espressione riducibile”, mentre il secondo è detto contratto). Si può esprimere questo passaggio con la formula (λxt)u → t[u |x]. Per esempio, il calcolo della funzione x ² + x per il valore x = 7 può essere così rappresentato nella λ-notazione (dove il simbolo ≡ indica «convertibile in»):

Ripetendo questo passo elementare un numero finito di volte si può ridurre un termine u in un altro termine u′ e la relazione binaria riflessiva e transitiva che si stabilisce fra u e u′ è detta β-conversione (o anche β-riduzione). Il procedimento di riduzione può continuare fintanto che nel termine in questione sono presenti dei redessi (espressioni riducibili); se ciò non accade, la riduzione si arresta e il termine a cui si è pervenuti viene detto in forma normale. Non sempre è possibile giungere a un termine in forma normale dopo un numero finito di passi. Si prenda per esempio il termine ω = (λx(x)x)λx(x)x in cui è presente un solo redesso: se si prova a ridurlo secondo la regola precedente si ottiene ancora lo stesso termine, cioè (λx(x)x)λx(x)x ≡ (λx(x)x)λx(x)x. Ciò significa che iterando il procedimento si otterrà sempre lo stesso redesso senza mai giungere a una forma normale; in questo caso il termine si dice non normalizzabile. Un’ulteriore regola di conversione, detta η-conversione, consente di trasformare (λxu)x in u purché sia ammissibile la sostituzione di x con u.

Due termini t e v sono convertibili tra loro e si scrive t ≡ v se sono ottenuti attraverso successive applicazioni dei tre operatori di conversione (α, β, η) e delle proprietà di congruenza della relazione di convertibilità. Si definisce poi combinatore un termine normale che non contiene occorrenze libere di variabili. Esempi di combinatori sono:

• il combinatore identico I così definito: I ≡ λxx che è tale che It ≡ t qualunque sia il termine t; infatti per la regole della β-conversione: (λxx)t ≡ x[t |x] ≡ t;

• il combinatore cancellatore K ≡ λxλyx che, di una coppia di termini, ne cancella il secondo:

• il combinatore nullo che di una coppia di termini cancella il primo;

• …

L’impiego di combinatori permette di convertire rapidamente un termine in un altro e di sviluppare così un calcolo (→ logica combinatoria). Per rappresentare nel lambda-calcolo funzioni numeriche si descrivono poi i numeri naturali per mezzo dei lambda-termini secondo la seguente corrispondenza:

• il numero 0 è rappresentato dal termine λƒ λxx che viene indicato con il simbolo 0;

• il numero 1 invece è rappresentato da 1 = λƒ λx(ƒ )x;

• il numero 2 da 2 = λƒ λx((ƒ )ƒ )x;

• …

• il numero k è rappresentato da k = λƒ λx(ƒ )^kx.

I termini che rappresentano i numeri naturali sono combinatori. Se φ è una funzione aritmetica, definita per un sottoinsieme di N, allora un termine Φ del lambda-calcolo rappresenta φ se, per n ∈ N, si ha:

• se φ(n) = m allora il termine (Φ)n si può ridurre per β-conversione al termine m;

• se φ(n) non è definita allora il termine (Φ)n non è normalizzabile.

La funzione φ si dice rappresentabile nel λ-calcolo. Per esempio, la funzione successore, che associa a ogni numero naturale n il numero naturale n + 1, può essere rappresentata dal termine λn λƒ λx((n)ƒ )(ƒ )x, come si osserva applicandolo al termine 0 = λƒ λxx. Si ottiene, infatti:

Con il procedimento di β-conversione si è giunti al termine 1 = λƒ λx(ƒ )x che rappresenta appunto il successore di 0.

L’importanza della nozione di funzione rappresentabile risiede nel fatto che l’insieme delle funzioni rappresentabili da termini del lambda-calcolo corrisponde esattamente all’insieme delle funzioni ricorsive parziali. Ciò implica che il lambda-calcolo può essere considerato, al pari delle funzioni ricorsive o della macchina universale di Turing, un modello di calcolo in grado di tradurre in termini rigorosi il concetto intuitivo di funzione calcolabile.