Введение в теорию программирования. Функциональный подход



             

Комбинаторная логика как формальная система - часть 2


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

Комбинаторные термы строятся по индукции (порядок построения можно считать определением) следующим образом.

Базис индукции: любая переменная или константа является комбинаторным термом по определению.

Шаг индукции: если M, N - произвольные комбинаторные термы и x - произвольная переменная, то справедливо, что выражение (MN) является допустимым комбинаторным термом.

Заметим, что при этом комбинаторное выражение (MN) обозначает операцию аппликации (или применения функции к аргументу).

Кроме того, примем, что никакой другой набор символов не является допустимым комбинаторным термом.

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

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

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

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

Аксиома (I) означает существование комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя.

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




Содержание  Назад