Normal Order Reduction

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

Examples

• λx.x y →β y is a normal order reduction
• λx.λz.x y →β λz.y is a normal order reduction
• λv.λw.(λx.x w) x →βλv.λw.w x is not a normal order reduction

References

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