normal order reduction

Under this evaluation strategy an expression is evaluated by

reducing the leftmost outermost redex first. This method

will terminate for any expression for which termination is

possible, whereas applicative order reduction may not. This

method is equivalent to passing arguments unevaluated because

arguments are initially to the right of functions applied to

them. See also computational adequacy theorem.