Текст:Роман Душкин:Комбинаторы? Это просто!

Исходный вариант статьи (Р. В. Душкин, «Комбинаторы? - Это просто!») опубликован в журнале «Потенциал», №7, 2006.

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

Введение

Комбинаторная логика (от слова «комбинатор», а не «комбинаторика»)— это направление в математической логике, разработанное в первой половине XX века логиками Мозесом Шёнфинкелем и Хаскеллом Карри в качестве науки о вычислительных процессах. Хотя первоначально этот вид логики претендовал только на то, чтобы удалить из логических высказываний переменные, через некоторое время в информатике были получены прикладные результаты, показавшие, что комбинаторную логику можно использовать для проведения вычислений.

На комбинаторную логику можно смотреть как на некоторое упрощение $\lambda$-исчисления , в котором нет символа $\lambda$, а все функциональные абстракции представлены ограниченным набором символов, называемых «комбинаторами». Такие комбинаторы не содержат переменных, являются функциями высшего порядка, т.е. в качестве аргументов могут принимать на вход другие функции, а также описывают определённые правила преобразования объектов, поданных им на вход в качестве аргументов.

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

Формальная теория

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

1. Алфавит.
2. Утверждения (множество правильно построенных формул).
3. Аксиомы.
4. Правила вывода.

Под алфавитом понимается набор символов, допустимых в нотации записей термов в комбинаторной логике. В общем виде при помощи нотации комбинаторной логики можно записывать объекты нескольких типов — константы, переменные, термы и специальные знаки.

Константы обозначаются малыми буквами латинского алфавита, возможно с индексами. Обычно для обозначения констант берутся символы с начала алфавита. Переменные обозначаются также малыми буквами, возможно, с индексами, но при этом они обычно выбираются с конца алфавита: $c_{1}$, $c_{2}$ — константы, $x$, $y$ — переменные.

Однако для выделения константных объектов иногда будет использоваться иной способ записи. Такой способ заключается в выделении наименований констант полужирным начертанием — эта запись будет использоваться, если наименование константы состоит более чем из одного символа: if, true, pair и др.

Комбинаторные термы (или просто «выражения») будут обозначаться заглавными буквами латинского алфавита, возможно также с индексами: $M$, $N$ и т. д.

Из специальных символов в комбинаторной логике используется всего три: это скобки «(» и «)», а также знак равенства ($=$). Последний обозначает отношение конвертируемости — возможность преобразования одного терма в другой. С точки зрения вычислительных процессов, отношение конвертируемости определяет сам процесс вычисления значения функции, представленной комбинаторным термом.

Множество правильно построенных формул в комбинаторной логике выглядит очень просто. Его составляют выражения вида {$M = N$}, где $M$ и $N$ — комбинаторные термы. При этом сами комбинаторные термы строятся по индукции:

1) {если $c$ — константа, то $c$ — комбинаторный терм;}

2) {если $x$ — переменная, то $x$ — комбинаторный терм;}

3) {если $M$ и $N$ — комбинаторные термы, то $(MN)$ — комбинаторный терм;}

4) {других комбинаторных термов нет.}

В этом индуктивном определении выражение $(MN)$ обозначает операцию аппликации, единственную операцию комбинаторной логики. Аппликация описывает применение функции (в данном примере — терм $M$) к её аргументу или аргументам (в данном примере — терм $N$).

Как видно, создание комбинаторных термов повлечёт за собой лавинообразное внедрение в запись таких термов скобок. Для того, чтобы уменьшить количество скобок в записях комбинаторных термов, вводятся соглашения о скобках, которые заключаются в том, что пропущенные скобки восстанавливаются по ассоциативности влево:

$\begin{matrix}XY = (XY) \\XYZ = ((XY)Z)\end{matrix}$

В качестве аксиом, входящих в множество правильно построенных формул, обычно выделяются следующие:

Ix = x	(I)
Kxy = x	(K)
Sxyz = xz(yz)	(S)

Данные аксиомы не надо доказывать, их наличие просто постулируется. Эти аксиомы определяют три базовых комбинатора, использующихся для вывода (вычислений) новых комбинаторов. Традиционно базис S,K,I является тем набором первоначальных комбинаторов, через который выражаются все прочие комбинаторы. Однако это не минимальный базис, ибо наличие комбинатора I не обязательно в нём, т. к. его можно выразить через комбинаторы S и K:

