lambda-calcolo

lambda-calcolo

Presentato per la prima volta da Alonzo Church nel 1932 come frammento di un più ampio sistema (poi dimostratosi contraddittorio) per la fondazione della matematica, il λ-calcolo nelle sue diverse formulazioni fornisce un’analisi del concetto di funzione, intesa non insiemisticamente ma come regola per trasformare espressioni in altre espressioni mediante un processo di riscrittura. In questa veste esso ha oggi un grande interesse tanto nella logica matematica (teoria dei tipi, teoria delle funzioni e dei funzionali ricorsivi) che nell’informatica. Nella logica, sopratutto dopo la individuazione da parte di Haskell B. Curry e William A. Howard di una fondamentale corrispondenza tra funzionali e dimostrazioni, il calcolo svolge un ruolo centrale nella teoria della dimostrazione, mentre nell’informatica fornisce una base per la formulazione e lo studio di linguaggi di programmazione. L’idea alla base delle diverse formulazioni è quella di introdurre – mediante regole sintattiche di riscrittura – un operatore λ che agisce su variabili il cui scopo è quello di permetterci di definire – a partire da un’espressione – un termine t(x) in cui occorre la variabile x, una nuova espressione λxt(x), in cui x risulta vincolata, che denota la funzione che applicata a qualunque argomento s ci darà come valore la funzione denotata da t per l’argomento denotato da s. Se la giustapposizione indica l’operazione di applicazione avremo così sul piano sintattico la regola

λxt(x)(s) = t(x/s),

dove t(x/s) indica la sostituzione di ogni occorrenza libera di x con una di s. Aggiungendo regole come quella di sopra (la conversione) si può determinare con più precisione la natura delle funzioni che così si definiscono in termini di regole di trasformazione. Nel sistema puro, l’operazione di applicazione non ha limitazioni e non si introducono distinzioni tra le espressioni e questo risulta fondamentale per studiare l’esistenza di punto fissi e principî di recursione; è però possibile introdurre distinzioni di tipo (distinguendo individui da funzioni, funzioni da funzioni di funzioni, ecc,) e questo si può fare in diversi modi come mostrato da Church (1940) e da Curry (1934). Abbiamo così formulazioni senza tipi e con tipi che arricchiscono di molto le possibilità espressive del calcolo ma – malgrado la semplicità della sintassi – come mostrato da Church nel 1941, è possibile già nel sistema di base aggiungendo opportune costanti introdurre termini per i numeri naturali e provare che tutte e sole le funzioni ricorsive generali sono definibili da λ-temini. Il fatto che in tutte le sue varianti il λ-calcolo sia di natura sintattica lo rende uno strumento possibile per la costruzione di modelli di teorie che definiscono funzioni o funzionali (per es., il sistema T di Gödel del 1958 per i funzionali ricorsivi finiti). Questi modelli hanno come oggetti termini quozientati rispetto a opportune relazioni di equivalenza definite a partire dalle regole di riscrittura. Centrali a questo riguardo divengono così le varie forme del teorema dimostrato originariamente da Church e John B. Rosser che garantiscono la possibilità di identificare queste classi d’equivalenza con termini irriducibili rispetto alle regole. Fino agli anni Settanta insoluto era rimasto il problema di un’analisi insiemistica delle diverse forme di λ-calcolo. Una prima analisi semantica di questo tipo fu fornita da Dana S. Scott nel 1976 in termini di spazi di funzioni continue. Questa analisi ha aperto la strada a un approccio al λ-calcolo in termini di teoria delle categorie e oggi sono molti e fondamentali i risultati in cui le due discipline interagiscono.

→ Programmazione, algoritmi di