Alonzo Church
Maggiori informazioni
- Nato il
- Morto il
- Noto per
- Lambda calcolo, tesi di Church-Turing, teorema di Church
- Nazionalità
- Statunitense
Rispose al problema della decisione di Hilbert pochi mesi prima di Turing, con uno strumento che si rivelò l'antenato dei linguaggi di programmazione.
Church, matematico a Princeton, sviluppò il lambda calcolo all'inizio degli anni Trenta: un sistema formale in cui tutto è una funzione e calcolare significa riscrivere espressioni. Nella primavera del 1936 lo usò per dimostrare che l'Entscheidungsproblem non ha soluzione. Turing giunse alla stessa conclusione quell'anno con un modello del tutto diverso, poi fu dottorando di Church dal 1936 al 1938, e i due sistemi risultarono calcolare esattamente le stesse cose: quella che oggi chiamiamo tesi di Church-Turing.
Il lambda calcolo non rimase confinato nella dimostrazione. La variante con tipi semplici del 1940 è l'antenata di ogni sistema di tipi successivo, e LISP, ML, Haskell e le espressioni lambda approdate in C++, Java e Python discendono direttamente dalla notazione di Church per le funzioni anonime.
Forse la sua eredità maggiore è l'elenco dei suoi allievi: Turing, Kleene, Rosser, Dana Scott, Michael Rabin, Raymond Smullyan. Church era meticoloso fino all'aneddoto, tanto da lavare la lavagna prima di scriverci, anche quando era già pulita, e nel 1936 fondò il Journal of Symbolic Logic, che poi tenne in ordine per quattro decenni.