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

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

Понятие вычислимости — очень важная и красивая математическая идея. Примечателен также и ее малый возраст в сравнении с другими столь же фундаментальными математическим проблемами: она была впервые выдвинута только в 1930-х годах. Эта проблема имеет отношение ко всем областям математики (хотя, справедливости ради, отметим, что большинство математиков пока не часто обращаются к вопросам вычислимости). Сила этой идеи связана отчасти с существованием четко определенных и все же неразрешимых математических операций (как, например, проблема остановки машины Тьюринга и некоторые другие, которые мы рассмотрим в главе 4). Если бы не было таких невычислимых объектов, то теория алгоритмической разрешимости не представляла бы особого интереса для математики. В конце концов, математики любят головоломки.

Задача о разрешимости определенной математической операции может их заинтриговать, особенно потому, что общее решение этой головоломки само по себе алгоритмически не разрешимо.

Следует сделать еще одно замечание. Вычислимость — это по-настоящему «абсолютная» математическая идея. Это абстрактное понятие, которое никак не зависит от какой-либо конкретной реализации в терминах «машин Тьюринга» в том виде, как я их описал выше. Как я уже указывал, нет необходимости придавать какое-либо специальное значение «лентам», «внутренним состояниям» и т. п., характерным для гениального, но тем не менее частного подхода Тьюринга. Существуют также и другие способы выражения идеи вычислимости, причем исторически первым было «лямбда-исчисление», предложенное американским логиком Алонзо Черчем совместно со Стивеном Клини. Процедура, предложенная Черчем, значительно отличалась от метода Тьюринга и была гораздо более абстрактна. Фактически, форма, в которой Черч изложил свою теорию, делала связь между ними и чем бы то ни было «механическим» совсем не очевидной. Главная идея, лежащая в основе процедуры Черча, абстрактна по своей сути — это математическая операция, которую сам Черч назвал «абстрагированием».

Мне кажется, что стоит привести краткое описание схемы Черча не только потому, что она подчеркивает математическую природу идеи вычислимости, не зависящую от конкретного понятия вычислительной машины, но и потому, что она иллюстрирует мощь абстрактных идей в математике. Читатель, не достаточно свободный в математике и не увлеченный излагаемыми математическими идеями как таковыми, скорее всего предпочтет сейчас перейти к следующей главе — и не утратит при этом нить рассуждений. Тем не менее я полагаю, что таким читателям будет небесполезно следовать за мной еще какое-то время и оценить чудесную по своей стройности и продуманности схему Черча (см. Черч [1941]).

В рамках этой схемы рассматривается «универсальное множество» различных объектов, обозначаемых, скажем, символами

каждый из которых представляет собой математическую операцию, или функцию. (Штрихованные буквы позволяют создавать неограниченные наборы символов для обозначения таких функций.) «Аргументы» этих функций, т. е. объекты, на которые эти функции действуют, в свою очередь являются объектами той же природы, т. е. функциями. Более того, результат действия одной функции на другую (ее «значение») также представляет собой функцию. (Поистине, в системе Черча наблюдается замечательная экономия понятий.) Поэтому, когда мы пишем[56]

а = bс,

мы подразумеваем, что функция b, действуя на функцию c, дает в результате другую функцию а. В рамках этой схемы нетрудно сформулировать понятие функции двух или более переменных. Если мы хотим представить f как функцию двух переменных, скажем р и q, то мы можем просто написать

(fp)q

(что есть результат действия функции fp на функцию q ). Для функции трех переменных можно использовать выражение

((fp)q)r

и так далее.

Теперь мы можем перейти к описанию важнейшей операции абстрагирования. Для нее мы будем использовать греческую букву ? (лямбда). Непосредственно за ней будет следовать символ одной из функций Черча, скажем х, который мы будем рассматривать как «фиктивную переменную». Каждое появление х в квадратных скобках, следующих сразу за этим выражением, обозначает теперь просто место, куда подставляется все, что идет за всем этим выражением. Таким образом, когда мы пишем

?x. [fx],

мы подразумеваем функцию, которая при действии на, например, а имеет значение fа, т. е.

(?х. [fx ])a = fа.

Другими словами, ?х. [fх] — это просто функция f, т. е.

?х. [fх ] = f.

Сказанное выше требует определенного осмысления. Это одна из тех математических тонкостей, которые на первый взгляд кажутся настолько педантичными и тривиальными, что их смысл часто совершенно ускользает от понимания. Рассмотрим пример из знакомой всем школьной математики. Примем за f тригонометрическую функцию — синус угла. Тогда абстрактная функция «sin» будет определяться выражением

?х. [sin х ] = sin.

(Не придавайте большого значения тому, что в качестве «функции» х может фигурировать величина угла. Мы скоро увидим, каким образом числа можно иногда рассматривать как функции, а величина угла — это просто число.) До сих пор все на самом деле тривиально. Однако представим себе, что обозначение «sin» не было изобретено, но нам известно о существовании представления sin х в форме степенного ряда:

