Систематическое конструирование однокомбинаторного базиса для λ-термов

Ерон Фоккер

1992

Аннотация: В этой статье описывается простое замкнутое λ-выражение, при помощи которого можно выразить все прочие λ-выражения. Его построение осуществляется систематическим образом. Полученное λ-выражение является более простым, чем известные из литературы однокомбинаторные базисы1.



Ключевые слова: Базис S, K, I, систематическое построение, простота в качестве цели.

1  Комбинаторные базисы

Комбинатором называется замкнутый λ-терм, то есть выражение, состоящее из λ-абстракций и применений (аппликаций), не содержащее свободных переменных. Например, вот как выглядят несколько обычно используемых комбинаторов:

В этой статье строчные буквы будут использоваться для обозначения переменных в языке λ-исчисления, а заглавные буквы будут использоваться для обозначения λ-термов. Зафиксированные (именованные) выражения обозначаются прямым шрифтом. Применение является левоассоциативной операцией, поэтому выражение ABC обозначает (AB)C. Абстракция распространяется на всё выражение после символа точки (.), поэтому выражение λ x.AB обозначает λ x.(AB). Множественные абстракции записываются сокращённо, поэтому выражение λ xy.A обозначает λ x.λ y.A.

Комбинаторы имеют важнейшее значение при реализации функциональных языков программирования [3]. Функциональные программы могут быть выражены через набор последовательных применений комбинаторов друг к другу, поэтому отсутствует необходимость в λ-абстракции. Набор комбинаторов, с помощью которых посредством применения (аппликации) могут быть построены все замкнутые λ-термы (с точностью до α-, β- и η-конверсии), называется базисом. Х. Карри [2] показал, что конечный базис существует:

Теорема 1   Набор комбинаторов S, K, I является базисом.

Proof. Любое заданное λ-выражение выражается через указанные комбинаторы при помощи последовательного применения следующих правил, убирающих абстракции:

1)λ x.x⇒I
2)λ x.A⇒KA, если x ∉ Free(A)
3)λ x.AB⇒S(λ x.A)(λ x.B)

Эти правила покрывают собой все возможные варианты, так как тело λ-абстракции является либо связанной переменной (правило 1), либо другой переменной (правило 2), либо применением (правило 3), либо другой абстракцией, которая сама должна быть убрана в первую очередь. Процесс перевода в указанный базис останавливается, как только он выдал набор применений меньших термов. Правило 1 являет собой определение комбинатора I, правило 2 корректно по определению комбинатора K:

KA={ Определение K }
(λ xy.x)A={ β-редукция }
λ y.A={ α-конверсия, x ∉ Free(A) }
λ x.A  

Правило 3 соответственно верно по определению комбинатора S:

S(λ x.A)(λ x.B)={ Определение S }
(λ fgx.fx(gx))(λ x.A)(λ x.B)={ β-редукция (дважды) }
λ x.(λ x.A)x((λ x.B)x)={ η-конверсия (дважды) }
λ x.AB  


М. Шейнфинкель [4]2 заметил, что комбинатор I может быть выражен через комбинаторы S и K:

Теорема 2   Набор комбинаторов S, K является базисом.

Proof. По теореме 1 набор комбинаторов S, K, I является базисом. Все появления комбинатора I необходимо заменить на выражение SKA, где A — произвольный терм, к примеру — K. Доказательство выглядит следующим образом:

SKA={ Определение S }
(λ fgx.fx(gx))KA={ β-редукция (дважды) }
λ x.Kx(Ax)={ Определение K }
λ x.(λ xy.x)x(Ax)={ β-редукция (дважды) }
λ x.x  


Центральной точкой рассмотрения этой статьи является поиск некоторого комбинатора X, составляющего базис.

2  Однокомбинаторный базис

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

Целью процесса является создание комбинатора X, при помощи которого можно получить комбинаторы S и K посредством операции применения. Затем по теореме 2 может быть построен любой замкнутый λ-терм. Ни один из комбинаторов S или K не являет собой однокомбинаторный базис, поэтому оба этих комбинатора должны быть построены из нескольких экземпляров комбинатора X.

Первым интуитивным шагом в построении однокомбинаторного базиса является предположение о том, что комбинаторы S и K являются применением, с левой стороны которого находится комбинатор X. Далее необходимо найти правые стороны этих применений:

Естественно, что термы A и B должны быть различными. Вторым интуитивным шагом будет предположение о том, что эти термы являются простейшими различными выражениями, которые можно получить из комбинатора X, а выражение для комбинатора K должно быть проще, чем такое для комбинатора S, то есть терм A должен быть проще терма B:

Теперь выражение комбинаторов S и K выглядит следующим образом:

(М. Шейнфинкель уже давал такую спецификацию в своей работе [4], однако с изменёнными местами для термов A и B. Но он не предоставил закрытую форму для комбинатора X). Используя первое представленное выражение во втором, можно получить:

Так как комбинатор X применяется к функциям (X и K), то его форма должна быть такой: λ f.M. Теперь необходимо сконструировать тело выражения M вне определения f. Не очень ясно, где внутри выражения M должна использоваться переменная f. Но эта переменная являет собой функцию, поэтому ясно, что она должна к чему-то применяться. Так как функция f может быть выражена через K, а у этого комбинатора два аргумента, то можно попробовать также применить функцию f к двум аргументам. Поэтому:

