Алонзо Чёрч

Алонзо Чёрч (англ. Alonzo Church; 14 июня 1903, Вашингтон — 11 августа 1995, Хадсон) — американский математик и логик, внёсший фундаментальный вклад в основания математики, теорию вычислимости и математическую логику. Чёрч наиболее известен как создатель λ-исчисления (лямбда-исчисления), формальной системы, ставшей концептуальной основой для языков функционального программирования, а также как автор тезиса Чёрча — Тьюринга, определяющего интуитивное понятие эффективно вычислимой функции.

Биография

Алонзо Чёрч родился 14 июня 1903 года в Вашингтоне, округ Колумбия. Его отец, Сэмюэл Роббинс Чёрч, был судьёй, а мать, Милдред Линдси Чёрч, занималась домашним хозяйством. После смерти отца в 1914 году семья переехала в Виргинию.

Чёрч проявил выдающиеся способности к математике ещё в школе. Он поступил в Принстонский университет, где в 1924 году получил степень бакалавра искусств, а в 1927 году — докторскую степень (Ph.D.) под руководством Освальда Веблена. Его диссертация была посвящена аксиомам теории множеств.

После окончания Принстона Чёрч стажировался в Гарвардском университете, а затем в 1927—1929 годах — в Гёттингене и Голландии, где работал, в частности, с Давидом Гильбертом. В 1929 году он вернулся в Принстон в качестве доцента, а в 1939 году стал профессором.

В годы Второй мировой войны Чёрч работал в Лаборатории баллистических исследований Армии США в Абердине. После войны он вернулся в Принстон, где оставался до 1967 года. В 1967 году он перешёл на работу в Калифорнийский университет в Лос-Анджелесе (UCLA), где преподавал до 1990 года, а в последующем — вплоть до смерти (1995) — работал в статусе почётного профессора.

Алонзо Чёрч был плодовитым редактором. С 1936 года он был редактором Journal of Symbolic Logic, а с 1971 года — одним из главных редакторов Journal of Symbolic Logic. Он также основал и редактировал Annual Review of Symbolic Logic. Чёрч был избран членом Национальной академии наук США (1949), Американской академии искусств и наук (1953) и Американского математического общества (1964). Он получил почётные докторские степени от нескольких университетов, включая Университет Нотр-Дам (1978).

Он скончался 11 августа 1995 года в Хадсоне, штат Огайо, на 93-м году жизни.

Научный вклад

Лямбда-исчисление

Основной и наиболее известной работой Чёрча является создание λ-исчисления — формальной математической системы, предназначенной для определения функций и их вычисления. Он впервые представил её в 1932 году в статье «A Set of Postulates for the Foundation of Logic» (Набор постулатов для оснований логики). Целью Чёрча было создание универсальной логической системы, в которой все математические конструкции могли бы быть представлены как функции.

λ-исчисление оперирует тремя конструкциями:

• λ-абстракция: построение функции вида λx.M, где x — аргумент, а M — тело функции.
• Применение (аппликация): применение функции к аргументу.
• Переменные.

Система оказалась достаточно выразительной: в ней можно было определить натуральные числа (числа Чёрча), арифметические операции, логические значения и условные выражения, рекурсию. В 1936 году Чёрч и его студент Стивен Клини доказали, что λ-исчисление является универсальной моделью вычислений — любая вычислимая функция может быть реализована в этой системе. Это привело к формулировке тезиса Чёрча.

В 1936 году Чёрч также показал, что в λ-исчислении существует неразрешимая задача — проблема остановки (проблема распознавания останова). Он доказал, что не существует алгоритма, который мог бы определить для произвольного λ-выражения, завершится ли его вычисление. Это был один из первых результатов о неразрешимости в математической логике.

λ-исчисление стало концептуальной основой для разработки языков функционального программирования, таких как Lisp (1958), Scheme (1975) и Haskell (1990). Оно также широко используется в теории доказательств и семантике языков программирования.

Тезис Чёрча — Тьюринга

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

Этот тезис не является формально доказуемой теоремой, а представляет собой эмпирическое обобщение, которое до сих пор не опровергнуто. Он служит основой для определения понятия алгоритма: функция называется вычислимой (или рекурсивной), если её можно реализовать на некоторой модели вычислений, эквивалентной λ-исчислению или машине Тьюринга.

