Понятие комбинатора

Лекция 6. Комбинаторная логика как формальная система

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

Рассмотрим построение формальной системы логики. Заметим, что важнейшим понятием для любой формы комбинаторной логики является понятие комбинатора.

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

Переменная x называется свободной в ламбда-выражении (терме) вида λx.A, если она не имеет вхождений в терм A; в противном случае переменная x называется связанной.

Для составных ламбда-выражений понятие связанной и свободной переменной определяется индукцией по построению с учетом возможных способов комбинирования, а именно, операций аппликации и абстракции.

Определение 6.1. Комбинатором называется ламбда-выражение (терм), не содержащее связанных переменных.

 

6.2. Комбинаторная логика как формальная система

Согласно математической практике, необходимо определить следующие элементы теории:

  • алфавит;
  • утверждения;
  • аксиомы;
  • правила вывода.

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

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

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

Правила вывода определяют правила преобразования одних символов (объектов), исследуемых в теории, в другие объекты.

Рассмотрим алфавит комбинаторной логики.

Допускаются элементы четырех видов:

1. константы;

2. переменные;

3. комбинаторные выражения (или, иначе, термы);

4. специальные символы.

При этом принимаются следующие обозначения.

Константы c1, c2, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Переменные x, y, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Выражения (или, иначе, термы) M, N, ... обозначаются заглавными буквами латинского алфавита, возможно, с индексами.

Допускается использование следующих специальных символов (взяты в кавычки и разделены запятыми): "(", ")".

6.2.1. Правила конструирования допустимых для заданного алфавита комбинаторных выражений (термов).

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

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

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

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

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