X = λ f.fPQ

Необходимо в этом уравнении найти выражения P и Q. Можно провести следующие вычисления:

S={ Спецификация }
XK={ Определение X }
KPQ={ Определение K }
P  

Таким образом видно, что P = S. Далее:

K={ Спецификация }
XX={ Определение X }
XPQ={ Определение X }
PPQQ={ P = S }
SSQQ={ Определение S }
SQ(QQ)  

Для редукции комбинатора S на этом шаге требуется три аргумента. Можно использовать принцип экстенсиональности и предположить для любых A и B:

A={ Определение K }
KAB={ Вышеприведённое выражение }
SQ(QQ)AB={ Определение S }
QA(QQA)B  

Последнее выражение полностью удовлетворяется формой Q = λ xyz.x. Этот вывод можно зафиксировать в следующей теореме:

Теорема 3   Пусть X = λ f.fS(λ xyz.x), тогда этот комбинатор составляет однокомбинаторный базис.

Proof. По теореме 2 набор S, K является базисом. Все появления комбинатора K необходимо заменить на выражение XX, а появление комбинатора S на выражения X(XX). Правильность таких замен показана выше.


3  Сравнение с другими базисами

Таблица 1: Однокомбинаторные базисы
MeredithX=λ abcd.cd(a(λ x.d))
 U=X3X2
 V=X4(KX4)
 K⇒X4(X4UX2)X2
 S⇒V(U(X4(X4V2)(KX4)))
BöhmX=λ f.f(fS(K3I))K
 K⇒XX
 S⇒X(XX)
BarendregtX=λ f.f(fS(KK))K
 K⇒XXX
 S⇒X(XXX)
RosserX=λ f.fKSK
 K⇒XXX
 S⇒X(XX)
FokkerX=λ f.fS(λ xyz.x)
 K⇒XX
 S⇒X(XX)

В [1] даны некоторые иные однокомбинаторные базисы. Первый был найден независимо Мередитом в 1963 году и Барендрегтом в 1971 году. Другие формы были найдены Бёмом и Россером. В таблице 1 приведены выражения из [1]. Проявления в определениях X комбинаторов S, K, I должно заменять на λ-термы, показанные в разделе 1.

Таблица 2: Простота базисов из таблицы 1
 размерKS
 XKSшагов∑ размеровшагов∑ размеров
Meredith741523804136226817681
Böhm234771292509637792
Barendregt185675241803535923
Rosser144444826211316
Fokker122538916712352

Для того чтобы оценить простоту различных представленных решений, можно определить понятие размера как суммарное количество абстракций и аппликаций в заданном выражении. Тогда простота решения будет выражаться как размер представления комбинаторов X, K и S. В таблице 2 показаны эти размеры. Другим критерием простоты может быть количество шагов редукции по нормальной редукционной стратегии, которые требуются для достижения нормальной формы, а также сумма размеров промежуточных выражений в ходе проведения редукции. Эти величины также показаны в таблице 2. Решение, которое на систематической основе получено в этой статье, имеет минимальный размер и сравнимо с решением Россера по скорости нормализации.

4  Иной способ решения

Решение Россера может быть вычислено примерно также, как это сделано в данной статье в разделе 2. Спецификация комбинаторов S и K в решении Россера такова (необходимо обратить внимание на дополнительный комбинатор X в первой строке):

Достаточным условием для выражения XXX является выражение XX = KK (и, поэтому, выражение XXX = K). Как и в основном решении можно подставить это достаточное условие в определение комбинатора S:

Теперь необходимо отметить, что KKABC = B, поэтому выражение KK требует три аргумента. Таким образом, в этом конструировании можно предположить, что комбинатор X имеет форму:

X = λ f.fPQR

Как и ранее теперь можно вычислить выражение S = X(KK) = KKPQR = Q, а также выражение KK = XX = XPQR = PPQRQR = PPSRSR, так что:

Здесь представлено одно уравнение с двумя неизвестными (P и R). У него много решений, некоторые из которых можно найти с лёгкостью. Например:

И только последнее решение не так очевидно, как все остальные. Оно показывается при помощи выражения KKSKSK = KKSK = KK. Из этого решения следует выражение Россера для комбинатора X: λ f.fKSK. Именно степень свободы в выборе термов P и Q для этого решения мотивировала автора статьи начать поиск более простого решения.

Список литературы

[1]
Barendregt H. P. The Lambda Calculus: Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984.
[2]
Curry H. B., Feys R. Combinatory Logic, volume I. North-Holland Publishing Company, Amsterdam, third printing edition, 1974.
[3]
Peyton Jones S. L. The Implementation of Functional Programming Languages. Series in Computer Science. Prentice-Hall International, 1987.
[4]
Schönfinkel M. Über die bausteine der mathematischen logik. Mathematische Annalen, 92:305, 1924.
1
Запросы и прочую корреспонденцию отправлять Ерону Фоккеру (jeroen@cs.uu.nl), Кафедра компьютерной науки, Университет Утрехта, Нидерланды, P. O. Box 80.089, 3508 TB Utrecht, The Netherlands.
2
В оригинальной статье нет ссылки на фундаментальную работу М. Шейнфинкеля — прим. перев.
Этот документ был получен из LATEX при помощи HEVEA