normal order reduction


normal order reduction

Under this evaluation strategy an expression is evaluated byreducing the leftmost outermost redex first. This methodwill terminate for any expression for which termination ispossible, whereas applicative order reduction may not. Thismethod is equivalent to passing arguments unevaluated becausearguments are initially to the right of functions applied tothem. See also computational adequacy theorem.