Church, Alonzo

Church, Alonzo

Logico e matematico statunitense (Washington 1903 - Hudson, Ohio, 1995). Prof. di matematica (1947-61), poi di matematica e filosofia (1961-67) a Princeton, insegnò dal 1967 matematica e filosofia all’univ. di California. Tra le sue opere: The calculi of lambda conversion (1941) e Introduction to mathematical logic (1956). Nel 1936 enunciò la tesi oggi chiamata tesi di Ch., secondo cui ogni funzione effettivamente calcolabile è ricorsiva. L’evidenza della tesi deriva dal fatto che altre classi di funzioni calcolabili (funzione λ-definibile, funzione calcolabile da una macchina di Turing, da un algoritmo di Markov, ecc.) sono coestensive alla classe delle funzioni ricorsive. Tuttavia la tesi si può confermare con argomenti di carattere sperimentale ma non può essere dimostrata, perché la nozione di ricorsività ammette una definizione precisa, mentre la nozione di calcolabilità ha un carattere informale, che rimanda a una nozione ‘fisica’ di calcolo meccanico. La tesi di Ch. e l’affermazione inversa, del tutto ovvia (ogni funzione ricorsiva è effettivamente calcolabile), caratterizzano la nozione di procedimento effettivo di calcolo nel caso di funzioni di numeri naturali. 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, un calcolo di funzioni alla base del primo linguaggio di programmazione funzionale, il LISP. Da ricordare anche l’importante contributo di Ch. alla semantica logica, sviluppo originale della teoria di Frege sul senso e la denotazione delle espressioni linguistiche (A formulation of the logic of sense and denotation, 1951).