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.

`λx.x y →`

is a normal order reduction_{β}y`λx.λz.x y →`

is a normal order reduction_{β}λz.y`λv.λw.(λx.x w) x →`

is not a normal order reduction_{β}λv.λw.w x

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

Copyright © 2014 Barry Watson. All rights reserved.