Другими словами, комбинаторный базис — это набор комбинаторов, через которые при помощи отношения конвертируемости ($=$) можно выразить все остальные комбинаторы. Минимальным комбинаторным базисом является набор из комбинаторов S и K, но обычно его дополняют комбинатором I для упрощения записи выражаемых комбинаторных термов. Однако разнообразных базисов может быть бесчисленное множество, и разные исследователи вводили разные базисы для своих целей. В следующем разделе будут рассмотрены некоторые примеры таких базисов.

Остаётся рассмотреть правила вывода, которые используются в рамках комбинаторной логики для преобразования одних термов в другие и описывают отношение конвертируемости ($=$). Данные правила вывода по своей сути описывают это отношение, задавая его характеристики.

a = a	{$\rho$}
(a = b) $\Rightarrow$ (b = a)	{$\sigma$}
(a = b) $\wedge$ (b = c) $\Rightarrow$ (a = c)	{$\tau$}
(a = b) $\Rightarrow$ (ca = cb)	{$\mu$}
(a = b) $\Rightarrow$ (ac = bc)	{$\nu$}

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

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

Примеры сложных комбинаторов

Вполне естественно, что создатели комбинаторной логики не ограничились использованием двух базовых комбинаторов — S и K. Хотя они и составляют минимальный базис, но запись функций только через них увеличивает громоздкость определений с ростом сложности функций. Поэтому для упрощения записи определений более сложных комбинаторов и комбинаторных термов были разработаны дополнительные комбинаторы, из которых также можно составлять базисы.

К таким комбинаторам относятся следующие:

1. $\mathbf{B}xyz = x(yz).$
2. $\mathbf{C}xyz = xzy.$
3. $\mathbf{W}xy = xyy$

Данные комбинаторы весьма существенно сокращают некоторые преобразования Ради этого многие комбинаторы даже получили свои собственные наименования. Так комбинатор I называется «комбинатором тождества», комбинатор K — «канцелятор», комбинатор S — «коннектор», комбинатор B — «композитор», комбинатор C — «пермутатор» и комбинатор W — «дубликатор».

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

$\mathbf{B} \equiv \mathbf{S}(\mathbf{K}\mathbf{S})\mathbf{K}$

$\mathbf{C} \equiv \mathbf{S}((\mathbf{S}(\mathbf{K}\mathbf{S})\mathbf{K})(\mathbf{S}(\mathbf{K}\mathbf{S})\mathbf{K})\mathbf{S})(\mathbf{K}\mathbf{K})$

$\mathbf{W} \equiv \mathbf{S}\mathbf{S}(\mathbf{K}(\mathbf{S}\mathbf{K}\mathbf{K}))$

Вдумчивому читателю предлагается самостоятельно проверить данные формулы. Для этого достаточно воспользоваться аксиомами для комбинаторов S и K и подставить в формулы переменные в заданном количестве (согласно определениям).

Однако возникает вопрос. На основании чего получены перечисленные выражения комбинаторов B, C и W через базисные? Как создать такие выражения самостоятельно? Можно попытаться ответить на этот вопрос, самостоятельно найдя выражение комбинатора I, как самого простого. Это можно проделать на основании следующих рассуждений.

Выражение комбинатора I может начинаться либо с комбинатора S, либо с комбинатора K. При помощи цифр в следующих записях будут обозначаться недостающие объекты, которые ещё необходимо найти. В этом случае два возможных пути поиска выражения для комбинатора I выглядят так:

Здесь видно, что первая альтернатива не подходит автоматически, т. к. канцелятор K отменяет переменную $x$, которая должна появиться в самом конце. Соответственно далее надо рассматривать только вторую альтернативу и искать способ выражения неизвестных объектов $1$ и $2$. Они также могут быть либо комбинатором S, либо комбинатором K. Соответственно, подставляя эти комбинаторы вместо неизвестного объекта $1$, можно получить:

