Lambda calcolo
![](http://upload.wikimedia.org/wikipedia/commons/thumb/3/3a/Greek_lc_lamda_thin.svg/150px-Greek_lc_lamda_thin.svg.png)
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
[modifica | modifica wikitesto]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
[modifica | modifica wikitesto]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:
dove la metavariabile 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 , si definisce l'insieme che contiene tutte le variabili menzionate in . Tra queste si distinguono due partizioni: l'insieme delle variabili libere, scritto , e l'insieme delle variabili legate, indicate con . L'insieme delle variabili libere è definito ricorsivamente come segue:
- ;
- ;
- .
L'insieme delle variabili legate è quindi ottenibile per differenza:
- .
Il punto 2 della definizione implica che il costrutto sintattico dell'astrazione è un legatore di variabile: se , allora .
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:
- ;
- ;
- ;
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. Si indica con la sostituzione del termine al posto di all'interno del termine : ogni occorrenza libera della variabile in è sostituita da . Un semplice esempio di sostituzione è il seguente:
- .
Una definizione ricorsiva dell'algoritmo di sostituzione è la successiva:
- ;
- , se ;
- ;
- , se e ;
- , se , , e è un nome fresco;
- .
Alcuni esempi di sostituzione:
- ;
- ;
- , dove è 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
[modifica | modifica wikitesto].
L'alfa conversione si applica ai termini che sono astrazioni. Data un'astrazione, è possibile riscriverla sostituendo la variabile astratta () con un'altra (), 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:
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:
- .
(Sostituire N, alle occorrenze delle variabili legate, in M)
La regola ha come oggetto un'applicazione di una lambda astrazione nella forma su un secondo termine . 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 dove il parametro attuale (effettivo) viene sostituito al parametro formale della funzione. In questo contesto dunque la sostituzione rappresenta proprio il passaggio del parametro.
Alcuni esempi di beta riduzione sono:
Eta conversione
[modifica | modifica wikitesto], se .
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 e si comportano allo stesso modo, equivale a dire che per ogni : . In altre parole la eta-conversione assiomatizza la dimostrabilità dell'uguaglianza nel -calcolo estensionale[1].
Termini equivalenti
[modifica | modifica wikitesto]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:
- ,
- , se .
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:
.
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
[modifica | modifica wikitesto]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
[modifica | modifica wikitesto]La numerazione di Church può esprimere l'insieme dei numeri naturali 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.
Tutti i numeri appartenenti all'insieme dei naturali possono essere espressi analogamente.
Operazioni aritmetiche
[modifica | modifica wikitesto]Relativamente alla precedente numerazione dei numeri naturali è possibile esprimere alcune computazioni elencate di seguito.
Funzione | Definizione aritmetica | Definizione secondo Church |
---|---|---|
Successore | ||
Addizione | ||
Moltiplicazione | ||
Potenza |
Esempi
[modifica | modifica wikitesto]
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, esprimibili come di seguito.
Da notarsi che la funzione rappresenta sia il valore zero che falso.
Operazioni logiche
[modifica | modifica wikitesto]Di seguito, verranno espresse alcune delle più semplici operazioni relative alla logica booleana.
Funzione Logica | Simbolo | Definizione |
---|---|---|
E (AND) | ||
O (OR) | ||
NON (NOT) |
Esempi
[modifica | modifica wikitesto]
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, si supponga di arricchire il calcolo aggiungendovi i numeri naturali (semplicemente denotati come ) e l'operazione di addizione binaria su di essi (scritta in forma prefissa come ), entrambi peraltro direttamente codificabili come lambda termini. Si consideri ora un termine che somma al suo argomento, ovvero e si usi come argomento il valore . Tale applicazione converge a forma normale , infatti: .
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 , che non fa altro che prendere un termine e restituirne due copie, l'una applicata all'altra. È possibile dunque definire il termine , e notare che esso riduce a se stesso .
Note
[modifica | modifica wikitesto]- ^ Barendregt, The Lambda Calculus
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]Altri progetti
[modifica | modifica wikitesto]Wikimedia Commons contiene immagini o altri file sul lambda calcolo
Collegamenti esterni
[modifica | modifica wikitesto]- (EN) lambda calculus, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
- (EN) Lambda calcolo, su Internet Encyclopedia of Philosophy.
- (EN) Lambda calcolo, su Stanford Encyclopedia of Philosophy.
- (EN) Eric W. Weisstein, Lambda calcolo, su MathWorld, Wolfram Research.
- (EN) Denis Howe, lambda-calculus, in Free On-line Dictionary of Computing. Disponibile con licenza GFDL
- (IT) Esempio di tesi su Lambda calcolo : "Compilatore Z : XML tra Source e Target", su tesionline
Controllo di autorità | LCCN (EN) sh85074174 · GND (DE) 4166495-4 · BNF (FR) cb119586908 (data) · J9U (EN, HE) 987007553113905171 |
---|