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 [...] 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 ...
Leggi Tutto
lambda-conversione
lambda-conversione locuzione con cui si indica la possibilità del → lambda-calcolo di utilizzare particolari regole per convertire una formula in un’altra. ...
Leggi Tutto
(II, p. 421; App. II, I, p. 125; III, I, p. 61; IV, I, p. 83)
Negli ultimi dieci anni lo sviluppo dell'a. è stato molto vivace. Ai temi di ricerca già consolidati se ne sono aggiunti nuovi e ne sono stati [...] la prima è semplicemente la limitatezza umana nel portare avanti calcoli per decine o centinaia di pagine, la seconda viene programmazione è evidente l'influenza dell'a. (del lambda-calcolo e dell'a. universale), specialmente per la programmazione ...
Leggi Tutto
INFORMAZIONE, SCIENZA DELLA
Roman Tirler
Pierluigi Ridolfi
Stefano Ceri e Alfonso Fuggetta
Tecnologie della comunicazione di Roman Tirler
Sommario: 1. Introduzione. 2. Tecniche di comunicazione dati: [...] possono essere composte tra di loro e richiamarsi ricorsivamente. Le radici di questo approccio sono da ricercarsi nel ‛lambdacalcolo' e nel linguaggio LISP. Attualmente, oltre al LISP, i linguaggi funzionali più diffusi sono Standard ML e Scheme ...
Leggi Tutto
Dimostrazione, teoria della
Jean-Yves Girard
La teoria della dimostrazione nasce negli anni Venti del Novecento come strumento di realizzazione del programma di David Hilbert per la fondazione della [...] tra derivazioni naturali e funzionali (il cosiddetto isomorfismo di Curry-Howard) con i conseguenti rapporti con il lambdacalcolo che coinvolgeranno più tardi anche la teoria delle categorie. Dal punto di vista della teoria riduzionista i risultati ...
Leggi Tutto
funzione calcolabile
funzione calcolabile funzione per la quale esiste una procedura di calcolo (→ algoritmo) che permette di determinarne, in un numero finito di passi, il valore in corrispondenza di [...] alcuni modelli formali per descrivere il processo di calcolo di una funzione. Fra i modelli di calcolo introdotti ci sono le → funzioni ricorsive, la macchina di → Turing e il λ-calcolo (→ lambda-calcolo). Secondo la cosiddetta tesi di → Church, l ...
Leggi Tutto
ricorsivita
ricorsività in logica, caratteristica di un procedimento che riduce la complessità di un problema riportandolo a problemi via via più semplici cui il procedimento stesso viene applicato. [...] . A tale scopo sono stati introdotti, negli anni Trenta del secolo scorso, diversi modelli di calcolo, fra cui l’insieme delle → funzioni ricorsive, il → lambda-calcolo e la macchina universale di → Turing, i sistemi di → Post. Tali modelli si sono ...
Leggi Tutto
Turing, macchina di
Turing, macchina di automa universale, elaborato dal logico inglese A.M. Turing, che fornisce una traduzione formale del concetto intuitivo di → calcolabilità. Sebbene introdotta [...] con altri formalismi costruiti per dare una definizione rigorosa al concetto di calcolabilità (→ Post, sistema di; → lambda-calcolo); tutti questi formalismi descrivono tutte e sole le funzioni ricorsive. La tesi di → Church afferma appunto che ...
Leggi Tutto
definibilita
definibilità termine che designa uno dei principali oggetti di studio della logica matematica, insieme con la dimostrabilità e la calcolabilità; consiste in una riflessione sul concetto [...] di una definizione rigorosa del concetto di → funzione calcolabile; la risposta a questa esigenza è fornita dallʼintroduzione di alcuni modelli di calcolo come la macchina di → Turing, le → funzioni ricorsive e il λ-calcolo (→ lambda-calcolo). ...
Leggi Tutto