Теперь давайте рассмотрим проблемы λ-исчисления. Одна из проблем — чисто техническая, да и вы, наверное, ее уже замечали выше по тексту. Пусть у нас есть какое-нибудь хитрое выражение, например:
(\y. y y) (\f. \x. f x)
Если попробовать делать β-редукции втупую, подстановкой, то получится:
(\y. y y) (\f. \x. f x) -> -> (\f. \x. f x) (\f. \x. f x) -> -> \x. (\f. \x. f x) x -> -> \x. \x. x x
Появляется проблема: в конце непонятно, к чему относится каждая переменная — к параметру внешней или внутренней λ-функции.
Такая проблема возникает, когда у аргумента есть свободные переменные, которые после подстановки ошибочно оказываются связанными не с той λ-функцией. Чтобы этого избежать, можно совершать дополнительные переименования во время вычислений.
Но что, если бы мы смогли избавиться от переменных?
Как известно, в λ-исчислении есть много комбинаторов, то есть функций, не использующих внешние переменные. С Y-комбинатором мы уже знакомы, введем еще три, на этот раз гораздо более простых:
S := \f. \g. \x. (f x) (g x) K := \x. \y. x I := \x. x
I — самый простой комбинатор, возвращающий свой аргумент.
K — уже известный нам как true комбинатор, который принимает два аргумента и всегда возвращает первый.
S — что-то новое. Его смысл можно понять так: если написать, скажем, f (g x), то аргумент x получит только функция g, а не функция f. Если расставить скобки по-другому или поменять местами аргументы — все равно аргумент x получит только одна функция. А если мы хотим его передать обоим функциям? Для этого и нужен этот комбинатор: S f g x =b (f x) (g x).
Так вот, оказывается, что абсолютно любой терм выражается как комбинация этих термов, вообще без создания новых функций через \x.! Следите за руками.
Мы будем мысленно брать выражение и рекурсивно переписывать его на комбинацию комбинаторов (ну, вы поняли). Выражение это может выглядеть совершенно по-разному.
Пусть, например, оно имеет такой вид: \x. E1 E2 (x, конечно, может участвовать в обоих подвыражениях). Его мы перепишем следующим образом: \t. ((\x. E1) t) ((\x. E2) t). Таким образом мы как бы проталкиваем \x. внутрь двух выражений. Теперь заметим, что это можно переписать через комбинатор S: S (\x. E1) (\x. E2). Например:
\x. 5 (succ x) =b S (\x. 5) (\x. succ x)
Для того, чтобы до конца преобразовать это выражение в SKI-базис, мы рекурсивно запустимся от \x. 5 и \x. succ x, и так далее. Формально:
rewrite[\x. E1 E2] := S rewrite[\x. E1] rewrite[\x. E2]
Вообще, давайте до конца поймем, как преобразуются определения функций. С \x. E1 E2 все ясно, еще возможен вариант \x. \y. E, где E зависит и от x, и от y. Тогда мы сначала преобразуем \y. E в SKI-базис и получим выражение вроде \x. E2, где теперь в E2 уж точно нет определений функций — итого, свели к первому случаю.
rewrite[\x. \y. E] := rewrite[\x. rewrite[\y. E]]
Осталось два исключения: \x. x и \x. t.
\x. x — это просто I-комбинатор:
rewrite[\x. x] := I
И последний вариант — когда функция есть, а ее параметр не используется. Например, как \x. t в примере выше. Иначе говоря, мы хотим выразить константную функцию. На самом деле, этим и занимается K-комбинатор: \x. t =b K t.
rewrite[\x. t] := K rewrite[t]
Все варианты вида \x. E уже разобраны, остались варианты вне функций. Первый — E1 E2, тут все просто:
rewrite[E1 E2] := rewrite[E1] rewrite[E2]
Ну и наконец, вообще самый базовый случай, когда выражение никак не раскладывается на подтермы, потому что оно является одной переменной:
rewrite[x] := x
Вообще говоря, при таких тупых заменах может образоваться что-то вроде \x. f x, что раскроется как
rewrite[\x. f x] = S rewrite[\x. f] rewrite[\x. x] = S (K f) I
в то время как f — гораздо более короткое решение, поэтому нередко к этим же пунктам добавляют η-преобразование.
Хотите потренироваться и преобразовать в SKI-базис Y-комбинатор? Нет? А я хочу. Для краткости возьмем асимметричный Y-комбинатор.
rewrite[Y] = = rewrite[\f. (\x. x x) (\x. f (x x))] = = S rewrite[\f. \x. x x] rewrite[\f. \x. f (x x)] = = S (K rewrite[\x. x x]) rewrite[\f. \x. f (x x)] = = S (K (S rewrite[\x. x] rewrite[\x. x])) rewrite[\f. \x. f (x x)] = = S (K (S I I)) rewrite[\f. \x. f (x x)] = = S (K (S I I)) rewrite[\f. rewrite[\x. f (x x)]] = = S (K (S I I)) rewrite[\f. S rewrite[\x. f] rewrite[\x. x x]] = = S (K (S I I)) rewrite[\f. S (K f) rewrite[\x. x x]] = = S (K (S I I)) rewrite[\f. S (K f) (S rewrite[\x. x] rewrite[\x. x])] = = S (K (S I I)) rewrite[\f. S (K f) (S I I)] = = S (K (S I I)) (S rewrite[\f. S (K f)] rewrite[\f. (S I I)]) = = S (K (S I I)) (S rewrite[\f. S (K f)] (K (S I I))) = = S (K (S I I)) (S (S rewrite[\f. S] rewrite[\f. K f]) (K (S I I))) = = S (K (S I I)) (S (S (K S) rewrite[\f. K f]) (K (S I I))) = = S (K (S I I)) (S (S (K S) K) (K (S I I)))
Красота.
Да, кстати, кроме SKI-базиса исследуется также SK-базис. Дело в том, что комбинатор I можно выразить через комбинаторы S и K.
Как ни удивительно, самый простой терм \x. x выражается в SK-базисе не так очевидно. Чтобы понять, как тут быть, заметим, что \x. x =b \x. K x (...), где ... — произвольный терм. Для симметрии пусть ... := K x, тогда \x. x =b \x. (K x) (K x). Что-то очень похожее с распределением аргумента мы видели раньше — в S-комбинаторе. И правда: \x. x =b S K K.
С помощью этого мы можем упростить SKI-базис до SK-базиса. Y-комбинатор в нем записывается так:
S (K (S (S K K) (S K K))) (S (S (K S) K) (K (S (S K K) (S K K))))
Шо, опять? Да, можно еще эффективнее. У нас уже есть базис из двух комбинаторов, так давайте построим базис из одного комбинатора. Засунем S и K в один ι-комбинатор в виде пары:
i := pair S K -> \f. f S K
Теперь у нас есть только ι, так что давайте просто переберем варианты комбинации йот.
i i -> -> (\f. f S K) i -> -> i S K -> -> (\f. f S K) S K -> -> (S S K) K -> -> (S K) (K K) -> -> \y. S K (K K) y -> -> \y. (K y) (K K y) -> -> \y. (\x. y) (K K y) -> -> \y. y -> -> I
Неожиданно, но приятно. Ясно, что (i i) i -> I i -> i особо бесполезно, так что попробуем теперь группировать скобки по-другому.
i (i i) -> -> i I -> -> I S K -> -> S K
Это ни на что не похоже, давайте еще накинем йот.
i (i (i i)) -> -> i (S K) -> -> S K S K -> -> (K K) (S K) -> -> K
Интересно. Еще одну йоту?
i (i (i (i i))) -> -> i K -> -> K S K -> -> S
Да, это было хорошей идеей. Пожалуйста, вот вам S, K, I комбинаторы в ι:
S =b i (i (i (i i))) K =b i (i (i i)) I =b i i
Таким образом, применяя ι-комбинатор в различных комбинациях, можно выразить любой терм.
Ну как, хотите Y-комбинатор в ι-базисе?
(i (i (i (i i)))) ((i (i (i i))) ((i (i (i (i i)))) (i i) (i i))) ((i (i (i (i i)))) ((i (i (i (i i)))) ((i (i (i i))) (i (i (i (i i))))) (i (i (i i)))) ((i (i (i i))) ((i (i (i (i i)))) (i i) (i i))))
А как вам ι-язык? Выражение, записанное в ι-базисе — это, по сути, бинарное дерево. Листья — собственно ι-комбинаторы, остальные вершины — вызовы функций. Если в листы записать единицы, а в остальные вершины — нули, а потом пройтись по этому дереву dfs'ом и выписать цифры в вершинах, получится выражение на ι-языке. Например, i (i i) кодируется как 01011. А вот как кодируется Y-комбинатор:
00010101011001010110001010101101101100010101011000101010110010101101010101101010110010101100010101011011011