Умолчания

Аксиомы комбинаторной логики

После определения алфавита и порядка построения допустимых комбинаторных выражений посредством операции аппликации, перечислим аксиомы комбинаторной логики.

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

Следующие аксиомы задают свойства отношения конвертируемости:

Аксиома (I)	Ix = x	существования комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя
Аксиома (K)	Kxy = x	существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка*
Аксиома (S)	Sxyz = xz(yz)	попарного связывания третьего элемента с первыми двумя

* Аксиома (K) близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.

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

(μ)	если a=b, то ca=cb
(ν)	если a=b, то ac=bc
(ρ)	a=a	рефлексивность - конвертируемость произвольного комбинаторного выражения к самому себе
(σ)	если a=b, то b=a	симметричность - двунаправленность вывода комбинаторных выражений посредством конверсии
(τ)	если a=b и b=c, то a=c	транзитивность - возможность опускать промежуточные этапы конверсии для цепочек вывода

Как видно, отношение конвертируемости обладает, в частности, свойствами рефлексивности, симметричности и транзитивности.

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

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

1. Скобки для операции аппликации восстанавливаются по ассоциации влево, например:

XY = (XY), XYZ = ((XY)Z),...

2. Избыточные скобки могут опускаться, например:

(XY) = XY, ((XY)Z) = XYZ,...

6.2.4. Синтаксис выражений комбинаторной логики

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

Задать синтаксис языка возможно, перечислив описание его конструкций с использованием метаязыка, например, с помощью форм Бэкуса-Наура или БНФ. БНФ созданы в 60-х годах Дж. Бэкусом (John Backus) и развиты П. Науром (Peter Naur) как метаязык для формализации синтаксиса языка программирования ALGOL 60. Впоследствии БНФ получили широкое распространение и в настоящее время являются основной нотацией для формализации синтаксиса языков программирования (мы будем пользоваться БНФ для формализации синтаксиса языка программирования SML).

В нотации БНФ символ "::=" интерпретируется словами "может иметь вид", а символ "|" - словом "или". Определяемое понятие записывается слева от значка "::=", а определяющие понятия записываются в угловых скобках справа от значка "::=".

Формализуем синтаксис выражений комбинаторной логики (или комбинаторов).

БНФ -описание комбинатора имеет вид:

<комбинатор>::= K | S | (<комбинатор> <комбинатор>)

БНФ -описание терма комбинаторной логики, возможно, содержащего переменные, имеет вид:

<комбинаторный терм>::= K | S | <переменная> |

(<комбинаторный терм> <комбинаторный терм>)

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

(I)	I a = a	комбинатор тождества
(K)	К ab = a	комбинатор первой проекции (иначе именуемый канцелятором, т.е. "отменяющим" "выполнение" всех "инструкций", кроме первой)
(S)	S abc = ac(bc)	комбинатор - коннектор - определяет порядок "связывания" "инструкций" программы таким образом, что третья "инструкция" "распределяется" по паре из двух первых
(B)	B abc = a(bc)	комбинатор композиции - образует последовательность комбинаторных термов и служит для объединения более элементарных "инструкций" в более сложные, а в итоге - в "программы"
(C)	C abc = acb	пермутация (перестановка)
(W)	W xy = xyy	дублирование аргументов

6.2.5. Редукция комбинаторных термов

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

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

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

Пример моделирования механизма редукции следующим

Рассмотрим комбинаторный терм вида

SKKx.

Пользуясь аксиомами (К) и (S), а также правилами вывода, произведем редукцию терма:

SKKx = (по правилу S) Kx(Kx) = (по правилу K) x.

В результате получаем, что SKKx = x, откуда, с учетом аксиом и правила (I), I = SKK.

Как видно из предыдущего примера, одни комбинаторы можно выразить через другие.

Дата добавления: 2014-01-07