Четыре правила

[codedot]

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

Используемые обозначения:

1) <var> - переменная;
2) <var>: <expr> - абстракция;
3) (<expr> @ <expr>) - аппликация;
4) A = B - A и B сводятся к одному и тому же терму с помощью бета-редукции.

Известно классическое определение бета-редукции:

(x: M @ A) -> M[x := A], (*)

где подстановка определяется четырьмя правилами:

1) x[x := A] = A;
2) y[x := A] = y;
3) (y: M)[x := A] = y: M[x := A];
4) (M @ N)[x := A] = (M[x := A] @ N[x := A]).

Можно заметить, что

(x: x @ A) = A; (1)

(x: y @ A) = y; (2)

ввиду (*)

(x: y: M @ A) -> (y: M)[x := A] =
= y: M[x := A] <- y: (x: M @ A),

таким образом

(x: y: M @ A) = y: (x: M @ A); (3)

ввиду (*)

(x: (M @ N) @ A) -> (M @ N)[x := A] =
= (M[x := A] @ N[x := A]) <- ((x: M @ A) @ (x: N @ A)),

таким образом

(x: (M @ N) @ A) = ((x: M @ A) @ (x: N @ A)). (4)

Полученные выше правила (1), (2), (3) и (4) приводят вычислимые выражения к нормальной форме за большее число шагов, чем "мгновенная" подстановка. Но "мгновенная" подстановка предполагает обход дерева в случае представления выражений графами. "Замедленная" же редукция с помощью правил (1)-(4) дает на каждом шаге самостоятельное выражение, равное с точностью до бета-редукции предыдущему, но более близкое к нормальной форме. Такой набор правил мог бы упростить создание машины для автоматического упрощения лямбда-выражений, основанной на представлении выражений графами, "ленивых" вычислениях и "сборке мусора", дав возможность после каждого такта работы (при условии, что любое из правил занимает один такт) иметь в памяти самостоятельное лямбда-выражение.