Пример 6.2

(lx.ly.y) ((lz. z z) (lz.z z))

® (lx.ly.y) ((lz.z z) (lz.z z))

® (lx.ly.y) ((lz.z z) (lz.z z))

®...

(бесконечный процесс редукции)

(lx.ly.y) ((lz. z z) (lz.z z))

®ly.y

(редукция закончилась)

Порядок редукций (стратегия выбора редексов)

Самым левым редексом называется редекс, символ l которого (или идентификатор примитивной функции в случае d-редекса) текстуально расположен в l-выражении левее всех остальных редексов. (Аналогично определяется самый правый редекс.)

Самым внешним редексом называется редекс, который не содержится внутри никакого другого редекса.

Самым внутреннимредексом называется редекс, не содержащий других редексов.

В контексте функциональных языков и l-исчисления существуют два важных порядка редукций [32].

Аппликативный порядок редукций (АПР), который предписывает вначале преобразовывать самый левый из самых внутренних редексов.

Нормальный порядок редукций (НПР), который предписывает вначале преобразовывать самый левый из самых внешних редексов.

(lx.ly.y) ((lz.zz) (lz.z z)) - самый левый из самых внутренних редексов - вычисление никогда не закончится.

(lx.ly.y) ((lz.z z) (lz.zz)) - самый левый из самых внешних редексов - вычисление закончится за один шаг.

Функция lx.ly.y - это классический пример функции, которая отбрасывает свой аргумент. НПР в таких случаях эффективно откладывает вычисление любых редексов внутри выражения аргумента до тех пор, пока это возможно, в расчете на то, что такое вычисление может оказаться ненужным.

В функциональных языках стратегии НПР соответствуют так называемые ленивые вычисления. “Не делай ничего, пока это не потребуется” - механизмвызова по необходимости (все аргументы передаются функции в не вычисленном виде и вычисляются только тогда, когда в них возникает необходимость внутри тела функции). Clean - один из языков с ленивыми вычислениями.

Стратегия АПР приводит к энергичным вычислениям. “Делай все, что можешь”; другими словами, не надо заботиться о том, пригодится ли, в конечном счете, полученный результат. Таким образом, реализуется механизм вызова по значению (значение аргумента передается в тело функции). В языке Лисп реализуются, как правило, энергичные вычисления.

Следствие из теоремы Чёрча-Россера [7, с.74]. Если выражение E может быть приведено двумя различными способами к двум нормальным формам, то эти нормальные формы совпадают или могут быть получены одна из другой с помощью замены связанных переменных.

Теорема стандартизации [7, с. 298-303]. Если выражение E имеет нормальную форму, то НПР гарантирует достижение этой нормальной формы (с точностью до замены связанных переменных).