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}.