Аппликативная редукционная стратегия

Аппликативная редукционная стратегия — такая стратегия редукции в λ-исчислении, при которой на каждом шаге редукции выбирается β-редекс, не содержащий внутри себя других β-редексов. Аппликативная редукционная стратегия не гарантирует получения нормальной формы λ-выражения, даже в случае если она существует. В программировании аппликативная редукционная стратегия соответствует вызову по значению.

Невозможность получения нормальной формы

При редукции выражения $M = (\lambda y.x)\Omega$ аппликативная редукционная стратегия не позволяет получить нормальную форму, которая существует.

1. НРС: $(\lambda y.x)\Omega = (\lambda y.x)[y \leftarrow \Omega] = x$.
2. АРС: $(\lambda y.x)\Omega = (\lambda y.x)((\lambda x.xx)(\lambda x.xx)) = (\lambda y.x)((\lambda x.xx)(\lambda x.xx)) = \ldots$.

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

См. также

• Нормальная редукционная стратегия
• Вызов по значению
• Комбинатор Ω