Алонзо Чёрч: забытый архитектор современного программирования

Все знают Алана Тьюринга. Он создал компьютер, который помог взломать Энигму, а также заложил основы концепции искусственного интеллекта. Его знаменитый тест «проверки на вшивость» недавно прошел ^[1] ChatGPT (правда, не всех это убедило, да и к самому тесту есть вопросы). 

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

Ранние годы Алонзо Чёрча

Будущий математический логик родился 14 июня 1903 года в ничем не примечательной семье: отец Сэмюэл Чёрч был рядовым мировым судьей в округе Колумбия, мать — домохозяйкой. Правда, более дальние родственники были довольно интересны. Его прадедушка, Алонзо Чёрч ^[2] (в честь которого и назвали мальчика) был профессором математики и 30 лет занимал должность президента Университета Джорджии. А его дедушка — библиотекарем Сената США. 

В 1910 году произошло событие, ключевым образом повлиявшее на всю дальнейшую жизнь Алонзо Чёрча: он играл с соседскими детьми, и один из них передал ему пневматическое ружье своего отца. Как-то получилось, что оно выстрелило в неподходящий момент, и Алонзо ослеп на один глаз ^[3]. В довершение всех бед отец начал терять зрение: то ли от старости, то ли от стресса из-за переживаний о ребенке. Исполнять обязанности судьи он больше не мог, поэтому семья за уединением переехала на ферму в Вирджинию. 

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

В 1920 году Алонзо Чёрч закончил школу и поступил не куда-нибудь, а в один из самых престижных университетов страны — Принстонский. Уже на втором курсе он выигрывает престижную «премию выпуска 1861 года ^[4]», вручаемую студенту, который показывает наилучшие результаты на так называемом «конкурсе Патнэма ^[5]» — своеобразной математической олимпиаде для студентов ведущих вузов США.

А в 1924 году, ещё будучи студентом, он публикует статью Uniqueness of the Lorentz Transformation ^[6], где математически доказывает корректность преобразований Лоренца ^[7] для одного измерения, взглянув на них под новым углом.

Становление математика и знакомство с Тьюрингом

Невероятные способности студента замечает профессор Освальд Веблен — знаменитый математик, соавтор теоремы Веблена-Янга ^[8] о проективном пространстве и человек, введший понятие функций и ординалов Веблена ^[9]. Веблен с 1925 года начинает активно «натаскивать» Чёрча. Результатом становятся несколько замечательных статей на широкий круг тем:

• 1925 год — On Irredundant Sets of Postulates ^[10], о многообразии математических постулатов.

• 1926 год — On the form of differential equations of a system of paths (ссылка на оригинал не сохранилась).

• 1927 год — Alternatives to Zermelo's assumption ^[11], посвященная выводам теории множеств Цермело ^[12]. Кстати, эта статья легла в основу его докторской диссертации ^[13] и была опубликована в журнале Transactions of the American Mathematical Society. 

С 1927 по 1929 года Алонзо получает национальную стипендию ^[14] и проходит стажировку сначала в Гарварде, Амстердаме, а затем в Гёттингене. Там он много работает с Дэвидом Гильбертом ^[15] — человеком, который консультировал Эйнштейна в его работе над ОТО и который в 1928 году сформулировал проблему Entscheidungsproblem (с нем. «проблема принятия решения»).

Если кратко, то Гильберт изучил работы Готфрида Лейбница (создателя механической вычислительной машины в 17 веке) и задался вопросом ^[16]: существует ли эффективно вычислимая и универсальная программа, которая для каждого математического утверждения будет принимать его и возвращать либо True, либо False, в зависимости от истинности утверждения, за конечное число шагов?

В 1929 году Алонзо Чёрч возвращается в Принстон и следующие 38 лет своей жизни посвящает преподаванию. Уже в 1930 году он начинает работать над Entscheidungsproblem, о которой ему подробно рассказал Гильберт. В этом деле ему помогают два одарённых студента: Стивен Клини и Дж. Баркли Россер.

В 1935 году Алонзо Чёрч шапочно знакомится с Аланом Тьюрингом, который тоже исследует Entscheidungsproblem. Есть разные точки зрения на то, обменивались ли они какой-то информацией и повлияли ли друг на друга. Но большая часть исследователей все-таки сходится в том, что Чёрч и Тьюринг работали независимо друг от друга. 

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

Главные работы: λ-исчисление и тезис Чёрча-Тьюринга

За несколько лет упорной работы Алонзо Чёрч вместе с Клини и Россером  разработали уникальную систему математической логики, которую представили в 1936 году — λ-исчисление ^[17]. Оно стало основой для появления современных функциональных языков программирования. 

Если примитивно и кратко (просьба не кидаться камнями в автора), в основе идеи Чёрча лежит определение, что буквально любые математические вычисления и преобразования можно представить в виде функций. Оно базируется на двух фундаментальных операциях:

• Абстракция — по сути объявление функции, которое обозначается символом λ. Например, λx.t, где Х — это аргумент, а t — ее тело. В современном программировании эквивалентно «анонимной функции». 

• Аппликация — применение функции. В выражении f x буква f обозначает непосредственно функцию, а x — значение аргумента. 

Чёрч разработал систему кодирования ^[18], установил правила приоритета и α-эквивалентности, а также определил функции базовых логических операций and, or, not и if. В результате любых преобразований в λ-исчислении на выходе тоже должны были появляться функции: либо true ((x, y) => x), либо false ((x, y) => y). То, что и лежало в первооснове Entscheidungsproblem. 