Как видно, первая альтернатива уже дала необходимый результат, а во второй альтернативе не хватает операндов у комбинатора S. Поэтому вторую альтернативу можно не рассматривать, а вернуться только к первой. В ней остаётся неизвестный объект $2$, который не участвует в цепочке вывода, т. к. уничтожается канцелятором. Поэтому вместо него может стоять любой комбинатор, например, всё тот же K. Так и получается, что выражение комбинатора тождества таково:

$\mathbf{I} \equiv \mathbf{S} \mathbf{K} \mathbf{K}$

Этот пример также показал, что способов разложения объектов в комбинаторном базисе существует бесконечное множество, поэтому всегда имеет смысл говорить о «минимальном» разложении, т. е. таком, в записи которого используется минимальное число комбинаторов и скобок.

Но описанный процесс не так прост, как может показаться на самом деле. Достаточно попробовать разложить подобным образом относительно простой комбинатор B, чтобы понять, что в процессе такого рассмотрения альтернатив дерево решений растёт подобно снежному кому. Поэтому ради облегчения процесса выражения объектов с заданными комбинаторными характеристиками были созданы специальные правила. Данные правила относятся к выражению в базисе S,K,I

1. $\mathbf{T}[v] \Rightarrow v$, где $v$ — переменная.
2. $\mathbf{T}[(E_{1}E_{2})] \Rightarrow (\mathbf{T}[E_{1}]\mathbf{T}[E_{2}])$.
3. $\mathbf{T}[\lambda x.x] \Rightarrow \mathbf{I}$.
4. $\mathbf{T}[\lambda x.y] \Rightarrow \mathbf{K}y$, если $y \ne x$.
5. $\mathbf{T}[\lambda x.\lambda y.E] \Rightarrow \mathbf{T}[\lambda x.\mathbf{T}[\lambda y.E]]$.
6. $\mathbf{T}[\lambda x.(E_{1}E_{2})] \Rightarrow \mathbf{S} \mathbf{T}[\lambda x.E_{1}] \mathbf{T}[\lambda x.E_{2}]$

В этих правилах используется $\lambda$-нотация, которая принята в $\lambda$-исчислении. Привести комбинатор с его сигнатурой и характеристикой к $\lambda$-нотации довольно просто — надо вместо символа, обозначающего сам комбинатор, использовать символ ($\lambda$), а вместо символа ($=$) использовать точку ($.$).

В следующем разделе приведены определения типов данных и функций на языке Haskell, которые осуществляют перевод заданного комбинатора в базис S,K,I. Однако для закрепления материала читателю предлагается самостоятельно выразить в базисе S,K,I следующие комбинаторы с такими характеристиками:

1. $\mathbf{\Psi}abcd = a(bc)(bd)$
2. $\mathbf{C^{[2]}}abcd = acdb$
3. $\mathbf{C_{[2]}}abcd = adbc$
4. $\mathbf{B^{2}}abcd = a(bcd)$
5. $\mathbf{C^{[3]}}abcde = acdeb$
6. $\mathbf{C_{[3]}}abcde = aebcd$
7. $\mathbf{B^{3}}abcde = a(bcde)$
8. $\mathbf{\Phi}abcd = a(bd)(cd)$

Модуль на языке Haskell для преобразования комбинаторов

В этом разделе приводится текст программы на языке Haskell, которая преобразует заданный комбинатор в базис S,K,I. Для того, чтобы понимать приведённые определения, необходимо быть знакомым с синтаксисом этого языка на уровне, достаточном для определения типов и функций. Рассмотрение этих тем выходит за рамки этой статьи, поэтому заинтересованного читателя можно отослать к специализированной литературе.

Для преобразования комбинаторов необходимо для начала определить тип данных для их представления. В соответствии с определением комбинаторного терма определение такого типа выглядит так:

data Combinator = Var String
                | App Combinator Combinator
                | Lam String Combinator
 deriving Eq

Это определение полностью соответствует математическому, которое гласит, что комбинаторный терм — это либо переменная (Var — от английского слова «variable»), либо абстракция (Lam} — от английского слова «lambda»), либо приложение одного комбинаторного терма к другому (App — от английского слова «application»).

