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

Материал из свободной русской энциклопедии «Традиция»
(перенаправлено с «АРС»)
Перейти к: навигация, поиск

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

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

При редукции выражения \(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\) в случае применения аппликативной редукционной стратегии невозможно.

См. также[править]