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

Лямбда-исчисление (Алонзо Чёрч, начало 1930х) – простая, но очень ёмкая математическая модель вычислительного устройства. Относится к классу т.н. “систем правил переписывания”, к которым также относится рассмотренная нами ранее нормализация высказываний.

Как и любая система правил переписывания, лямбда-исчисление постулирует некоторую структуру формул, а также правила (точнее, ровно одно правило) преобразования этих формул. Кроме того, поскольку лямбда-исчисление не гарантирует, что выражение когда-либо окажется в нормальной форме, существуют многочисленные способы задать порядок преобразований. При этом иногда оказывается интересен не сам результат преобразований, а промежуточные шаги.

Отметим напоследок, что в лямда-исчислении у каждого выражения существует не более одной нормальной формы. Это следует из известной теоремы Чёрча-Россера.

Грамматика

Требуется наличие одной бинарной операции (её будем обозначать * или вообще опускать) и одной унарной связывающей операции λ.

Под связывающей операцией понимается операция, в операндах которой в качестве “листьев” допускаются “привязки”. Обычно, для удобства отображения и восприятия, эти привязки обозначаются какой-нибудь буквой, хотя их не следует считать полноценными буквами. Например, формулу

λx λy x x y

следует воспринимать как

   ___________
  |           |
λ λ (_ * _) * _
|____|___|

Эта формула та же, что и, например,

λa λb a a b

Отметим, что подформула лямбды записывается между знаком “лямбда” и ближайшей закрывающей скобкой, не относящейся к этой подформуле: ровно того же соглашения придерживаются в математике при написании сумм, произведений и интегралов. Договоримся также в случаях наподобие λx λx x расставлять “привязки” из глубины наружу, то есть так: λx λy y.

Правило преобразования

В лямбда исчислении ровно одно правило преобразования: “подстановка”. Выражение вида (λx F) G разрешается заменить на F[x/G]. Последняя запись расшифровывается как: “заменить все привязки лямбды в подформуле F на формулу G”.

Ни в коем случае не следует воспринимать преобразование (λx F) G → F[x/G] буквально: рассмотрим, например, формулу

(λx λy x y) y

в которой правая y – просто буква (операция арности 0). Результатом преобразования этой формулы является

λz y z

а не λy y y, как можно было бы подумать.

Порядок вычислений

Есть два широких класса порядков вычислений (с большим количество разных вариаций): энергичный и ленивый. Основное различие – работа с выражением вида A*B.

Энергичный порядок (или, как ещё говорят, аппликативный) регламентирует следующую процедуру преобразования A*B:

Преобразовать B, получив b.
Сделать некоторые преобразования с A, получив a.
Если a=(λx F), то перейти от A*B к F[x/b] и повторить все три пункта.

Ленивый порядок отличается от аппликативного отсутствием пункта 1. При дальнейшем рассмотрении лямбда-исчисления мы будем использовать т.н. “нормализующий ленивый порядок”. Он очень прост: нужно на каждом шаге применять преобразование к самой левой лямбде среди тех, к которым можно его применить.

Есть важный (но нетривиально доказываемый) факт: “нормализующий ленивый порядок” приводит выражение к нормальной форме, если она есть.

Экстенсиональная эквивалентность

В лямбда-исчислении редко рассматривают отношение равенства на множестве формул: оно оторвано от практики. Гораздо более полезны и часто встречаются отношения нормальной эквивалентности и экстенсиональной эквивалентности.

Формулы F и G называются нормально эквивалентными, если у них одна и та же нормальная форма (или же нормальной формы нет ни у F, ни у G). При рассмотрении ненормализующих порядков вычислений под нормальной эквивалентностью обычно понимают одинаковый результат преобразования F и G: либо оба приводятся к нормальной форме, либо оба зацикливаются.

Формулы F и G называются экстенсионально эквивалентными, если для любого x выражения Fx и Gx нормально эквивалентны.

В каком-то смысле нормальная эквивалентность является экстенсиональной эквивалентностью “нулевого порядка”. Можно рассматривать и экстенсиональную эквивалентность второго порядка: F и G вторично эквивалентны, если для любого x выражения Fx и Gx экстенсионально эквивалентны.

Иногда вводят специальное обозначение ⊥ для какого-нибудь зацикливающегося выражения. Тогда высказывание о зацикивании F (логически) эквивалентно высказыванию о нормальной эквивалентности F и ⊥.

В завершение разговора об экстенсиональной эквивалентности приведём несколько примеров.

Выражения (λx x x) (λx x x) и ⊥ нормально эквивалентны.
Выражения (λx (λy y) x) и (λy y) экстенсионально эквивалентны.
Более общо, выражения λx F x и F экстенсионально эквивалентны.
А вот выражения λx (λy F y) и λx F экстенсионально эквивалентными не являются (хотя являются вторично-экстенсионально эквивалентными).
Выражения λk k k ((λx x x) (λx x x)) и (λx x x) (λx x x) нормально эквивалентны, но не экстенсионально эквивалентны: если в них подставить λx λy x, первое преобразуется в λx λy x, а второе зациклится.

Важные комбинаторы

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

Тождественным преобразованием называется выражение I = λx x.

Генератором константы называется выражение K = λx λy x.

Комбинатором подстановки называется выражение S = λa λb λx (a x) (b x).

