Алонзо Чёрч

Чёрч дважды оказался первым и оба раза остался в тени: его ответ на проблему разрешимости опередил тьюринговский на семь месяцев, а придуманный им язык лежит в основании половины современного программирования — под чужими именами.

Принстон

Родился в 1903 году в Вашингтоне. В детстве был ранен из духового ружья и почти ослеп на один глаз. Почти вся его жизнь прошла в Принстоне — студент, аспирант, преподаватель, профессор, с 1924 года по 1967-й; перерыв составили два года стажировки в Гарварде, Гёттингене и Амстердаме. Работал ночами, писал доску безупречным почерком, стирал её так тщательно, что это запомнили все его ученики.

Около 1932 года он строит формальную систему для оснований математики. Основанием она не стала: в 1935-м его собственные аспиранты Клини и Россер доказали, что система противоречива. Но внутри неё был кусок, который выжил и оказался важнее целого.

Три строчки грамматики

Это $\lambda$-исчисление, и вся его грамматика такова. Выражение — это переменная $x$; или абстракция $\lambda x.\,M$ («функция, которая по $x$ даёт $M$»); или применение $M\,N$. Правило вычисления одно:

$$(\lambda x.\,M)\,N \;\longrightarrow\; M[x := N].$$

Ни чисел, ни сложения, ни памяти, ни условных операторов. Оказывается, этого хватает на всё: числа строятся как «применить функцию $n$ раз», сложение и умножение — двумя строчками, дальше логические значения, пары, списки, рекурсия.

Ответ Гильберту

Дальше Чёрч сделал три шага.

Тезис. Функция вычислима в интуитивном смысле тогда и только тогда, когда она $\lambda$-определима. Это утверждение не теорема — его нельзя доказать, потому что «вычислимость вообще» не определена математически; это предложение считать одно определением другого.

Совпадение. Клини доказал, что класс $\lambda$-определимых функций в точности совпадает с классом общерекурсивных функций Гёделя и Эрбрана, введённых из совершенно других соображений. Два независимых определения дали одно и то же — довод в пользу того, что пойман правильный класс.

Неразрешимость. В апреле 1936 года выходит «Неразрешимая задача элементарной теории чисел», а вслед за ней заметка о Entscheidungsproblem: общего алгоритма, распознающего выводимость формулы логики предикатов, не существует.

Через семь месяцев Тьюринг публикует свой ответ на тот же вопрос — с машиной вместо подстановки — и сам же доказывает, что два подхода дают один класс функций. Сегодня утверждение так и называется — тезис Чёрча — Тьюринга. Тьюринг после этого приехал в Принстон и написал у Чёрча диссертацию.

Учитель

Список его аспирантов читается как оглавление учебника: Тьюринг, Клини, Россер, Хартли Роджерс, Майкл Рабин, Дана Скотт, Реймонд Смальян. В 1936 году Чёрч основал «Journal of Symbolic Logic» и десятилетиями вёл в нём библиографический раздел, вручную реферируя всё, что выходило по логике в мире.

Из его языка позже выросли Lisp и вся линия функциональных языков, а из типизированной версии — системы, в которых доказательство и программа оказались одним и тем же объектом: машинная проверка математики устроена именно так.

Умер в 1995 году в Огайо, девяноста двух лет. Обозначение $\lambda$, если верить распространённому рассказу, никакого смысла не несёт вовсе: исходная запись со значком над буквой не набиралась в типографии, значок съехал влево и стал греческой буквой.