# Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex.

Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions.

So (λw. (λx.x) z) is in normal form under NOE, but not under NOR.

Does using NOE instead of NOR weaken the Normalization property?

The Normalization property states that if there is a normal form under beta-reduction, that NOR will find it. Edit: Sorry, it's the Curry/Feys Theorem that says that NOR always finds a normal form if it exists.

• Is that terminology usual? I thought “normal-order reduction” and “normal-order evaluation” are usually used synonymously. Jan 18, 2012 at 16:43
• That is the way it was covered in class. Jan 18, 2012 at 17:41
• I'm not sure I understand the question; if you are asking whether being normalizing for NOE is weaker than being normalizing for NOR then the answer is yes as your own example shows.
– cody
Jan 18, 2012 at 19:08
• @cody: The question is confusing, but I think that I understand what the question means. Restrict a beta-reduction to a case where the redux does not occur inside a lambda-abstraction. Call an expression NOE-normal if every redux occurs inside a lambda-abstraction (that is, no restricted beta-reduction can occur). Then the question is whether the following statement holds or not: If e is an expression and there is a way to apply restricted beta-reductions repeatedly to turn e into an NOE-normal expression, then applying NOE to e necessarily ends up with the same NOE-normal expression. Jan 18, 2012 at 20:33
• We were talking about how reducing the leftmost outermost redex is an evaluation strategy that, if a normal form exists, will find it. Then we added the restriction that you can't do any reductions inside an abstraction, and I am now asking if the normal form will still be found if it exists? Jan 18, 2012 at 21:56

NOE reduction strategy (as you define it) won't find the $\beta$-normal form of a term. For example, the normal form of $\lambda x.((\lambda y.y)x)$ is $\lambda x.x$ but NOE won't find it, because it won't reduce the inner redex $(\lambda y.y)x$ which is under the outer $\lambda$-abstraction. So it's not a normalizing reduction strategy.

However, in a typed functional language with data types like Int, if you know that some expression is of such a type, you know that it cannot be a function, so it's enough to restrict reductions to so-called Weak Head Normal Form (which is close to NOE), and it simplifies many things. See also:

They only differ if you have the leftmost outermost redex is an abstraction that isn't applied. Something like this:

(λz.(λx.x)z)


(λz.(λx.x)z) __