Конвертируемость

Аксиомы ламбда-исчисления

Выражения (термы)

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

Константы

Алфавит ламбда-исчисления.

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

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

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

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

4. выражения (или термы).

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

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

5.1.2. Переменные

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

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

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

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

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

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

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

1) ламбда- выражение (λx.M) является допустимым ламбда- термом и обозначает операцию абстракции;

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

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

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

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

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

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

Аксиома (a) о возможности подстановки терма z (конкретизации?) вместо всех вхождений переменной x в ламбда- выражение a.

(a) λx.a = λz.[z/x]a;

Аксиома (β) о возможности редукции (то есть упрощения вида) ламбда- выражения в левой части путем подстановки b вместо всех вхождений переменной x в ламбда- выражение a.

(β) (λx.a)b = [b/x]a.

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

Перечислим правила вывода термов, которые задают характеристики отношения конвертируемости:

(μ)	если a=b, то ca=cb
(ν)	если a=b, то ac=bc
(ξ)	если a=b, то λx.a=λx.b
(ρ)	a=a	рефлексивность - конвертируемость произвольного ламбда- выражения к самому себе
(σ)	если a=b, то b=a	симметричность - двунаправленность вывода ламбда- выражений посредством конверсии
(τ)	если a=b и b=c, то a=c	транзитивность - возможность опускать промежуточные этапы конверсии для цепочек вывода

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

Дата добавления: 2014-01-07