Для того, чтобы иметь возможность просматривать полученные результаты преобразования комбинаторных термов, необходимо определить тип Combinator экземпляром класса Show, который является классом величин, которые могут быть отображены. Конечно, интерпретатор языка Haskell может самостоятельно определить такой экземпляр, но он сделает это не так красиво, как можно сделать вручную. Поэтому вводится следующее определение:

instance Show Combinator where
   show (Var x)   = x
   show (App x y) =
       case y of
            App _ _ -> showLam x ++ "(" ++ show y ++ ")"
            _       -> showLam x ++ showLam y
       where showLam l@(Lam _ _) = "(" ++  show l  ++ ")"
             showLam x           = show x
   show (Lam x e)  = "\\" ++ x ++ "." ++ show e

Здесь видно, что переменная отображается просто своим именем, которое представляется строкой символов. Применение комбинаторных термов друг к другу просто записывается перечислением комбинаторных термов друг за другом со взятием в скобки, если второй терм сложный. А абстракция записывается при помощи символа ($\backslash$) с указанием сигнатуры и характеристики.

Базис S,K,I определяется при помощи константных функций, возвращающих комбинаторные термы в виде переменных с известными именами: i = Var "I"!, k = Var "K"!, s = Var "S"!.

Дополнительно, хотя это и не обязательно, можно реализовать предикат, который проверяет, является ли заданная переменная свободной в исследуемом комбинаторном терме. Этот предикат определяется так:

free :: String -> Combinator -> Bool
free x (Var y)     = x == y
free x (App e1 e2) = free x e1 || free x e2
free x (Lam y e) | x /= y = free x e
                 | x == y = False

Всё в полном соответствии с математическим определением.

Наконец, сама функция transform, которая осуществляет перевод комбинаторного терма в базис S,K,I. Её определение также выглядит в полном соответствии с перечисленными в предыдущем разделе правилами трансформации. Здесь можно видеть всю силу выразительности языка Haskell, которая позволяет записывать определения функций практически в математической нотации.

transform :: Combinator -> Combinator
transform (Var x) = Var x
transform (App x y) = App (transform x)
                          (transform y)
transform (Lam x (Var y))
 | x == y           = i
 | otherwise        = App k (Var y)
transform (Lam x (l@(Lam _ _))) = transform (Lam x (transform l))
transform (Lam x (App e1 e2)) = App (App s (transform (Lam x e1)))
                                    (transform (Lam x e2))

Видно, что определение этой функции полностью совпадает с описанием правил трансформации комбинаторных термов. Однако данная функция не позволяет получить минимальное выражение комбинаторного терма в базисе S,K,I. Она возвращает один из возможных вариантов разложения терма. Например, комбинатор B, закодированный при помощи $\lambda$-нотации следующим образом:

b = Lam "x"
       (Lam "y"
            (Lam "z"
                 (App (Var "x")
                      (App (Var "y")
                           (Var "z")))))

Если передать это определение функции transform, то на выходе будет такая конструкция: S(S(KS)(S(KK)(S(KS)(S(KK)I))))(K(S(S(KS)(S(KK)I))(KI)))!

Представление данных и функций

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

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

Булевские значения

Для кодирования булевских величин необходимо иметь способ представления в комбинаторной логике значений true, false, а также служебную структуру if. Обычно для этих целей используются следующие правила кодирования:

1. true $\equiv$ K.
2. false $\equiv$ KI.
3. if $\equiv$ I.

Действительно, предложенный способ кодирования можно легко проверить:

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

Вполне естественно, что над представленными значениями истинности должны иметься функции для выполнения базовых операций булевской логики. Такие базовые операции могут быть выражены через условные выражения. Способы кодирования трёх базисных булевских операций (отрицание, конъюнкция и дизъюнкция) выглядят следующим образом:

1. not $\equiv$ C(C if false) true.
2. and $\equiv$ B (CC false) if.
3. or $\equiv$ C if true.

Читателю предлагается самостоятельно проверить данные тождества на предмет их верности. Для этого необходимо рассмотреть таблицы истинности для перечисленных логических операций и сравнить их с традиционными таблицами истинности.

Нумералы Чёрча

Вполне понятно, что для кодирования чисел или подобных им объектов можно использовать любой способ выражения, главное, что потом на таком способе можно было бы построить приемлемые операции, тождественные тем, что определены для чисел. Поэтому, собственно, способов кодирования чисел существует множество. Но самым первым способом был тот, что предложен А. Чёрчем, и теперь носит наименование «нумералы Чёрча».

