Alonzo Church
Więcej informacji
- Data urodzenia
- Data śmierci
- Znany z
- Rachunek lambda, teza Churcha-Turinga, twierdzenie Churcha
- Narodowość
- amerykańska
Odpowiedział na problem rozstrzygalności Hilberta na kilka miesięcy przed Turingiem, narzędziem, które okazało się przodkiem języków programowania.
Church był matematykiem z Princeton, który na początku lat trzydziestych rozwinął rachunek lambda: system formalny, w którym wszystko jest funkcją, a obliczanie polega na przepisywaniu wyrażeń. Wiosną 1936 roku użył go, by wykazać, że Entscheidungsproblem nie ma rozwiązania. Turing doszedł w tym samym roku do tej samej odpowiedzi zupełnie innym modelem, po czym w latach 1936–1938 został doktorantem Churcha, a oba systemy okazały się obliczać dokładnie to samo — to, co dziś nazywamy tezą Churcha-Turinga.
Rachunek lambda nie pozostał w granicach dowodu. Jego prosto typowany wariant z 1940 roku jest przodkiem wszystkich systemów typów, a LISP, ML, Haskell i wyrażenia lambda, które przeniknęły do C++, Javy i Pythona, pochodzą wprost od zapisu Churcha dla funkcji anonimowych.
Większym dziedzictwem może być lista jego doktorantów: Turing, Kleene, Rosser, Dana Scott, Michael Rabin, Raymond Smullyan. Church był skrupulatny do stopnia, który stał się anegdotą — zmywał tablicę przed pisaniem, nawet gdy była już czysta — i założył w 1936 roku Journal of Symbolic Logic, po czym pilnował go przez cztery dekady.