3
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • $\begingroup$ Is that terminology usual? I thought “normal-order reduction” and “normal-order evaluation” are usually used synonymously. $\endgroup$
    – Tsuyoshi Ito
    Commented Jan 18, 2012 at 16:43
  • $\begingroup$ That is the way it was covered in class. $\endgroup$
    – Theo Belaire
    Commented Jan 18, 2012 at 17:41
  • $\begingroup$ 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. $\endgroup$
    – cody
    Commented Jan 18, 2012 at 19:08
  • 1
    $\begingroup$ @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. $\endgroup$
    – Tsuyoshi Ito
    Commented Jan 18, 2012 at 20:33
  • $\begingroup$ 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? $\endgroup$
    – Theo Belaire
    Commented Jan 18, 2012 at 21:56

2 Answers 2

Reset to default
1
$\begingroup$

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:

Improve this answer
$\endgroup$
0
$\begingroup$

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

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

If you had

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

With some expression where the __ is, then the leftmost outermost redex is the same for both NOE, and NOR. So the only time the two evaluation strategies would differ, NOE is in normal form already. Thus it will find the normal form if it exists.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.