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


         

Рассмотрим далее порядок конструирования допустимых


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

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

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

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

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

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

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

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

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

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

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

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


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