Комбинаторная логика как формальная система
Рассмотрим построение формальной системы логики. Заметим, что важнейшим понятием для любой формы комбинаторной логики является понятие комбинатора.
Для того, чтобы формально определить комбинатор, необходимо ввести понятие свободной и связанной переменной в ламбда-выражении.
Переменная x называется свободной в ламбда-выражении (терме) вида ?x.A, если она не имеет вхождений в терм A; в противном случае переменная x называется связанной.
Для составных ламбда-выражений понятие связанной и свободной переменной определяется индукцией по построению с учетом возможных способов комбинирования, а именно, операций аппликации и абстракции.
Теперь становится возможным дать лаконичное определение комбинатора.
Ламбда-выражение (терм), не содержащее связанных переменных, называется комбинатором.
Перейдем к описанию комбинаторной логики как формальной системы. Согласно математической практике, необходимо определить следующие элементы теории:
- алфавит;
- утверждения;
- аксиомы;
- правила вывода.
Напомним, что под алфавитом понимается множество символов, допустимых в нотации той или иной формализации.
Утверждения устанавливают правила образования терминальных символов математической теории.
Под аксиомами понимаются элементарные утверждения, которые считаются истинными без необходимости доказательства истинности.
Правила вывода определяют правила преобразования одних символов (объектов), исследуемых в теории, в другие объекты.
Рассмотрим алфавит комбинаторной логики.
Допускаются элементы четырех видов:
- константы;
- переменные;
- комбинаторные выражения (или, иначе, термы);
- специальные символы.
При этом принимаются следующие обозначения.
Константы c 1
, c 2
, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.
Переменные x, y, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.
Выражения (или, иначе, термы) M, N, ... обозначаются заглавными буквами латинского алфавита, возможно, с индексами.
Допускается использование следующих специальных символов (взяты в кавычки и разделены запятыми): "(", ")".
Рассмотрим далее порядок конструирования допустимых для заданного алфавита комбинаторных выражений, или, иначе, термов.Комбинаторные термы строятся по индукции (порядок построения можно считать определением) следующим образом.
Базис индукции: любая переменная или константа является комбинаторным термом по определению.
Шаг индукции: если M, N - произвольные комбинаторные термы и x - произвольная переменная, то справедливо, что выражение (MN) является допустимым комбинаторным термом.
Заметим, что при этом комбинаторное выражение (MN) обозначает операцию аппликации (или применения функции к аргументу).
Кроме того, примем, что никакой другой набор символов не является допустимым комбинаторным термом.
После определения алфавита и порядка построения допустимых комбинаторных выражений посредством операции аппликации, перечислим аксиомы комбинаторной логики.
Отметим, что употребляемый ниже символ "=" понимается в комбинаторной логике как обозначение отношения конвертируемости, которым связываются соединенные этим значком комбинаторные термы. Конвертируемость двух комбинаторных термов означает, что один комбинаторный терм может быть преобразован к другому. Отношение конвертируемости моделирует переобозначения и во многих отношениях, как отмечалось ранее, напоминает процесс программирования.
Следующие аксиомы задают свойства отношения конвертируемости:
(I) Ix = x; (K) Kxy = x; (S) Sxyz = xz(yz).
Аксиома (I) означает существование комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя.
Аксиома (K) означает существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка. Интуитивно ясно, что эта аксиома близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.
