• Istituto
    • Chi Siamo
    • La nostra storia
  • Magazine
    • Agenda
    • Atlante
    • Il Faro
    • Il Chiasmo
    • Diritto
    • Il Tascabile
    • Le Parole Valgono
    • Lingua italiana
    • WebTv
  • Catalogo
    • Le Opere
    • Bottega Treccani
    • Gli Ebook
    • Le Nostre Sedi
  • Scuola e Formazione
    • Portale Treccani Scuola
    • Formazione Digitale
    • Formazione Master
    • Scuola del Tascabile
  • Libri
    • Vai al portale
  • Arte
    • Vai al portale
  • Treccani Cultura
    • Chi Siamo
    • Come Aderire
    • Progetti
    • Iniziative Cultura
    • Eventi Sala Igea
  • ACQUISTA SU EMPORIUM
    • Arte
    • Cartoleria
    • Design & Alto Artigianato
    • Editoria
    • Idee
    • Marchi e Selezioni
  • Accedi
    • Modifica Profilo
    • Treccani X

lambda-calcolo

di Silvio Bozzi - Enciclopedia della Scienza e della Tecnica (2008)
  • Condividi

lambda-calcolo

Silvio Bozzi

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

Vedi anche
Alonzo Church Church ‹čë´ëč›, Alonzo. - Matematico e logico-matematico statunitense (Washington 1903 - Hudson, Ohio, 1995), prof. di matematica (1947-61), poi di matematica e filosofia (1961-67) a Princeton, dal 1967 di matematica e filosofia all'univ. di California. Nel 1936 enunciò la proposizione oggi chiamata ... Haskell Brooks Curry Curry ‹kḁ´ri›, Haskell Brooks. - Matematico statunitense (Millis, Massachusetts, 1900 - Filadelfia 1982); prof. alla Pennsylvania State Univ. dal 1941. Si è occupato soprattutto di logica matematica. Tra le sue opere: Combinatory logic (1958), Foundations of mathematical logic (1963). ricorsività ricorsività La proprietà di essere ricorsivo, cioè ricorrente. Teoria della ricorsivita, o della ricorsione, o computabilità, la disciplina che si occupa di fornire una caratterizzazione matematica del concetto di algoritmo. 1. Teoria della ricorsività La motivazione originaria per lo studio della ... lògica matemàtica lògica matemàtica Branca della logica, che utilizza un linguaggio simbolico e adotta un sistema di calcolo di tipo algebrico per esaminare le espressioni di un discorso deduttivo. Queste ultime possono essere considerate formalmente come oggetti grafici combinabili tra loro (sintassi) o in relazione ...
Categorie
  • LOGICA in Filosofia
Tag
  • LINGUAGGI DI PROGRAMMAZIONE
  • TEORIA DELLA DIMOSTRAZIONE
  • TEORIA DELLE CATEGORIE
  • FUNZIONI RICORSIVE
  • LOGICA MATEMATICA
Altri risultati per lambda-calcolo
  • lambda-calcolo
    Enciclopedia della Matematica (2013)
    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, ...
Vocabolario
variante Lambda
variante Lambda (variante lambda; per ellissi, Lambda) loc. s.le f. Mutazione del coronavirus SARS-CoV-2 emersa nel Perù nel corso del 2020. ♦ «I dati inglesi della "variante Delta" evidenziano che colpisce anche le fasce più giovani, i...
lambda
lambda (o labda) s. m. [dal gr. λάμβδα o λάβδα (lat. lambda), dal fenicio lama, ebr. lāmedh], invar. – Nome della undicesima lettera dell’alfabeto greco e del segno che la rappresenta (minuscolo λ, maiuscolo Λ), corrispondente alla lettera...
  • Istituto
    • Chi Siamo
    • La nostra storia
  • Magazine
    • Agenda
    • Atlante
    • Il Faro
    • Il Chiasmo
    • Diritto
    • Il Tascabile
    • Le Parole Valgono
    • Lingua italiana
    • WebTv
  • Catalogo
    • Le Opere
    • Bottega Treccani
    • Gli Ebook
    • Le Nostre Sedi
  • Scuola e Formazione
    • Portale Treccani Scuola
    • Formazione Digitale
    • Formazione Master
    • Scuola del Tascabile
  • Libri
    • Vai al portale
  • Arte
    • Vai al portale
  • Treccani Cultura
    • Chi Siamo
    • Come Aderire
    • Progetti
    • Iniziative Cultura
    • Eventi Sala Igea
  • ACQUISTA SU EMPORIUM
    • Arte
    • Cartoleria
    • Design & Alto Artigianato
    • Editoria
    • Idee
    • Marchi e Selezioni
  • Accedi
    • Modifica Profilo
    • Treccani X
  • Ricerca
    • Enciclopedia
    • Vocabolario
    • Sinonimi
    • Biografico
    • Indice Alfabetico

Istituto della Enciclopedia Italiana fondata da Giovanni Treccani S.p.A. © Tutti i diritti riservati

Partita Iva 00892411000

  • facebook
  • twitter
  • youtube
  • instagram
  • Contatti
  • Redazione
  • Termini e Condizioni generali
  • Condizioni di utilizzo dei Servizi
  • Informazioni sui Cookie
  • Trattamento dei dati personali