Applicative Order Reduction

In the lambda calculus an applicative order reduction is a beta reduction where the λ-subterm that is reduced is the innermost-leftmost of all possible λ-subterms that could be reduced.

Examples

• λx.x y →β y is an applicative order reduction
• λv.λw.(λx.x w) x →βλv.λw.w x is an applicative order reduction
• λv.λw.(λx.x w) x →βλw.(λx.x w) is not an applicative order reduction

References

W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.