Тогда мы могли бы ввести определение

Можно было поступить еще проще и определить, например, операцию «одна шестая куба», для которой не существует стандартного «функционального» обозначения:

Тогда, например,

К обсуждаемым проблемам большее отношение имеют выражения, составленные просто из элементарных функциональных операций Черча, таких как

?f.[f (fx)]

Это функция, которая, действуя на другую функцию, скажем g, дает дважды итерированную g, действующую на x

(?f.[f (fx)])g = g(gx) .

Мы могли бы сначала «абстрагироваться» от x и рассмотреть выражение

?f. [?х. [f (fх)]],

которое можно сократить до

?fx. [f (fx)].

Это и есть операция, применение которой к g дает функцию «вторая итерация g». По сути, это та самая функция, которую Черч обозначил номером 2 :

2 = ?fx.[f (fx)],

так что (2g) y = g (gy). Аналогичным образом он определил:

3 = ? fx. [f (f (fx))],

4 = ?fх. [f (f (f (fx)))], и т. д.,

а также

1 = ?fх. [fх] и 0 = ? fx.

[x].

Видно, что 2 Черча больше похоже на «дважды», 3 — на «трижды» и т. д. Значит, действие 3 на функцию f, т. е. 3f равносильно операции «применить f три раза», поэтому 3f при действии на у превращается в

(3f)y = f (f (f (y))) -

Посмотрим, как в схеме Черча можно представить очень простую математическую операцию — прибавление 1 к некоторому числу. Определим операцию

S = ?abc. [b ((аb)с)].

Чтобы убедиться, что S действительно прибавляет 1 к числу в обозначениях Черча, проверим ее действие на 3 :

поскольку (3b)с = b (b (bc)). Очевидно, эта операция с таким же успехом может быть применена к любому другому натуральному числу Черча. (В действительности, операция

?аbс. [(аb)(bс)] приводит к тому же результату, что и S.)

А как насчет удвоения числа? Удвоение числа может быть получено с помощью операции

что легко видеть на примере ее действия на 3 :

Фактически, основные арифметические операции — сложение, умножение и возведение в степень могут быть определены, соответственно, следующим образом:

А = ?fgxy. [((fx)(gx))y],

М = ?fgx. [f (gx)],

P = ?fg. [fg]

Читатель может самостоятельно убедиться (или же принять на веру), что

(Am) n = m + n,

(Mm) n = m x n,

(Pm) n = n^m,

где m и n — функции Черча для двух натуральных чисел, m + n — функция, выражающая их сумму, и т. д. Последняя из этих функций поражает больше всего. Посмотрим, например, что она дает в случае m = 2, n = 3:

Операции вычитания и деления определяются не так легко (на самом деле нам потребуется соглашение о том, что делать с (m — n ), когда m меньше n, и с (m/n ), когда m не делится на n ). Решающий шаг в развитии этого метода был сделан в начале 1930-х годов, когда Клини удалось найти выражение для операции вычитания в рамках схемы Черча! Затем были описаны и другие операции. Наконец, в 1937 году Черч и Тьюринг независимо друг от друга показали, что всякая вычислимая (или алгоритмическая) операция — теперь уже в смысле машин Тьюринга — может быть получена в терминах одного из выражений Черча (и наоборот).

Это воистину замечательный факт, который подчеркивает глубоко объективный и математичный характер понятия вычислимости. На первый взгляд, понятие вычислимости по Черчу не связано с вычислительными машинами. И тем не менее, оно имеет непосредственное отношение к практическим аспектам вычислений. В частности, мощный и гибкий язык программирования LISP включает в себя как существенный элемент основные структуры исчисления Черча.

Как я отмечал ранее, существуют и другие способы определения понятия вычислимости. Несколько позже, но независимо от Тьюринга, Пост предложил во многом сходную концепцию вычислительной машины. Тогда же благодаря работам Дж. Хербранда и Геделя появилось и более практичное определение вычислимости (рекурсивности). X. Б. Карри в 1929 году, и ранее, в 1924, М. Шенфинкель, предложили иной подход, который был отчасти использован Черчем при создании своего исчисления (см. Ганди [1988]). Современные подходы к проблеме вычислимости (такие как машина с неограниченным регистром, описанная Катлендом [1980]) в деталях значительно отличаются от разработанного Тьюрингом и более пригодны для практического использования. Однако понятие вычислимости во всех этих подходах остается неизменным.

Как и многие другие математические идеи, особенно наиболее фундаментальные и красивые, идея вычислимости кажется овеществленной и объективно существующей в платоновском смысле. Именно к этому мистическому вопросу о платоновской реальности математических понятий мы и обратимся в следующих двух главах.

Данный текст является ознакомительным фрагментом.