<p>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.</p>

<p>However, in a typed functional language with data types like <code>Int</code>, 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 <em>Weak Head Normal Form</em> (which is close to NOE), and it simplifies many things. See also:</p>

<ul>
<li><a href="http://www.haskell.org/haskellwiki/Weak_head_normal_form" rel="nofollow noreferrer">http://www.haskell.org/haskellwiki/Weak_head_normal_form</a></li>
<li><a href="https://en.wikibooks.org/wiki/Haskell/Graph_reduction#Weak_Head_Normal_Form" rel="nofollow noreferrer">https://en.wikibooks.org/wiki/Haskell/Graph_reduction#Weak_Head_Normal_Form</a></li>
<li><a href="https://stackoverflow.com/questions/6872898/haskell-what-is-weak-head-normal-form">https://stackoverflow.com/questions/6872898/haskell-what-is-weak-head-normal-form</a></li>
</ul>

CC BY-SA 3.0
2012-08-29T16:20:54.297Z
2012-08-29T16:20:54.297Z
2017-05-23T12:40:09.333Z
Petr
<p>They only differ if you have the leftmost outermost redex is an abstraction that isn't applied.
Something like this:</p>

<pre><code>(λz.(λx.x)z)
</code></pre>

<p>If you had</p>

<pre><code>(λz.(λx.x)z) __
</code></pre>

<p>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.</p>

CC BY-SA 3.0
2012-01-20T15:49:00.027Z
2012-03-31T03:12:35.870Z
2012-03-31T03:12:35.870Z
Theo Belaire
<p>Normal Order Reduction (NOR)
reduce the leftmost, outermost redex.</p>

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

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

<p>Does using NOE instead of NOR weaken the Normalization property?</p>

<p>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.</p>

CC BY-SA 3.0
2012-01-18T16:43:13.673Z
Is that terminology usual?  I thought “normal-order reduction” and “normal-order evaluation” are usually used synonymously.
Tsuyoshi Ito
CC BY-SA 3.0
2012-01-18T17:41:48.383Z
That is the way it was covered in class.
Theo Belaire
CC BY-SA 3.0
2012-01-18T19:08:10.700Z
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
CC BY-SA 3.0
2012-01-18T20:33:13.880Z
@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
CC BY-SA 3.0
2012-01-18T21:56:25.487Z
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
CC BY-SA 3.0
2012-01-19T18:54:11.700Z
I think you should check on lambda-calculus with simple types, where strong normalization holds under beta reductions.
I think that NOR is still strongly normalizing (of course the NOR normal form is not the same as the NOE normal form).
Victor
CC BY-SA 3.0
2012-04-30T21:16:19.800Z
I am not sure what you mean by "weakening" normalization property.  Normal order evaluation obviously can't find the normal form.  But it finds what is called the "weak head normal form".  (I think that is what the term is, but can't be sure.)  Try doing web search for that term.
Uday Reddy
<lo.logic><pl.programming-languages><lambda-calculus>
Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?
Theo Belaire
# Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

(Asked by: username_0 on 2012-01-18)

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.

**Tags:** lo.logic, pl.programming-languages, lambda-calculus
> **Comments:**
> **username_1**: Is that terminology usual?  I thought “normal-order reduction” and “normal-order evaluation” are usually used synonymously.  
> **username_0**: That is the way it was covered in class.  
> **username_2**: 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.  
> **username_1**: @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.  
> **username_0**: 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?  
> **username_3**: I think you should check on lambda-calculus with simple types, where strong normalization holds under beta reductions. I think that NOR is still strongly normalizing (of course the NOR normal form is not the same as the NOE normal form).  
> **username_4**: I am not sure what you mean by "weakening" normalization property.  Normal order evaluation obviously can't find the normal form.  But it finds what is called the "weak head normal form".  (I think that is what the term is, but can't be sure.)  Try doing web search for that term.  

---

## 2 answers

### Answer by username_5 on 2012-08-29. Score: 1 | Accepted answer

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:

* <http://www.haskell.org/haskellwiki/Weak_head_normal_form>
* <https://en.wikibooks.org/wiki/Haskell/Graph_reduction#Weak_Head_Normal_Form>
* <https://stackoverflow.com/questions/6872898/haskell-what-is-weak-head-normal-form>


---

### Answer by username_0 on 2012-01-20. Score: 0

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.


---