Нумералом Чёрча порядка $n$ называется такой объект $\overline{n}$ ($n$ — натуральное число из расширенного множества натуральных чисел $\mathbb{N}^{+}$), который выражается через базовые комбинаторы следующим образом:

где под записью $\mathbf{(SB)^{n}}$ понимается $n$-кратное приложение объекта $\mathbf{(SB)}$ к самому себе:

$(SB)^{0}(KI) =KI,$

$(SB)^{1}(KI) =SB(KI),$

$(SB)^{2}(KI) =SB(SB)(KI),$

$(SB)^{3}(KI) =SB(SB(SB))(KI)$

и т. д. Т. е. по индукции эти объекты можно определить как:

1. $\overline{0} = (SB)^{0}(KI) = KI$.
2. $\overline{n} = (SB)^{n}(KI) = SB(SB^{n - 1})(KI)$, $n > 0$.

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

$\overline{0} f x = x$

$\overline{1} f x = f x$

$\overline{n} f x = \underbrace{f(f(\ldots(f}_{n} x)\ldots))$

Для этих объектов довольно простым способом можно определить функции для сложения, умножения и возведения в степень. Это делается следующим образом:

1. add $\equiv$ CI(SB).
2. mlt $\equiv$ B.
3. exp $\equiv$ CI.

Доказательство данных тождеств легко проводится по индукции и предлагается для самостоятельной проработки.

Упорядоченные пары

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

Для кодирования пары при помощи комбинаторных термов необходимо создать функцию, которая является конструктором такой пары. Это можно сделать следующим образом:

pair \(\equiv\) BC(CI)

Данный комбинатор составляет пару из двух заданных объектов любой природы. Для того, чтобы достать эти объекты из пары, необходимы т. н. «селекторы», т. е. функции для доступа к элементам пары. Эти селекторы можно определить так:

head \(\equiv\) CI true
tail \(\equiv\) CI false
 

Эти комбинаторы «вынимают» первое или второе значение из переданной им на вход пары. Например, можно доказать, что выражение:

head (pair \(x\) \(y\)) = \(x\)

для любого выражения $x$. Тоже самое можно сказать и о селекторе tail. Читателю опять же рекомендуется провести исследование этого выражения — это позволит закрепить изученный материал и более тонко понять смысл и назначение комбинаторной логики.

Общие замечания

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

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

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

Заключение

Рассмотренное в этой статье введение в основы комбинаторной логики не претендует на целостность изложения, да и невозможно в малой научно-популярной статье изложить сложную науку о вычислениях, на которой основана реализация многих функциональных языков программирования. Поэтому всех заинтересовавшихся читателей можно отослать к изучению комбинаторной логики и $\lambda$-исчисления по учебникам, полноценно описывающим эти интереснейшие направления логики. В качестве направлений для дальнейшего изучения можно посоветовать рассмотреть следующие вопросы:

1. Синтез нового объекта с заданными комбинаторными характеристиками.
2. Использование редукции комбинаторов при помощи графов, что позволяет проводить ленивые вычисления, в том числе и потенциально бесконечных структур данных.
3. Преобразование $n$-местных операторных функций в каррированные,позволяющие производить частичные вычисления.
4. Типизация комбинаторов, которая позволяет разбить всё множество комбинаторов на некие классы эквивалентности по их типам (сортам).
5. Оболочка Каруби — специальная категория в рамках комбинаторной логики, при помощи которой кодируются все объекты операторных вычислений, включая их типы.
6. Выражение при помощи комбинаторов различных систем программирования,в том числе выражение языков Lisp, Haskell и прочих.
7. Изучение суперкомбинаторов — объектов для ленивого вычисления значений некоторых выражений.
8. Оптимизация вычислений путём комбинирования параметров — шаг к построению систем суперкомпиляции.
9. Техники проведения синтаксического анализа на функциональных языках программирования.

Автор оригинального текста статьи благодарит Антонюка Д. А., который помог написать функции на языке Haskell для трансформации комбинаторных термов в базис S,K,I