Чёрч: вычисление как подстановка

Язык из трёх строчек

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

Нумералы Чёрча — счётчики повторов; «единица плюс единица» приводится к двойке одной подстановкойMathLocus · построено для этого сайта

Это $\lambda$-исчисление, и его грамматика умещается в три строки. Выражение — это:

переменная: $x$;
абстракция: $\lambda x.\,M$ — «функция, которая по $x$ даёт $M$»;
применение: $M\,N$ — «подставить $N$ в функцию $M$».

Правило вычисления одно, называется $\beta$-редукцией:

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

— «применили функцию к аргументу — подставьте аргумент вместо переменной». Всё. Ни чисел, ни сложения, ни условных операторов, ни памяти. Только функции и подстановка.

Замечательно, что этого хватает.

Как в этом языке появляются числа

Числа не постулируются, а строятся. Число $n$ — это «применить функцию $n$ раз»:

$$\bar 0 = \lambda f.\lambda x.\,x, \qquad \bar 1 = \lambda f.\lambda x.\,f\,x, \qquad \bar 2 = \lambda f.\lambda x.\,f\,(f\,x), \qquad \bar 3 = \lambda f.\lambda x.\,f\,(f\,(f\,x)).$$

Это нумералы Чёрча. Сложение теперь — «примени $f$ сперва $n$ раз, потом ещё $m$ раз»:

$$\mathrm{plus} = \lambda m.\lambda n.\lambda f.\lambda x.\; m\,f\,(n\,f\,x).$$

Проверим на $\bar 1 + \bar 1$. Подставляем и редуцируем:

$$\mathrm{plus}\ \bar1\ \bar1 \;\to\; \lambda f.\lambda x.\ \bar1\,f\,(\bar1\,f\,x) \;\to\; \lambda f.\lambda x.\ f\,(f\,x) \;=\; \bar 2 .$$

Три подстановки — и «$1+1=2$» доказано. Расселу и Уайтхеду на это потребовалось полтора тома; правда, они доказывали другое утверждение и в другой системе.

Умножение выходит ещё короче: $\mathrm{mult} = \lambda m.\lambda n.\lambda f.\ m\,(n\,f)$. Логические значения, пары, списки, рекурсия — всё строится тем же способом, из ничего.

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

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

Определение. Функция называется $\lambda$-определимой, если её можно записать $\lambda$-выражением, работающим на нумералах. Тезис Чёрча: $\lambda$-определимость — это и есть «вычислимость» в интуитивном смысле.

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

Неразрешимость. В статье «Неразрешимая задача элементарной теории чисел» (апрель 1936) Чёрч показывает: нет алгоритма, который по двум $\lambda$-выражениям определяет, приводятся ли они к одному виду. А в короткой заметке того же года — «A note on the Entscheidungsproblem» — выводит отсюда главное следствие:

Проблема разрешения Гильберта неразрешима. Нет процедуры, которая по любой формуле логики первого порядка отвечает, доказуема ли она.

Это первый по времени ответ на Entscheidungsproblem, и он опередил Тьюринга примерно на семь месяцев.

Почему помнят Тьюринга

И всё же в учебниках стоит машина, а не $\lambda$-выражение. Причина не в несправедливости.

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

Показателен свидетель. Гёдель, которому в 1934 году Чёрч изложил своё определение, счёл его совершенно неудовлетворительным: почему именно эти правила, а не другие? После работы Тьюринга Гёдель переменил мнение и писал, что понятие вычислимости стало абсолютным именно благодаря анализу Тьюринга.

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

Отсюда и двойное имя — тезис Чёрча — Тьюринга.

Что из этого выросло

Судьба $\lambda$-исчисления оказалась удивительнее судьбы машины Тьюринга. Машина осталась инструментом теории. $\lambda$-исчисление стало языком программирования — и не одним.

LISP (Джон Маккарти, 1958): функции как значения, lambda прямо в синтаксисе. Второй по возрасту из живых языков программирования.
ML, Haskell, OCaml, F#, Scala — вся ветвь функциональных языков; безымянные функции, приехавшие оттуда же, есть теперь в Python, JavaScript, C++, Java.
Типизированное $\lambda$-исчисление и изоморфизм Карри — Ховарда: типы соответствуют утверждениям, программы — доказательствам, вычисление программы — упрощению доказательства. На этом соответствии построены Coq, Agda и Lean, то есть современная машинная проверка математики. Мечта Лейбница о том, чтобы спор разрешался вычислением, реализована в конце концов именно на языке Чёрча.
Денотационная семантика Дейны Скотта (ученика Чёрча) дала $\lambda$-исчислению математическую модель и превратила теорию языков программирования в науку.

Алонзо Чёрч (1903–1995) проработал в Принстоне тридцать девять лет, основал в 1936 году «Journal of Symbolic Logic» и редактировал его сорок лет. У него был тридцать один аспирант, среди них Тьюринг, Клини, Россер, Дейна Скотт, Майкл Рабин, Мартин Дэвис, Рэймонд Смаллиан. Логику второй половины XX века делали в основном его ученики и ученики его учеников.

Для класса

Проверьте вычислением, что $\mathrm{mult} = \lambda m.\lambda n.\lambda f.\ m\,(n\,f)$ действительно умножает: приведите $\mathrm{mult}\ \bar2\ \bar3$ к нумералу.

(Ответ: $\mathrm{mult}\ \bar2\ \bar3 \to \lambda f.\ \bar2\,(\bar3\,f)$. Внутри $\bar 3\,f$ — это «применить $f$ трижды»; $\bar 2$ применяет свой аргумент дважды, значит получаем «применить трижды, потом ещё трижды» — то есть $\lambda f.\lambda x.\ f^6(x) = \bar 6$. Идея всей конструкции: число — это счётчик повторов, умножение — повтор повторов.)

Следующая точка: Кембридж — где то же самое получат, разобрав по косточкам человека с карандашом.