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



             

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


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

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

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

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

Теперь становится возможным дать лаконичное определение комбинатора.

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

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

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

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

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

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

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

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

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

  1. константы;
  2. переменные;
  3. комбинаторные выражения (или, иначе, термы);
  4. специальные символы.

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

Константы c 1

, c 2

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

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

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

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




Содержание    Вперед