Конвертируемость
Аксиомы ламбда-исчисления
Выражения (термы)
Специальные символы
Константы
Алфавит ламбда-исчисления.
Допускаются элементы четырех видов:
1. константы;
2. переменные;
3. специальные символы;
4. выражения (или термы).
При этом принимаются следующие обозначения.
Константы c1 , c2 , ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.
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 | транзитивность - возможность опускать промежуточные этапы конверсии для цепочек вывода |
Именно в силу фундаментальности отношения конвертируемости для ламбда-исчисления эта теория известна также под другим, более точно характеризующим ее суть названием, а именно, как исчисление ламбда-конверсий.