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

1. АППЛИКАТИВНЫЙ порядок редукции (АПР): вначале преобразовывается самый левый из самых внутренних редексов, не содержащих других редексов:

такой порядок редукции в данном примере привел к зацикливанию.

1. НОРМАЛЬНЫЙ порядок редукции (НПР): вначале преобразовывается самый левый из самых внешних редексов, которые не содержатся в других редексах:

такой порядок редукции в данном примере привел за один шаг к окончанию вычислений.

ЗАМЕЧАНИЕ: Функция в случае НПР отбрасывает свой аргумент .

ВЫВОДЫ:

1. НПР в таких случаях эффективно откладывает вычисление любых редексов внутри выражения аргумента до тех пор, пока это возможно: «не делай ничего, пока это не потребуется». Это пример «ленивых вычислений» - стратегия НПР, которая встречается в некоторых функциональных языках, например, в алгоритмическом языке Clean.

2. Стратегия АПР соответствует “энергичным вычислениям» -«делай все, что можешь». Эта стратегия применяется в языке ЛИСП, которая может приводить иногда к зацикливанию.

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

Теорема «стандартизации»: Если выражение имеет нормальную форму (НФ), то НПР гарантирует достижение этой НФ (с точностью до замены связанных переменных).