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. – Tsuyoshi Ito Jan 18 '12 at 16:43
• That is the way it was covered in class. – Theo Belaire Jan 18 '12 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 '12 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. – Tsuyoshi Ito Jan 18 '12 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? – Theo Belaire Jan 18 '12 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) __