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

В 1941 году в своей статье “исчисление функций” американский математик Алонсо Черч предложил достаточно простой формализм для описания частично рекурсивных функций[1], а также высказал знаменитый тезис Черча, одной из формулировок которого является следующая: любая функция, вычислимая интуитивно, эквивалентна некоторой частично рекурсивной функции. При этом следует понимать, что, несмотря на слово “интуитивно”, описание алгоритма должно быть однозначным и не должно требовать от исполняющего его домысливания этого алгоритма, под интуитивным вычислением понимается лишь представление о том, что алгоритм вычисления действительно существует. Существует также деление тезиса Черча на “слабую” и “ сильную” формулировки, последняя из которых утверждает априори эквивалентность всех определений вычислимости. Тезис Черча не был, да и не может быть доказан в виду нестрогой формулировки, однако с тех пор никому так и не удалось его опровергнуть.

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

Лямбда-исчисление очень удобно для определения вычислимости. Например, Тьюринг показал, что вычислимость в терминах машины Тьюринга эквивалентна собственно возможности лямбда-описания системы. Клин доказал, что эта возможность описания также эквивалентна рекурсивности Гёделя-Гербрандта. Таким образом, если задача сформулирована с помощью лямбда-исчисления, то она имеет решение за конечное время[2].

Лямбда-исчисление оперирует следующими основными понятиями – лямбда-выражение, редукция и редекс. Лямбда-выражение – специального вида выражение, синтаксис которого с помощью формул Бэкуса-Наура можно записать так:

M ::= x | ( M₁ M₂) | (lx.M)

Где x – переменная, (M₁ M₂) – применение функции M₁ к аргументу M₂

(lx.M) – абстракция (определение функции с параметром x и телом M).

В качестве примера приведём лямбда-выражение (lx. x*x) 10.Данное выражение означает применение функции возведения в квадрат к числу 10. Такая формула называется термом. Результатом редукции этого терма, очевидно, явится число 100. В чистом лямбда-исчислении рассматриваются только переменные, абстракции и применения, оно не рассматривает никаких привязок к конкретным предметным областям. Поэтому приведённый пример (lx. x*x) 10не может считаться чистым лямбда-термом, так как содержит в себе арифметические знаки. В прикладном лямбда-исчислении допустимы константы, которые могут быть не только числовыми, но также и именами объектов и функций. Когда говорят о лямбда-исчислении, обычно имеют в виду именно прикладное лямбда-исчисление.

Для лямбда-термов вводится понятие бета-эквивалентности. M =_b N.Для приведённого выше примера можно сказать, что (lx. x*x) 10=_b10*10.В более общем виде это записывается так:

(lx.M) N =_bR

Упрощённо говоря, бета-эквивалентность означает, что левая и правая части выражения имеют одно и то же значение.

Одним из синтаксических соглашений лямбда-исчисления является то, что применение функции имеет более высокий приоритет, нежели абстракция, поэтому (lx.x y)должно рассматриваться как (lx.(x y)), т.е. определение функции x как применение x к переменной y. Также в лямбда-выражениях иногда раскрывают скобки, например, ( (x y) z)можно представить как x y z, а (x (y z)) как x (y z). При отсутствии функций применения группируются слева направо. Также выражения, содержащие несколько вложенных абстракций могут быть преобразованы к одной абстракции, например, выражение lx. ly. lz.M, может быть записано как lxyz.M

Вхождение переменной x сразу за символом l в lx.M называется связывающим вхождением или просто связыванием x. Все вхождения x в (lx.M) называются связанными в области этого связывания. Все не связанные вхождения переменных в терм являются свободными. Каждое вхождение переменной может быть либо связанным, либо свободным (не может быть и тем и другим). Надо иметь в виду, что переменная является свободной в терме, если хотя бы в одном из подтермов она является свободной, например, (lx.y) (ly.y)переменная y является свободной.

Применение функции может рассматриваться как подстановка значения, к которому она применяется, во все вхождения аргумента в тело функции. Например, (lx.x+5*x*x) mможет рассматриваться как m+m*m². Подстановка терма. Подстановка терма N вместо переменной x в терме M записывается как

