Все знают Алана Тьюринга. Он создал компьютер, который помог взломать Энигму, а также заложил основы концепции искусственного интеллекта. Его знаменитый тест «проверки на вшивость» недавно прошел ChatGPT (правда, не всех это убедило, да и к самому тесту есть вопросы).
Но вот про Алонзо Чёрча, ближайшего сподвижника Тьюринга, который сыграл огромную роль в появлении современных функциональных языков программирования, как-то редко вспоминают. Мы решили исправить эту ситуацию и рассказать про этого удивительного человека.
Ранние годы Алонзо Чёрча
Будущий математический логик родился 14 июня 1903 года в ничем не примечательной семье: отец Сэмюэл Чёрч был рядовым мировым судьей в округе Колумбия, мать — домохозяйкой. Правда, более дальние родственники были довольно интересны. Его прадедушка, Алонзо Чёрч (в честь которого и назвали мальчика) был профессором математики и 30 лет занимал должность президента Университета Джорджии. А его дедушка — библиотекарем Сената США.
В 1910 году произошло событие, ключевым образом повлиявшее на всю дальнейшую жизнь Алонзо Чёрча: он играл с соседскими детьми, и один из них передал ему пневматическое ружье своего отца. Как-то получилось, что оно выстрелило в неподходящий момент, и Алонзо ослеп на один глаз. В довершение всех бед отец начал терять зрение: то ли от старости, то ли от стресса из-за переживаний о ребенке. Исполнять обязанности судьи он больше не мог, поэтому семья за уединением переехала на ферму в Вирджинию.
С деньгами проблем не возникло, поскольку помогать вызвался брат отца — его тоже звали Алонзо Чёрч, и он был преуспевающим предпринимателем. Заметив интерес мальчика к точным наукам, он помог ему устроиться в престижную частную школу в Коннектикуте.
В 1920 году Алонзо Чёрч закончил школу и поступил не куда-нибудь, а в один из самых престижных университетов страны — Принстонский. Уже на втором курсе он выигрывает престижную «премию выпуска 1861 года», вручаемую студенту, который показывает наилучшие результаты на так называемом «конкурсе Патнэма» — своеобразной математической олимпиаде для студентов ведущих вузов США.
А в 1924 году, ещё будучи студентом, он публикует статью Uniqueness of the Lorentz Transformation, где математически доказывает корректность преобразований Лоренца для одного измерения, взглянув на них под новым углом.
Становление математика и знакомство с Тьюрингом
Невероятные способности студента замечает профессор Освальд Веблен — знаменитый математик, соавтор теоремы Веблена-Янга о проективном пространстве и человек, введший понятие функций и ординалов Веблена. Веблен с 1925 года начинает активно «натаскивать» Чёрча. Результатом становятся несколько замечательных статей на широкий круг тем:
-
1925 год — On Irredundant Sets of Postulates, о многообразии математических постулатов.
-
1926 год — On the form of differential equations of a system of paths (ссылка на оригинал не сохранилась).
-
1927 год — Alternatives to Zermelo's assumption, посвященная выводам теории множеств Цермело. Кстати, эта статья легла в основу его докторской диссертации и была опубликована в журнале Transactions of the American Mathematical Society.
С 1927 по 1929 года Алонзо получает национальную стипендию и проходит стажировку сначала в Гарварде, Амстердаме, а затем в Гёттингене. Там он много работает с Дэвидом Гильбертом — человеком, который консультировал Эйнштейна в его работе над ОТО и который в 1928 году сформулировал проблему Entscheidungsproblem (с нем. «проблема принятия решения»).
Если кратко, то Гильберт изучил работы Готфрида Лейбница (создателя механической вычислительной машины в 17 веке) и задался вопросом: существует ли эффективно вычислимая и универсальная программа, которая для каждого математического утверждения будет принимать его и возвращать либо True, либо False, в зависимости от истинности утверждения, за конечное число шагов?
В 1929 году Алонзо Чёрч возвращается в Принстон и следующие 38 лет своей жизни посвящает преподаванию. Уже в 1930 году он начинает работать над Entscheidungsproblem, о которой ему подробно рассказал Гильберт. В этом деле ему помогают два одарённых студента: Стивен Клини и Дж. Баркли Россер.
В 1935 году Алонзо Чёрч шапочно знакомится с Аланом Тьюрингом, который тоже исследует Entscheidungsproblem. Есть разные точки зрения на то, обменивались ли они какой-то информацией и повлияли ли друг на друга. Но большая часть исследователей все-таки сходится в том, что Чёрч и Тьюринг работали независимо друг от друга.
Однако именно их две работы стали, пожалуй, самыми влиятельными с точки зрения дальнейшего исследования теории алгоритмов и приведших к появлению компьютеров, какими мы их знаем.
Главные работы: λ-исчисление и тезис Чёрча-Тьюринга
За несколько лет упорной работы Алонзо Чёрч вместе с Клини и Россером разработали уникальную систему математической логики, которую представили в 1936 году — λ-исчисление. Оно стало основой для появления современных функциональных языков программирования.
Если примитивно и кратко (просьба не кидаться камнями в автора), в основе идеи Чёрча лежит определение, что буквально любые математические вычисления и преобразования можно представить в виде функций. Оно базируется на двух фундаментальных операциях:
-
Абстракция — по сути объявление функции, которое обозначается символом λ. Например, λx.t, где Х — это аргумент, а t — ее тело. В современном программировании эквивалентно «анонимной функции».
-
Аппликация — применение функции. В выражении f x буква f обозначает непосредственно функцию, а x — значение аргумента.
Чёрч разработал систему кодирования, установил правила приоритета и α-эквивалентности, а также определил функции базовых логических операций and, or, not и if. В результате любых преобразований в λ-исчислении на выходе тоже должны были появляться функции: либо true ((x, y) => x), либо false ((x, y) => y). То, что и лежало в первооснове Entscheidungsproblem.
Еще Чёрч создал массу дополнительных надстроек: например, преобразовал в λ-исчисление базовые арифметические операции вроде сложения и умножения, а также натуральные числа, что позволило не ограничиваться только булевой логикой и производить полноценные вычисления. Также Чёрч ввел β-редукцию, «каррирование», рекурсивные вызовы функций с помощью Y-комбинатора (комбинатора неподвижной точки) и много чего еще.
Например, следствием разработки λ-исчисления стала теорема Чёрча-Россера, которая гласила, что «порядок применения правил редукции к термам не влияет на конечный результат. Если для некоторого λ-терма a имеется два варианта редукции a → b и a → c, то существует некоторый λ-терм d — такой, что b → d и c → d.».
Более подробно познакомиться с λ-исчислением и его сутью читатель может в замечательных статьях на том же Хабре: например, тут и тут.
Параллельно Алан Тьюринг подошел к Entscheidungsproblem с несколько иной стороны. Опираясь на «теорему о неполноте» немецкого математика Курта Гёделя (он же придумал классы рекурсивных функций и активно полемизировал с Чёрчем), Тьюринг предложил концепцию абстрактной вычислительной машины и формализовал понятие алгоритма. Свою работу он опубликовал в статье On Computable Numbers, with an Application to the Entscheidungsproblem спустя несколько месяцев после работы Чёрча.
Суть абстрактной машины заключалась в том, что есть лента бесконечной длины, разделенная на ячейки, и головка записи-чтения (ГЗЧ), которая может записывать в них символы некоторого алфавита (А) и состояний машины (Q). Положение и движение ГЗЧ влево или вправо зависит от считанного в ячейке символа и описывается правилами перехода с конечным количеством шагов. А это, по сути, и есть алгоритм.
Важно то, что Тьюринг убедительно доказал две вещи:
-
Если требуется произвести любое вычисление, которое можно описать в виде алгоритма для «машины Тьюринга», то это однозначно можно сделать, вне зависимости от сложности задачи.
-
Не существует общего алгоритма, который бы позволял только на основании входных данных сказать, что машина выдаст некий конечный результат, или будет бесконечно долго работать. Тьюринг сформулировал это как «проблему остановки».
Когда Алану Тьюрингу показали работу Чёрча, то он был поражен, что они пришли к одному и тому же выводу: Entscheidungsproblem не имеет решения. При этом решение Чёрча, хоть и считалось менее доступным и интуитивно понятным, с математической и абстрактной точки зрения было более совершенным.
Это положило начало прекрасным отношениям двух математических гениев. А утверждение о «вычислимости всего, что может быть вычислено» получило название «тезиса Чёрча-Тьюринга» — два противоположных подхода (λ-исчисления и «машина Тьюринга») имели очень схожие свойства.
В сентябре 1936 года Алан Тьюринг перебрался в Принстон и работал над докторской диссертацией на тему «Логические системы, основанные на ординалах» под руководством Алонзо Чёрча. В 1938 году Тьюринг успешно защитил ее. И параллельно изучал криптографию и разработал несколько схем электромеханического двоичного умножителя.
Во многом благодаря этому Тьюринг позже возглавил центр криптографии в Блетчли-Парке и взломал шифр «Энигмы» при помощи компьютера bombe. Но об этом написано и сказано уже очень много — если кто-то не видел, рекомендуем к просмотру фильм «Игра в имитацию» с Бенедиктом Камбербэтчем.
Наследие Алонзо Чёрча
Удивительно, что Алонзо Чёрч никогда не пользовался славой Тьюринга, Гёделя или фон Неймана, который также работал в Принстоне в те годы. Возможно, это связано с самим характером Чёрча: он был очень тихим и скромным человеком с безупречным почерком. За это все его студенты были ему очень благодарны — разбирать каракули других преподавателей на меловой доске не нравилось никому.
В 1936 году Чёрч основал журнал Symbolic Logic и был его бессменным редактором до 1979 года. В 1941 году он опубликовал книгу The Calculi of Lambda-Conversion, в которой собрал воедино все свои работы по λ-исчислению.
За время работы преподавателем в Принстоне (он уволился только в 1967 году), Алонзо Чёрч помог 31 аспиранту, многие из которых стали выдающимися математиками: Мартин Дэвис, Алан Тьюринг, Джон Джордж Кемени, Михаэль Рабин, Хартли Роджерс-младший, Рэймонд Смаллиан. И конечно те, кто помогал Чёрчу в появлении λ-исчисления: Стивен Клини и Дж. Баркли Россер.
Кроме математической логики, еще Алонзо интересовался теорией множеств, преобразованиями Лапласа, практическим применением дифференциальных уравнений и многим другим. Более подробно математические работы Чёрча приводятся на сайте Стэнфордского университета.
В 1967 году Алонзо Чёрч переходит на работу в Калифорнийский университет в Лос-Анджелесе, где трудится профессором вплоть до выхода на пенсию в 1990 году. За свою жизнь Чёрч (он умер естественной смертью в 1995 году, в почтенном возрасте 92 лет) получил множество наград: например, Британской академии, Американской академии искусств и наук и Национальной академии наук.
Но главным делом всей его жизни стало λ-исчисление. Именно оно легло в основу языка LISP, разработанного Джоном Маккарти в 1958 году и являющегося старейшим ЯП наряду с Фортраном и Коболом. А влияние λ-исчисления прослеживается в функциональных языках вроде Haskell, ML, Erlang и других.
Так что можно смело сказать, что без фундаментальной работы Алонзо Чёрча история появления компьютеров могла бы пойти по совершенно другому пути. Хотя так можно сказать и про все другие области, к которым руку приложили великие люди.
НЛО прилетело и оставило здесь промокод для читателей нашего блога:
-15% на заказ любого VDS (кроме тарифа Прогрев) — HABRFIRSTVDS
Автор: klimensky