Еще Чёрч создал массу дополнительных надстроек: например, преобразовал в λ-исчисление базовые арифметические операции вроде сложения и умножения, а также натуральные числа, что позволило не ограничиваться только булевой логикой и производить полноценные вычисления. Также Чёрч ввел β-редукцию, «каррирование», рекурсивные вызовы функций с помощью Y-комбинатора (комбинатора неподвижной точки) ^[19] и много чего еще. 

Например, следствием разработки λ-исчисления стала теорема Чёрча-Россера ^[20], которая гласила, что «порядок применения правил редукции к термам не влияет на конечный результат. Если для некоторого λ-терма a имеется два варианта редукции a → b и a → c, то существует некоторый λ-терм d — такой, что b → d и c → d.».

Более подробно познакомиться с λ-исчислением и его сутью читатель может в замечательных статьях на том же Хабре: например, тут ^[21] и тут ^[22].  

Параллельно Алан Тьюринг подошел к Entscheidungsproblem с несколько иной стороны. Опираясь на «теорему о неполноте» ^[23] немецкого математика Курта Гёделя (он же придумал классы рекурсивных функций ^[24] и активно полемизировал с Чёрчем), Тьюринг предложил концепцию абстрактной вычислительной машины и формализовал понятие алгоритма. Свою работу он опубликовал в статье On Computable Numbers, with an Application to the Entscheidungsproblem ^[25] спустя несколько месяцев после работы Чёрча. 

Суть абстрактной машины ^[26] заключалась в том, что есть лента бесконечной длины, разделенная на ячейки, и головка записи-чтения (ГЗЧ), которая может записывать в них символы некоторого алфавита (А) и состояний машины (Q). Положение и движение ГЗЧ влево или вправо зависит от считанного в ячейке символа и описывается правилами перехода с конечным количеством шагов. А это, по сути, и есть алгоритм. 

Важно то, что Тьюринг убедительно доказал две вещи:

• Если требуется произвести любое вычисление, которое можно описать в виде алгоритма для «машины Тьюринга», то это однозначно можно сделать, вне зависимости от сложности задачи. 

• Не существует общего алгоритма, который бы позволял только на основании входных данных сказать, что машина выдаст некий конечный результат, или будет бесконечно долго работать. Тьюринг сформулировал это как «проблему остановки» ^[27].

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

Это положило начало прекрасным отношениям двух математических гениев. А утверждение о «вычислимости всего, что может быть вычислено» получило название «тезиса Чёрча-Тьюринга» ^[28] — два противоположных подхода (λ-исчисления и «машина Тьюринга») имели очень схожие свойства. 

В сентябре 1936 года Алан Тьюринг перебрался в Принстон и работал над докторской диссертацией на тему «Логические системы, основанные на ординалах» под руководством Алонзо Чёрча. В 1938 году Тьюринг успешно защитил ее. И параллельно изучал криптографию и разработал несколько схем электромеханического двоичного умножителя. 

Во многом благодаря этому Тьюринг позже возглавил центр криптографии в Блетчли-Парке и взломал шифр «Энигмы» при помощи компьютера bombe ^[29]. Но об этом написано и сказано уже очень много — если кто-то не видел, рекомендуем к просмотру фильм «Игра в имитацию» с Бенедиктом Камбербэтчем. 

Наследие Алонзо Чёрча

Удивительно, что Алонзо Чёрч никогда не пользовался славой Тьюринга, Гёделя или фон Неймана, который также работал в Принстоне в те годы. Возможно, это связано с самим характером Чёрча: он был очень тихим и скромным человеком с безупречным почерком. За это все его студенты были ему очень благодарны — разбирать каракули других преподавателей на меловой доске не нравилось никому.

В 1936 году Чёрч основал журнал Symbolic Logic и был его бессменным редактором до 1979 года. В 1941 году он опубликовал книгу The Calculi of Lambda-Conversion ^[30], в которой собрал воедино все свои работы по λ-исчислению. 

За время работы преподавателем в Принстоне (он уволился только в 1967 году), Алонзо Чёрч помог 31 аспиранту, многие из которых стали выдающимися математиками: Мартин Дэвис ^[31], Алан Тьюринг, Джон Джордж Кемени ^[32], Михаэль Рабин ^[33], Хартли Роджерс-младший ^[34], Рэймонд Смаллиан ^[35]. И конечно те, кто помогал Чёрчу в появлении λ-исчисления: Стивен Клини ^[36] и Дж. Баркли Россер ^[37]. 

Кроме математической логики, еще Алонзо интересовался теорией множеств ^[38], преобразованиями Лапласа ^[39], практическим применением дифференциальных уравнений и многим другим. Более подробно математические работы Чёрча приводятся на сайте ^[40] Стэнфордского университета. 

В 1967 году Алонзо Чёрч переходит на работу в Калифорнийский университет в Лос-Анджелесе, где трудится профессором вплоть до выхода на пенсию в 1990 году. За свою жизнь Чёрч (он умер естественной смертью в 1995 году, в почтенном возрасте 92 лет) получил множество наград: например, Британской академии, Американской академии искусств и наук и Национальной академии наук. 

Но главным делом всей его жизни стало λ-исчисление. Именно оно легло в основу языка LISP ^[41], разработанного Джоном Маккарти в 1958 году и являющегося старейшим ЯП наряду с Фортраном и Коболом. А влияние λ-исчисления прослеживается в функциональных языках вроде Haskell, ML, Erlang и других.

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

НЛО прилетело и оставило здесь промокод для читателей нашего блога:

-15% на заказ любого VDS ^[42] (кроме тарифа Прогрев) — HABRFIRSTVDS