Алонзо Чёрч
Подробнее
- Родился
- Умер
- Известен как
- Лямбда-исчисление, тезис Чёрча — Тьюринга, теорема Чёрча
- Гражданство
- США
Ответил на проблему разрешения Гильберта за несколько месяцев до Тьюринга — с помощью инструмента, который оказался прародителем языков программирования.
Чёрч, математик из Принстона, в начале 1930-х разработал лямбда-исчисление — формальную систему, где всё является функцией, а вычисление означает переписывание выражений. Весной 1936 года он с её помощью показал, что у Entscheidungsproblem нет решения. Тьюринг в том же году пришёл к тому же ответу совершенно иной моделью, а затем в 1936–1938 годах стал аспирантом Чёрча; выяснилось, что обе системы вычисляют ровно одно и то же — это и есть тезис Чёрча — Тьюринга.
Лямбда-исчисление не осталось внутри доказательства. Его простая типизированная версия 1940 года — предок всех систем типов, а LISP, ML, Haskell и лямбда-выражения, добравшиеся до C++, Java и Python, напрямую происходят от нотации Чёрча для анонимных функций.
Возможно, ещё важнее его учителя-наследие: Тьюринг, Клини, Россер, Дана Скотт, Михаэль Рабин, Реймонд Смаллиан. Чёрч был дотошен до степени анекдота — мыл доску перед тем, как писать, даже если она и так была чистой, — и в 1936 году основал Journal of Symbolic Logic, сорок лет следя за порядком в нём.