Тезис был сформулирован в 1936 году Чёрчем в работе «An Unsolvable Problem of Elementary Number Theory» (Неразрешимая проблема элементарной теории чисел), а Тьюринг пришёл к аналогичному выводу в работе «On Computable Numbers, with an Application to the Entscheidungsproblem» (О вычислимых числах в применении к проблеме разрешения). Чёрч первым признал приоритет Тьюринга в этом вопросе и предложил название «тезис Чёрча — Тьюринга», хотя сам предпочитал термин «тезис Чёрча — Тьюринга».

Проблема разрешения (Entscheidungsproblem)

В 1936 году Чёрч (и независимо Тьюринг) дал отрицательный ответ на проблему разрешения, поставленную Давидом Гильбертом. Гильберт спрашивал, существует ли общий алгоритм, который для данной формулы логики первого порядка определяет, является ли она общезначимой (т.е. истинной во всех интерпретациях). Чёрч доказал, что такого алгоритма не существует, используя приёмы, позднее лёгшие в основу теорем Гёделя о неполноте. Этот результат, известный как теорема Чёрча, является одним из фундаментальных результатов математической логики.

Прочие работы

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

Известные ученики

Алонзо Чёрч был одним из ведущих диссертационных руководителей в XX веке. Среди его наиболее известных учеников:

• Алан Тьюринг (1922—1954) — кембриджский логик, работавший под руководством Чёрча в Принстоне в 1936—1938 годах. Получил степень доктора в 1938 году за работу «Systems of Logic Based on Ordinals».
• Стивен Клини (1909—1994) — американский логик, основатель теории рекурсивных функций.
• Дана Скотт (род. 1924) — американский логик, лауреат премии Тьюринга (1976) за вклад в теорию денотационной семантики.
• Роберт Константайн — американский логик, внёсший вклад в теорию двухосновных систем.

Всего Чёрч подготовил более 50 докторов наук.

Признание

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

• Премия Лейбница (1950) за вклад в логику.
• Премия Тьюринга (1969) за вклад в основания математики и теорию вычислений.
• Медаль науки (1978) — высшая научная награда США.
• Премия Шовене (1984) за выдающиеся работы по логике и математике.

В честь Чёрча названа Премия Алонзо Чёрча, присуждаемая Европейской ассоциацией теоретической информатики (EATCS) за выдающиеся результаты в области теоретической информатики. Также его имя носит тип данных «Алгебраический тип Чёрча» (Church encoding) и «Числа Чёрча» — стандартная кодировка натуральных чисел в λ-исчислении.

Основные публикации

Книги

• Introduction to Mathematical Logic (1956) — фундаментальный учебник, выдержавший несколько переизданий (2-е изд. 1962, 3-е изд. 1966, 4-е изд. 1972, 5-е изд. 1976).
• The Calculi of Lambda-Conversion (1941) — классическая монография, посвящённая λ-исчислению.
• A Bibliography of Symbolic Logic (1938) — библиографический справочник, долгое время остававшийся основным в этой области.

Избранные статьи

• 1932: «A set of postulates for the foundation of logic». Annals of Mathematics 33 (2): 346–366.
• 1936: «An unsolvable problem of elementary number theory». American Journal of Mathematics 58 (2): 345–363.
• 1936: «A note on the Entscheidungsproblem». Journal of Symbolic Logic 1 (1): 40–41.
• 1940: «A formulation of the simple theory of types». Journal of Symbolic Logic 5 (2): 102–116.

Источники

• Church, Alonzo. The Calculi of Lambda-Conversion. Princeton University Press, 1941.
• Church, Alonzo. Introduction to Mathematical Logic. Princeton University Press, 1956.
• Mitchell, John C. Foundations for Programming Languages. MIT Press, 1996.
• Barendregt, Henk. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1984.
• Kleene, Stephen C. «Alonzo Church». Journal of Symbolic Logic, Vol. 60, No. 4, 1995, pp. 1069–1071.
• Gandy, Robin. «Alonzo Church (1903—1995)». Nature, Vol. 378, 1995, p. 450.