{N/x} Mи определяется следующими правилами:

1.Если свободные переменные в Nне имеют связанных вхождений в M, то терм {N/x}Mполучается заменой всех свободных вхождений xв Mна N

2.Если же существует такая переменная y, которая свободна в Nи связана в M, то все связанные вхождения y в M заменяются на некоторую новую переменную z. Так продолжается до тех пор, пока не станет возможным применение предыдущего правила

Можно привести следующие примеры подстановок:

{u/x} x = u {u/x} (x x) = (u u) {u/x} (x y) = (u y) {u/x} (x u) = (u u) {(lx.x)/x} x = (lx.x)

{u/x} y = y {u/x} (y z) = (y z) {u/x} (ly.y) = (ly.y) {u/x} (lx.x) = (lx.x) {(lx.x)/x} y = y

{u/x}(lu.x) = {u/x}(lz.x) = (lz.u) {u/x}(lu.u) = {u/x}(lz.z) = (lz.z)

Точное определение подстановки таково:

– {N/x} x = N

– {N/x} y = y y¹x

– {N/x}(P Q) = {N/x} P {N/x} Q

– {N/x}(lx.P) = lx.P

– {N/x}(ly.P) = ly.{N/x}P y¹x, yÏfree(N)

– {N/x}(ly.P) = lz.{N/x}{z/y}P y¹x, zÏfree(N) zÏfree(P)

где под free(X) понимается множество свободных переменных терма X.

В основе лямбда-исчисления лежат также две аксиомы – альфа и бета.

– (lx.M) N =b {N/x}M(бета - аксиома)

– (lx.M) =blz.{z/x}M(альфа - аксиома или аксиома переименования)

Бета-аксиома утверждает бета-эквивалентность исходного терма и терма, полученного в результате подстановки. Альфа-аксиома утверждает бета-эквивалентность исходного терма и терма, в котором некоторая переменная заменена на другую, не являющуюся свободной в исходном терме. Фактически, альфа-аксиома просто позволяет переименовать переменные некоторого терма для избежания, например, конфликта имён. На основе этих аксиом доказываются следующие свойства лямбда-термов:

M =bM	Свойство идемпотентности
M =bN Þ N =bM	Свойство коммутативности
M =bN, N =bP Þ M =bP	Свойство транзистивности
A =bB, C =bD Þ A C =bB D	Свойства конгруэнтности
M =bN Þ lx.M =blx.N

Считается, что подстановка приводит терм к более простому виду. Поэтому вместе с бета-эквивалентностью вводят понятие бета-редукции (lx.M) N Þb{N/x} M.Редексом называется применение абстракции к аргументу (lx.M) N .

С понятием редекса тесно связана теорема Черча-Россера. Если ~ - отношение, то пусть ~* означает его конечно-транзитивное замыкание. Пусть X à Y означает, что X редуцируется в Y. Обозначим X cnv Y <=> X à Y или Y à X. Тогда X cnv* Y => существует такое N, что X à* N и Y à* N

Следствием этой теоремы является ромбическое свойство. Оно гласит, что если выражение A может быть редуцировано либо к B, либо к C, то всегда существует такое выражение D, к которому могут быть редуцированы и B, и C.

Если к терму нельзя применить бета-редукцию, то говорят, что он находится в нормальной форме. Например, (lx.M) N– не в нормальной форме, а x или lx.x x – в нормальной форме. Некоторые термы нельзя свести к нормальной форме. В качестве примера можно привести терм (lx.x x) (lx.x x) . Другие выражения в зависимости от стратегии вычисления могут давать или не давать результата, например, (ly.0)(( lx.x x)( lx.x x)). Существует два основных метода получения нормальной формы - вызов по значению, когда сначала производится подстановка в самых внутренних редексах, и вызов по необходимости, когда сначала производится подстановка в самом внешнем редексе (слева). Если нормальная форма достижима, то она всегда может быть получена стратегией вызова по необходимости, однако вызов по значению обычно требует меньше редукций.