Комбинаторная логика: S, K, I и программирование без переменных

Оглянитесь на пройденный трек и спросите себя: что в лямбда-исчислении было по-настоящему сложным? Не абстракция — это x => .... Не аппликация — это вызов. Сложными были имена: свободные и связанные переменные (https://courses.digitable.life/post/lambda-calculus/02-variables-and-substitution/), захват при подстановке, альфа-переименование (https://courses.digitable.life/post/lambda-calculus/03-reductions/), генерация свежих имён, индексы де Брёйна. Вся механическая грязь исчисления — про имена, и ни про что больше.

Отсюда естественный вопрос: а нельзя ли выбросить переменные совсем? Не «сделать удобнее», а именно выбросить — так, чтобы в языке не осталось ни одного связывателя, ни одного λ, и подстановка перестала существовать как понятие.

Ответ: можно. Причём выяснили это раньше, чем появилось само лямбда-исчисление: Моисей Шейнфинкель доложил свою конструкцию в Гёттингене в 1920 году (опубликовано в 1924-м), Хаскелл Карри развил её в 1930-х, а Чёрч опубликовал лямбда-исчисление в 1932-м. Дисциплина называется комбинаторной логикой, и в ней всё программирование сводится к трём константам.

Идея: функция без параметров

Комбинатор — это замкнутый терм, то есть терм без свободных переменных (https://courses.digitable.life/post/lambda-calculus/02-variables-and-substitution/). λx. x — комбинатор. λx. x y — нет, y торчит наружу. Смысл слова простой: комбинатор ничего не берёт из контекста, он самодостаточен и только комбинирует то, что ему дали.

Идея комбинаторной логики: зафиксировать несколько таких комбинаторов как константы языка и запретить писать λ вообще. Тогда терм — это либо константа, либо применение терма к терму. Всё.

терм ::= S | K | I          (1) константы-комбинаторы
       | x                  (2) переменная (только свободная, связывать нечем)
       | (терм терм)        (3) аппликация

Обратите внимание на пункт (2): переменные в записи остаются, но связать их нечем — конструкции «λ» в грамматике просто нет. Значит, любая переменная в терме свободна, а вопрос «попадёт ли она под чужой связыватель» не может даже возникнуть. Захват имён исчез вместе с самим понятием связывания.

Правила вычисления задаются не подстановкой, а тремя правилами переписывания:

I x     →  x                 — тождество
K x y   →  x                 — выбросить второй аргумент
S x y z →  x z (y z)         — раздать z обоим и применить

Скобки, как и раньше, левоассоциативны: S x y z — это (((S x) y) z) (https://courses.digitable.life/post/lambda-calculus/01-syntax/).

Прочитаем правила как код. I — это identity. K — это const: берёт значение и возвращает функцию, которая его отдаёт, что бы ей ни подсунули. S — единственный нетривиальный: он распределяет общий аргумент по двум функциям и склеивает результат. На JavaScript и Python это буквально три строчки:

const I = x => x;
const K = x => y => x;
const S = f => g => x => f(x)(g(x));

console.log(S(K)(K)(42));  // 42

I = lambda x: x
K = lambda x: lambda y: x
S = lambda f: lambda g: lambda x: f(x)(g(x))

print(S(K)(K)(42))  # 42

I — лишний: SKK

Строчка S(K)(K)(42) === 42 из примера выше не случайна. Раскрутим S K K x по правилам, шаг за шагом:

Шаг 0.  S K K x
Шаг 1.  Правило S с x := K, y := K, z := x:
        →  K x (K x)
Шаг 2.  Правило K с x := x, y := (K x) — второй аргумент выбрасывается:
        →  x

Получили x для произвольного x, то есть S K K ведёт себя ровно как I. Значит, базис можно сократить до двух комбинаторов: S и K достаточно. I оставляют в системе исключительно ради читаемости — как x + 0 оставляют в коде, когда так понятнее.

Сокращать дальше тоже можно: существует однокомбинаторный базис. Например, ι = λf. f S K — из одной этой константы выражаются и S, и K (I = ι ι, K = ι (ι (ι ι)), S = ι (ι (ι (ι ι)))). На этом построен эзотерический язык Iota, а его старший брат Unlambda — полноценный язык программирования, где нет ничего, кроме комбинаторов. Практической пользы ноль, но как доказательство «одной детали хватает» — впечатляет.

Теорема: это тот же самый язык

Утверждение, ради которого всё затевалось: комбинаторная логика на базисе {S, K} и бестиповое лямбда-исчисление эквивалентны по выразительной силе. Любой лямбда-терм переводится в комбинаторный и обратно, вычисление сохраняется.

«Обратно» тривиально: S, K, I — это просто лямбда-термы λf.λg.λx. f x (g x), λx.λy. x, λx. x, а аппликация переводится в аппликацию.

Интересное направление — прямое: как выкинуть λ из произвольного терма. Это делает алгоритм устранения абстракции (bracket abstraction). Обозначение: λ*x. M — «комбинаторный терм, который ведёт себя как λx. M». Три правила:

(1) λ*x. x  =  I                               — тело и есть переменная
(2) λ*x. M  =  K M            если x ∉ FV(M)   — тело не зависит от x
(3) λ*x. (M N)  =  S (λ*x. M) (λ*x. N)         — иначе разнести по обеим половинам

Полный перевод лямбда-терма в комбинаторный: переменные и аппликации переносятся как есть, а каждая абстракция снимается изнутри наружу через λ*.

T[x]      = x
T[M N]    = T[M] T[N]
T[λx. M]  = λ*x. T[M]

Считаем руками

Возьмём λx. λy. x — комбинатор K, только записанный лямбдой. Снимаем связыватели изнутри наружу.

T[λx. λy. x]
= λ*x. (λ*y. x)                    внутренняя абстракция первой
= λ*x. (K x)                       правило (2): y ∉ FV(x)
= S (λ*x. K) (λ*x. x)              правило (3): тело — аппликация K к x
= S (K K) I                        правило (2) слева, правило (1) справа

Ответ: S (K K) I. Проверим, что он ведёт себя как K:

Шаг 0.  S (K K) I a b
Шаг 1.  Правило S (x := K K, y := I, z := a):
        →  K K a (I a) b
Шаг 2.  Правило K (внешний аргумент a выбрасывается):
        →  K (I a) b
Шаг 3.  Правило K ещё раз (b выбрасывается):
        →  I a
Шаг 4.  Правило I:
        →  a

Работает: S (K K) I a b →→ a, ровно как K a b → a. Но обратите внимание — вместо одного узла K мы получили четыре. Это первый звоночек про цену перевода; к нему вернёмся.

Попробуйте теперь снять два связывателя с числа Чёрча «два» (λf. λx. f (f x) из https://courses.digitable.life/post/lambda-calculus/05-numerals/) — внутренняя абстракция даст S (K f) (S (K f) I), а после снятия внешней терм разрастётся на десяток узлов. Дальше руками писать больно, и это честный вывод: устранение абстракции механическое, его надо не считать, а запускать.

Реализация: 40 строк на Python

Терм представим кортежами, как в https://courses.digitable.life/post/lambda-calculus/03-reductions/: ('var', имя), ('app', M, N), ('c', 'S'|'K'|'I'), а на входе допустим ещё ('lam', x, тело).

def V(x):       return ('var', x)
def A(m, n):    return ('app', m, n)
def C(name):    return ('c', name)
def L(x, body): return ('lam', x, body)

S, K, I = C('S'), C('K'), C('I')


def occurs(x, t):
    """Встречается ли переменная x в терме t."""
    if t[0] == 'var':
        return t[1] == x
    if t[0] == 'app':
        return occurs(x, t[1]) or occurs(x, t[2])
    return False


def abstract(x, t):
    """λ*x. t — устранение одного связывателя."""
    if t == V(x):                       # (1) λ*x. x = I
        return I
    if not occurs(x, t):                # (2) λ*x. M = K M
        return A(K, t)
    return A(A(S, abstract(x, t[1])),   # (3) λ*x. (M N) = S (λ*x.M) (λ*x.N)
             abstract(x, t[2]))


def to_cl(t):
    """Перевод произвольного лямбда-терма в комбинаторный."""
    if t[0] in ('var', 'c'):
        return t
    if t[0] == 'app':
        return A(to_cl(t[1]), to_cl(t[2]))
    if t[0] == 'lam':
        return abstract(t[1], to_cl(t[2]))   # тело переводим ПЕРВЫМ
    raise ValueError(t)

Порядок в последней строке важен: сначала переводим тело (внутренние абстракции исчезают), и только потом снимаем внешний связыватель. Иначе abstract наткнётся на ('lam', ...), которого не понимает.

Редуктор для комбинаторов заметно проще лямбда-редуктора: нет подстановки, нет свежих имён, нет проверки захвата. Достаточно разобрать терм на «голову и аргументы» — это называется остов (spine) — и посмотреть, хватает ли аргументов для срабатывания правила.

def spine(t):
    """Разбирает терм на голову и список аргументов слева направо."""
    args = []
    while t[0] == 'app':
        args.append(t[2])
        t = t[1]
    args.reverse()
    return t, args


def rebuild(head, args):
    for a in args:
        head = A(head, a)
    return head


def step(t):
    """Один шаг переписывания; None — нормальная форма."""
    head, args = spine(t)
    if head[0] == 'c':
        name = head[1]
        if name == 'I' and len(args) >= 1:
            return rebuild(args[0], args[1:])
        if name == 'K' and len(args) >= 2:
            return rebuild(args[0], args[2:])
        if name == 'S' and len(args) >= 3:
            x, y, z = args[0], args[1], args[2]
            return rebuild(A(A(x, z), A(y, z)), args[3:])
    for i, a in enumerate(args):        # голова не сработала — идём в аргументы
        red = step(a)
        if red is not None:
            new_args = list(args)
            new_args[i] = red
            return rebuild(head, new_args)
    return None


def normalize(t, limit=10_000):
    for _ in range(limit):
        nxt = step(t)
        if nxt is None:
            return t
        t = nxt
    raise RuntimeError('лимит шагов исчерпан — вероятно, терм расходится')


def show(t):
    """Печать в привычной левоассоциативной записи."""
    if t[0] in ('var', 'c'):
        return t[1]
    right = show(t[2])
    return show(t[1]) + ' ' + ('(' + right + ')' if t[2][0] == 'app' else right)

Запускаем на числе Чёрча «два»:

two = L('f', L('x', A(V('f'), A(V('f'), V('x')))))
two_cl = to_cl(two)
print(show(two_cl))
# S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))

print(show(normalize(A(A(two_cl, V('g')), V('a')))))
# g (g a)

Восемнадцать узлов вместо шести — но поведение то же: применить g дважды. Самый убедительный тест — подсунуть комбинаторам обычные питоновские функции и посмотреть на число:

def run(t, env):
    """Интерпретируем CL-терм напрямую питоновскими функциями."""
    if t[0] == 'var':
        return env[t[1]]
    if t[0] == 'c':
        return {'S': lambda x: lambda y: lambda z: x(z)(y(z)),
                'K': lambda x: lambda y: x,
                'I': lambda x: x}[t[1]]
    return run(t[1], env)(run(t[2], env))

print(run(A(A(two_cl, V('inc')), V('zero')), {'inc': lambda n: n + 1, 'zero': 0}))
# 2

Терм, в котором не осталось ни одной переменной и ни одной лямбды, посчитал 0 + 1 + 1. Никакой магии: S, K и аппликация — это и есть весь язык.

Сложность. abstract обходит терм целиком на каждом снимаемом связывателе: O(размер тела) на шаг. Хуже другое — размер результата. Правило (3) превращает один узел-аппликацию в узел S плюс две рекурсивные копии, так что за один снятый связыватель терм может вырасти примерно втрое, а d вложенных абстракций дают верхнюю оценку 3^d. На практике до экспоненты доходит редко, но и реальность невесёлая — измерим.

Цена наивного перевода — и как её сбивают

Возьмём семейство термов λx1. … λxn. x1 (x2 (… (xn x1))) (каждая переменная используется, вложенность растёт) и посчитаем размеры в узлах:

Наивный алгоритм даёт кубический рост, оптимизированный — квадратичный. Откуда берётся оптимизация: правило (3) применяется вслепую, даже когда x встречается только в одной половине аппликации. Дэвид Тёрнер в работе Another Algorithm for Bracket Abstraction (Journal of Symbolic Logic, 1979) предложил различать случаи, добавив два комбинатора:

B x y z  →  x (y z)      — композиция:  B = (.) в Haskell
C x y z  →  x z y        — перестановка: C = flip в Haskell

Оптимизированные правила:

λ*x. (M x)   =  M                     если x ∉ FV(M)      — это η-редукция
λ*x. (M N)   =  B M (λ*x. N)          если x ∉ FV(M)      — x только справа
λ*x. (M N)   =  C (λ*x. M) N          если x ∉ FV(N)      — x только слева
λ*x. (M N)   =  S (λ*x. M) (λ*x. N)   если x есть в обоих

Разница на конкретных термах — не косметическая:

Последняя строчка — красивая: число Чёрча «два» это S B I. Проверим: S B I f x → B f (I f) x → f (I f x) → f (f x). Ровно то, что нужно.

Дальнейшее развитие темы — директорные строки (Kennaway & Sleep, 1988), где вместо комбинаторов к каждому узлу приписывается маршрут аргумента; там рост уже O(n log n). Именно этот путь и привёл в промышленность: см. ниже.

Первый комбинатор, который вы точно знали: композиция

Комбинаторы B, C, K, W образуют ещё один классический базис (система Карри BCKW):

B x y z  →  x (y z)     — композиция
C x y z  →  x z y       — перестановка аргументов
K x y    →  x           — игнорирование
W x y    →  x y y       — дублирование

И вот тут комбинаторная логика внезапно перестаёт быть экзотикой, потому что каждый из этих четырёх — функция из стандартной библиотеки любого функционального языка:

-- B, C, K, W в Haskell — все четыре давно в Prelude или в base
b = (.)                 -- композиция:      (.) f g x = f (g x)
c = flip                -- перестановка:    flip f x y = f y x
k = const               -- игнорирование:   const x _ = x
w f x = f x x           -- дублирование (join для функций)

const B = f => g => x => f(g(x));   // compose / R.compose / pipe наоборот
const C = f => x => y => f(y)(x);   // flip / R.flip
const K = x => _ => x;              // constant / R.always / _.constant
const W = f => x => f(x)(x);        // «использовать аргумент дважды»

Стиль, в котором функции определяются композицией комбинаторов, без явного упоминания аргументов, называется point-free (бесточечный, он же tacit programming). Мы уже касались его в https://courses.digitable.life/post/lambda-calculus/03-reductions/ как следствия эта-редукции; теперь видно, что это ровно устранение абстракции, выполняемое руками:

-- было: с точками (аргументами)
sumOfSquares xs = sum (map (^2) xs)

-- стало: point-free — аргумент xs устранён через B (композицию)
sumOfSquares = sum . map (^2)

И самый эффектный пример — «среднее арифметическое одним проходом по определению»:

-- аргумент xs встречается ДВАЖДЫ, значит нужен S, а не B
average xs = sum xs / fromIntegral (length xs)

-- point-free: <*> для функций — это буквально комбинатор S
average = (/) <$> sum <*> (fromIntegral . length)

Это не аналогия и не игра слов: у аппликативного функтора функций (Reader) операции определены как pure = const = K и f <*> g = \x -> f x (g x) = S. Каждый раз, когда вы пишете (<*>) над функциями, вы пишете S Шейнфинкеля. Подробнее про аппликативы — https://courses.digitable.life/post/functional-programming/07-functors-and-applicatives/.

Практический совет, который стоит унести: point-free полезен ровно до порога читаемости. sum . map (^2) лучше версии с аргументом. ((.) . (.)) (композиция двух функций двух аргументов) — уже нет; в сообществе Haskell такие термы называют «pointless style», и линтер hlint намеренно не предлагает переписывать в них. Если хочется поиграть — есть pointfree.io, который переводит выражение в комбинаторную форму онлайн; посмотрите на результат для функции из трёх аргументов и всё поймёте сами.

Y без единой лямбды

Проверим силу базиса на самом сложном, что было в треке, — комбинаторе неподвижной точки (https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/). Переведём Y = λf. (λx. f (x x)) (λx. f (x x)) алгоритмом из кода выше:

Y = S (S (S (K S) (S (K K) I)) (K (S I I)))
      (S (S (K S) (S (K K) I)) (K (S I I)))

Двадцать пять узлов, ни одной переменной. Раскрутим Y F нашим редуктором (это первые шаги трассировки, полностью терм не нормализуется — он и не должен):

 0: S (S (S (K S) (S (K K) I)) (K (S I I))) (S (S (K S) (S (K K) I)) (K (S I I))) F
 1: S (S (K S) (S (K K) I)) (K (S I I)) F (S (S (K S) (S (K K) I)) (K (S I I)) F)
 …
 8: I F (K (S I I) F (S (S (K S) (S (K K) I)) (K (S I I)) F))
 9: F (K (S I I) F (S (S (K S) (S (K K) I)) (K (S I I)) F))
10: F (S I I (S (S (K S) (S (K K) I)) (K (S I I)) F))

На девятом шаге снаружи появилось F, а внутри — снова заготовка, которая при следующем требовании развернётся в F (…). Это то же самое поведение Y F →→ F (Y F), только собранное из констант. Кстати, S I I в трассировке — это самоприменение λx. x x: S I I x → I x (I x) → x x. Тот самый Ω-строитель, переехавший в комбинаторную запись.

Здесь же виден и предел системы: сильной нормализации не появилось, расходимость никуда не делась. Комбинаторная логика полна по Тьюрингу ровно в той же мере, что и лямбда-исчисление, — с той же ценой (https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/).

Зачем это делали на самом деле: графовая редукция

Комбинаторы могли остаться логической диковиной, если бы не одно инженерное соображение. Посмотрите на правило S x y z → x z (y z): аргумент z в правой части встречается дважды. Если переписывать термы буквально (как делает наш step), z копируется — и, если это дорогое невычисленное выражение, оно посчитается дважды. Это ровно та проблема дублирования работы, из-за которой в https://courses.digitable.life/post/lambda-calculus/08-evaluation-strategies/ нормальный порядок проигрывал по скорости.

Решение: не копировать, а разделять ссылку. Тогда терм — не дерево, а граф; редукция переписывает узлы на месте, и посчитанное один раз видно всем, кто на него ссылается.

Так устроена графовая редукция комбинаторов — техника, на которой Дэвид Тёрнер построил реализацию языков SASL и Miranda (A New Implementation Technique for Applicative Languages, Software: Practice and Experience, 1979). Компилятор переводил программу в комбинаторы, а рантайм крутил маленький цикл: раскрутить остов, найти голову, применить правило, переписать узел.

Дальше история пошла дальше и мимо: фиксированный набор комбинаторов оказался слишком мелкозернистым — на каждый шаг приходилось трогать память, а полезной работы делалось на копейку. Джон Хьюз предложил суперкомбинаторы: вместо S и K брать комбинаторы, порождённые самой программой (Super-combinators: A New Implementation Method for Applicative Languages, 1982). Приём, которым лямбды превращаются в такие комбинаторы, называется lambda lifting — вы наверняка встречали его в описаниях компиляторов: каждая внутренняя функция получает свободные переменные дополнительными параметрами и всплывает на верхний уровень. Отсюда прямая линия к машине STG в GHC и к тому, как компилируются замыкания вообще (https://courses.digitable.life/post/compilers/09-virtual-machines/, https://courses.digitable.life/post/compilers/07-optimization/).

Логическая сторона: S и K — это две аксиомы

В https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/ мы отмечали, что типы K и S — это аксиомы импликационного фрагмента интуиционистской логики:

K : A → (B → A)
S : (A → (B → C)) → ((A → B) → (A → C))

Теперь можно сказать сильнее и точнее. Гильбертовское исчисление высказываний — это система, где нет никаких правил вывода, кроме modus ponens, зато есть аксиомы. Естественная дедукция — система, где есть правило «введения импликации»: доказал B, предполагая A, — получи A → B. Так вот:

• лямбда-исчисление относится к комбинаторной логике ровно так же, как естественная дедукция к гильбертовскому исчислению;
• абстракция λx. M — это правило введения импликации (сделать предположение и разрядить его);
• аппликация — modus ponens;
• алгоритм устранения абстракции — это доказательство теоремы о дедукции, той самой, которая говорит: «если из A выводится B, то A → B доказуемо без предположений».

Кубический рост термов из таблицы выше — это, если смотреть с логической стороны, честная цена превращения «доказательства с предположением» в «доказательство без предположений». Формальная сторона теоремы о дедукции разобрана в https://courses.digitable.life/post/mathematics/02-logic-and-proofs/.

Где вы это встретите вне учебника

Parser combinators. Слово «комбинатор» в названии parsec, nom, fast-check, zod — не украшение. Библиотека даёт набор базовых значений и функций, которые их комбинируют, а язык программирования выступает метаязыком. Идея ровно та же: маленький базис плюс аппликация.

Тацитные языки. J и K (наследники APL) — промышленные языки, где point-free стиль не приём, а норма; «вилка» в J ((+/ % #) — среднее арифметическое) это буквально комбинатор S с явным синтаксисом. Автор K, Артур Уитни, писал на этом торговые системы, где важна каждая микросекунда.

Минификаторы и оптимизаторы. Часть проходов компилятора — это правила переписывания в чистом виде: «flip (flip f) → f», «map g . map h → map (g . h)». Никакой семантики, только алгебра комбинаторов (https://courses.digitable.life/post/compilers/07-optimization/).

Колмогоровская сложность и «самая короткая программа». Джон Тромп построил binary lambda calculus — бинарную кодировку лямбда-термов и комбинаторов, на которой считают минимальный размер универсального интерпретатора (206 бит). Это тот редкий случай, когда «сколько бит в языке» — не вопрос вкуса, а измеримая величина.

Интервью и код-ревью. Практический навык из этой статьи ровно один, зато полезный: увидев \x -> f (g x), вы автоматически думаете f . g; увидев \x -> f x (g x), вы знаете, что это S, и что тащить x через три строки не обязательно.

Типичные ошибки и заблуждения

«Комбинаторная логика — это лямбда-исчисление, только хуже». Она эквивалентна по силе, но это другая система: в ней нет связывателей, поэтому нет альфа-эквивалентности, нет захвата и нет подстановки. Реализуется она проще, а читается хуже. Обмен, а не деградация.

«Раз S и K хватает, компиляторы так и делают». Делали — Тёрнер, SASL, Miranda, SKIM. Отказались: гранулярность слишком мелкая. Современные реализации используют суперкомбинаторы, окружения и замыкания. Комбинаторы остались как идея, а не как рантайм.

«λ*x — это то же самое, что λx». Нет: λ*x. M — не конструкция языка, а функция уровня трансляции, которая по терму M строит другой терм. В результирующем языке никаких λ* не остаётся.

«Устранение абстракции сохраняет размер». Не сохраняет — растёт кубически при наивных правилах. Об этом легко забыть, глядя на аккуратные K и S в учебнике.

«Point-free всегда лучше». Point-free выигрывает, когда убирает шум (sum . map f), и проигрывает, когда прячет смысл. Название аргумента — это документация; выбрасывая его, вы платите читаемостью.

«В комбинаторной логике нет переменных вообще». Свободные переменные в термах остаются — их некому связать, поэтому они безопасны. Исчезли именно связанные переменные, а вместе с ними вся механика имён.

Упражнения

Все редукции раскручивайте полностью, по одному правилу за шаг.

1. Сведите K I a b к нормальной форме. Какой известный комбинатор получился из K I?
2. Что делает терм S I I? Примените его к a и к S I I.
3. Переведите λx. λy. y в комбинаторную форму наивным алгоритмом и упростите результат правилами Тёрнера.
4. Переведите λx. x x (самоприменение) и проверьте результат на аргументе a.
5. Выразите B через S и K. Подсказка: B = λx.λy.λz. x (y z), гоните алгоритм.
6. Почему λ*x. (M N) = S (λ*x. M) (λ*x. N) корректно, даже если x не входит ни в M, ни в N? Что при этом получится и чем это плохо?
7. Число Чёрча «три» в наивном переводе занимает 26 узлов, а «два» с комбинатором B — это всего S B I. Как выглядит «три» через B? Проверьте редукцией.

Ответы

1. K I a b → I b → b. Раскручиваем: K I a — правило K, второй аргумент a выбрасывается, остаётся I; затем I b → b. Итого K I ведёт себя как λx.λy. y, то есть это FALSE из https://courses.digitable.life/post/lambda-calculus/04-booleans/ (и второй проектор пары из https://courses.digitable.life/post/lambda-calculus/06-pairs-and-lists/). Забавно: K — это TRUE, K I — это FALSE, вся логика Чёрча живёт в базисе SK.

2. S I I x → I x (I x) → x (I x) → x x — это самоприменение. Значит S I I a → a a, а S I I (S I I) — это Ω: расходящийся терм, редуцирующийся сам в себя вечно.

3. Наивно: λ*x. (λ*y. y) = λ*x. I = K I (правило (2), x не входит в I). Правила Тёрнера тут ничего не улучшают — K I уже минимально. Обратите внимание, что для λx.λy. x наивный алгоритм дал громоздкое S (K K) I, а для λx.λy. y — сразу компактное K I: асимметрия из-за того, что во втором случае внешняя переменная не используется.

4. λ*x. (x x) = S (λ*x. x) (λ*x. x) = S I I. Проверка: S I I a → I a (I a) → a a. Совпадает с ответом 2.

5. Наивный алгоритм даёт для λx.λy.λz. x (y z) 25 узлов (см. таблицу выше) — именно поэтому B вводят отдельной константой, а не выражают через S и K каждый раз. Каноническая короткая форма: B = S (K S) K. Проверьте её редукцией: S (K S) K x y z → K S x (K x) y z → S (K x) y z → K x z (y z) → x (y z). Сходится.

6. Корректно, потому что правило (3) ничего не предполагает про вхождения: S (K M) (K N) z → K M z (K N z) → M N, то есть результат применим и даёт M N для любого z. Плохо это тем, что вместо короткого K (M N) получается вчетверо больший терм. Отсюда ещё одна классическая оптимизация Тёрнера: S (K M) (K N) = K (M N).

7. «Два» = S B I, а «три» получается добавлением ещё одной композиции: S B (S B I). Проверка: S B (S B I) f x → B f (S B I f) x → f (S B I f x) → f (f (f x)), поскольку S B I f x →→ f (f x) из разбора выше. Общий шаблон: число n — это S B применённое n-1 раз к I, что читается как «композиция функции с собой n раз» и в точности повторяет определение чисел Чёрча через итерацию.

Мини-итог

• Комбинаторная логика старше лямбда-исчисления и решает ту же задачу без единого связывателя: только константы, аппликация и правила переписывания.
• Базиса {S, K} достаточно: I = S K K, а любой лямбда-терм переводится механически алгоритмом устранения абстракции из трёх правил.
• Плата за отсутствие переменных — рост термов (кубический при наивных правилах, квадратичный с B и C, O(n log n) с директорными строками).
• Все базовые комбинаторы давно живут в стандартных библиотеках: B = (.), C = flip, K = const, S = <*> для функций. Point-free стиль — это устранение абстракции, выполняемое руками.
• Реальная инженерная мотивация — графовая редукция: правило S дублирует ссылку, а не значение, поэтому разделяемое вычисление считается один раз. Отсюда выросли SASL, Miranda, суперкомбинаторы, lambda lifting и, в конечном счёте, STG в GHC.
• Логически лямбда-исчисление относится к комбинаторной логике как естественная дедукция к гильбертовскому исчислению, а устранение абстракции — это теорема о дедукции.

Источники

• Moses Schönfinkel. Über die Bausteine der mathematischen Logik, 1924 — первая работа о комбинаторах, обзор и перевод.
• Haskell Curry, Robert Feys. Combinatory Logic, Vol. I, North-Holland, 1958 — каноника.
• David Turner. Another Algorithm for Bracket Abstraction, JSL, 1979 — jstor.org/stable/2273733.
• David Turner. A New Implementation Technique for Applicative Languages, SPE, 1979 — wiley.
• John Hughes. Super-combinators, ACM Symposium on LISP, 1982 — dl.acm.org/doi/10.1145/800068.802129.
• Simon Peyton Jones. The Implementation of Functional Programming Languages, 1987 — полный текст, главы про графовую редукцию и суперкомбинаторы.
• Raymond Smullyan. To Mock a Mockingbird, 1985 — комбинаторы в виде головоломок про птиц; лучший способ набить руку.
• Stanford Encyclopedia of Philosophy, Combinatory Logic — plato.stanford.edu/entries/logic-combinatory.
• John Tromp. Binary Lambda Calculus and Combinatory Logic — tromp.github.io/cl/cl.html.

Что дальше

Мы избавились от переменных — и обнаружили, что вычисление всё равно управляется тем, кто кого применяет и в каком порядке. Следующий шаг радикальнее: сделать сам порядок явной частью терма. Приём называется CPS, и из него выросли колбэки, промисы, генераторы, исключения и async/await — то есть примерно весь ваш рабочий день.

Продолжения и CPS: откуда взялись колбэки, генераторы и async/await