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
(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
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
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 [...] . Ch. sviluppò anche altre linee di ricerca, quali le relazioni con la logica combinatoria di Curry, le questioni di teoria dei tipi e il λ-calcolo. Tra le opere: The calculi of lambda-conversion (1941) e Introduction to mathematical logic (1956). ...
Leggi Tutto
Biologia
In genetica, tratto di DNA che fa parte di un operone e condiziona la trascrizione dei geni strutturali immediatamente adiacenti (➔ operone).
Filosofia
In filosofia analitica, un’espressione [...] quello di d’Alembert: ∂2/∂x2−∂2/∂y2 ecc.
Calcolo operatorio
Il calcolo operatorio e l’interesse allo studio degli o. come enti attributo a essa corrispondente. Esso si chiama o. lambda (simbolo λ). Nella logica estensionale ogni attributo ...
Leggi Tutto
Matematica
Termine, derivato dall’appellativo al-Khuwārizmī («originario della Corasmia») del matematico Muḥammad ibn Mūsa del 9° sec., che designa qualunque schema o procedimento sistematico di calcolo [...] definizione delle funzioni mediante l’operatore di astrazione lambda e i sistemi di combinatori di H.B. . Dall’altro si cerca di caratterizzare in modo astratto il procedimento di calcolo. Si hanno in questo modo la teoria delle macchine di A. Turing ...
Leggi Tutto
La grande scienza. Cronologia scientifica: 1971-1980
1971-1980
1971
I problemi NP-completi. L'informatico americano Stephen Cook dà il primo esempio di problema algoritmico NP-completo. La classe NP [...] dal virus SV40 e da una varietà modificata di fago lambda. Questo esperimento è considerato l'atto di fondazione dell' . Poco dopo i francesi D. Bonneau e R. Foy comunicano di avere calcolato 4000 km ca. per Plutone e 2000 km ca. per il suo unico ...
Leggi Tutto
La grande scienza. Cronologia scientifica: 1951-1960
1951-1960
1951
Sui gruppi di omotopia e di omologia. In una serie di articoli (Homologie singulière des espaces fibrés) Jean-Pierre Serre fornisce [...] rivestimento universale e, due anni dopo, sarà in grado di calcolare molti gruppi di omotopia delle sfere. Serre sarà insignito della adroni con spin semintero, quali, per esempio, quelli csi, delta, lambda, omega e sigma. ¹
I campi di Yang-Mills. I ...
Leggi Tutto
teoremi di indecidibilità
Silvio Bozzi
In logica matematica, risultati che affermano che una data teoria formalizzata T non è decidibile, vale a dire non ammette un algoritmo in grado di stabilire in [...] finita di una teoria indecidibile – e che non esiste calcolo per la logica d’ordine superiore. Mediante il metodo della fermata per macchine di Turing, il problema della lambda-convertibilità o quello della derivabilità di parole entro sistemi di ...
Leggi Tutto
LOGICA E INFORMATICA
Carlo Cellucci
I. McCarthy (1963) afferma che è ragionevole sperare che le relazioni tra l'i. e la l. matematica nel prossimo secolo saranno altrettanto fruttuose di quelle tra [...] Q ed N ▷β Q.
Si è già detto che il λ−calcolo costituisce una modellizzazione dei procedimenti di computo a un più alto livello Tourlakis, Computability, Reston 1984; H.P. Barendregt, The lambda calculus, its syntax and semantics, Amsterdam 1984; H. ...
Leggi Tutto