Стратегии редукции

Какой из подтермов сворачивать раньше?
Как избежать бесконечной редукционной цепочки?

Самый внутренний (вложенный) редекс: (λx . y) ((λx.x x x) (λx.x x x))
→ (λx . y) ((λx.x x x) (λx.x x x) (λx.x x x))
→ (λx . y) ((λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x))
→ ...
Самый левый внешний редекс: (λx . y) ((λx.x x x) (λx.x x x)) → y

Самый левый внешний редекс (leftmost outermost) терма w обозначатся LOR(w) и определяется индукцией по строению терма:

`w`	LOR(`w`)
(λ`x`. `u`) `v`	(λ`x`. `u`) `v`
`u v`	LOR(`u`)
λ`x`. `u`	LOR(`u`)

Лемма

Если u → v и v имеет нф, то любая редукционная цепочка, начинающаяся с u и состоящая из применения правил к LOR, всегда завершается и приводит к терму в нф.