Дупликатором называется выражение D = λx x x. Иногда его ещё обозначают буквой M.

Спаривателем называется выражение P = λa λb λc c a b.

Композитором или ассоциатором называется выражение C = λf λg λx f (g x). Можно ещё встретить обозначение B.

Транспозицией называется выражение T = λa λb b a.

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

Начнём с важнейших комбинаторов: S, K, I. Именно они находились в основе SKI-исчисления (М.Э. Шейнфинкель, начало 1920х), которое являлось непосредственным предком лямбда-исчисления. При помощи только этих трёх комбинаторов можно выразить любое лямбда-выражение. Алгоритм неожиданно прост: если обозначить {_} соответствие между лямбда-выражениями и SKI-выражениями, то

{A B}              = {A} {B}
{λ ... λ (λx x)}   = {λ ... λ I}
{λ ... λ (λy x)}   = {λ ... λ K x}
{λ ... λ (λx F G)} = {λ ... λ S {λx F} {λx G}}

Учитывая, что выражение SKK преобразуется в I, можно сделать вывод, что достаточно даже двух комбинаторов: S и K.

Остальные комбинаторы появятся в последующих разделах.

Арифметика Чёрча

Есть традиционный для лямбда исчисления способ представления целых неотрицательных чисел:

<0> = λf λx x
<1> = λf λx f x
<2> = λf λx f (f x)
<3> = λf λx f (f (f x))
...
<n> = λf λx f (f ( ... (f x)..))

Грубо говоря, выражение <n> применяет n раз свой “первый” вход ко “второму”. Нетрудно видеть, что <n> является результатом нормализации λf λx f (<n-1> f x), в связи с чем операцию “плюс один” определяют следующим образом:

(+1) = λn λf λx f (n f x)

Операцию сложения определить не сложнее:

(+) = λn n (+1)

Действительно:

(+)<m><n> → <m>(+1)<n> → (+1)((+1) ... ((+1)<n>)..) → ... → <n+m>

Умножение определяется похожим образом:

(*) = λm λn λf λx m (n f) x

или экстенсионально эквивалентным выражением

λm λn λf m (n f)

Логика Чёрча

В лямбда-исчислении при использовании ленивого порядка вычислений условное ветвление реализуется почти тривиально. “Истина” и “ложь” кодируются выражениями

<true>  = λa λb a = K
<false> = λa λb b = <0>

Само ветвление тогда реализуется выражением

<if> = λa λb λc a b с

Как видно из его определения, допустимы следующие преобразования:

<if> <true>  A B → A
<if> <false> A B → B

При помощи некоторой модификации условной конструкции можно агрегировать данные. А именно, рассмотрим выражение

pair = λa λb λc <if> c a b

В него можно запихнуть два выражения A и B конструкцией pair A B. Обратно их можно вытащить операциями

fst = λp p <true>
snd = λp p <false>

Стоит отметить, что выражение pair эквивалентно комбинатору P, упомянутому в одном из предыдущих разделов.

Как пример использования операции спаривания, покажем, как можно реализовать “псевдоминус один”, который от любого положительного числа отнимает 1, а ноль сохраняет:

shift = λp pair (snd p) ((+1) (snd p))  

(-1) = λn fst (n shift (pair <0> <0>))

Комбинатор неподвижной точки

От полноценного (точнее, полного по Тюрингу) языка программирования нас отделяет только возможность реализации управляемого зацикливания. В лямбда-исчислении управляемое зацикливание реализуется как процедура поиска неподвижных точек.

Неподвижной точкой выражения F называется выражение X, в каком-то смысле эквивалентное F X. Классический способ нахождения неподвижных точек – использование выражения

fix = λf (C f D) (C f D)

Действительно, есть следующая “цепочка” преобразований:

fix F → C F D (C F D) → F (D (C F D))

Последнее выражение нормально и экстенсионально эквивалентно F ((C F D) (C F D)) (хотя эквивалентность не совсем очевидна).

Более популярной альтернативой является комбинатор

Y = λf (λx f (x x)) (λx f (x x))

полученный из fix путём нормализации внутренних (C f D). Популярность Y-комбинатора обусловлена следующей цепочкой преобразований:

Y F → (λx F (x x)) (λx F (x x)) → F ((λx F (x x)) (λx F (x x)))

Выражение X = (λx F (x x)) (λx F (x x)) не просто является неподвижной точкой операции F, но ещё и преобразуется в F X при ленивом порядке вычислений (для аппликативного порядка вычислений Y-комбинатор бессмысленен, вместо него используется т.н. Z-комбинатор).

Теперь на примере реализации факториала покажем, как можно использовать Y-комбинатор на практике. Как известно из курса арифметики:

fac = λn <if> ((=0) n) <1> (fac ((-1) n))

Реализация операции (-1) приведена выше. Предикат (=0) можно задать выражением

(=0) = λn n (K<false>) <true>

Остаётся проблема с рекуррентной зависимостью fac от fac. Решается она так:

fac_y = Y (λf λn <if> ((=0) n) <1> (f ((-1) n)))

Если через X обозначить результат одного преобразования fac_y, то X экстенсионально эквивалентен выражению

λn <if> ((=0) n) <1> (X ((-1) n))

поэтому X вычисляет факториал поданного ему на вход числа.