<p>In all courses and textbooks I have seen, normal order reduction (NOR) and applicative order reduction (AOR) are defined as reducing respectively the leftmost outermost and rightmost innermost redex. Did someone ever give a more formal definition? (in some texts, I saw call-by-value and call-by-name formally defined, but IIUC, they are not exactly NOR and AOR, just in the same families of evaluation stratetgies)</p>

<p>Would the following definition of NOR be correct:</p>

<pre><code>NOR(x) = ∅
NOR(λx.B) = NOR(B)
NOR(M N) =
  if ∃ x,B | M = λx.B
  then (M N)
  else
    if NOR(M) ≠ ∅
    then NOR(M)
    else NOR(N)
</code></pre>

CC BY-SA 3.0
2011-07-28T05:49:40.603Z
You are asking us how to translate a perfectly understandable informal explanation to something involving symbolic notation. This is an exercise, not a research level question. I would suggest that you ask your question on http://stackoverflow.com/, and ask "where can I see an implementation of the normal order evaluation strategy, or at the very least written down formally?"
Andrej Bauer
CC BY-SA 3.0
2011-07-28T13:35:45.763Z
Since when is defining something formally not a "research level" matter? Any decent scientific article that proves anything either builds on formal definitions by someone else or begins with formal definitions…
Nowhere man
CC BY-SA 3.0
2011-07-28T20:43:58.680Z
In the present case the formal definition is not very challenging.
Andrej Bauer
CC BY-SA 3.0
2011-07-29T02:54:05.433Z
I never thought it to be challenging, I'm just wondering if there may be a subtle difference between my understanding of a perfectly understandable informal explanation and an hypothetically canonical formal definition. But let's face it, there's never a difference between the interpretation of something informal and its formal counterpart…
Nowhere man
CC BY-SA 3.0
2011-07-29T19:29:10.233Z
Well, for what is worth, I don't quite understand what your definition is supposed to accomplish. Normal-form evaluation should be some sort of a transition system, and you seem to be defining a function which takes a term and returns either the empty set or a term. That's a bit strange. Are you using the empty set as "no answer"?
Andrej Bauer
CC BY-SA 3.0
2011-08-16T17:29:41.220Z
As I describe it, the function returns the redex that the reduction order "selects" and, yes, the empty set would then mean "nothing".
Nowhere man
<lo.logic><pl.programming-languages><lambda-calculus>
Did someone give a formal definition of normal and applicative order?
Nowhere man
# Did someone give a formal definition of normal and applicative order?

(Asked by: username_0 on 2011-07-25)

In all courses and textbooks I have seen, normal order reduction (NOR) and applicative order reduction (AOR) are defined as reducing respectively the leftmost outermost and rightmost innermost redex. Did someone ever give a more formal definition? (in some texts, I saw call-by-value and call-by-name formally defined, but IIUC, they are not exactly NOR and AOR, just in the same families of evaluation stratetgies)
Would the following definition of NOR be correct:
NOR(x) = ∅
NOR(λx.B) = NOR(B)
NOR(M N) =
  if ∃ x,B | M = λx.B
  then (M N)
  else
    if NOR(M) ≠ ∅
    then NOR(M)
    else NOR(N)

**Tags:** lo.logic, pl.programming-languages, lambda-calculus
> **Comments:**
> **username_1**: You are asking us how to translate a perfectly understandable informal explanation to something involving symbolic notation. This is an exercise, not a research level question. I would suggest that you ask your question on http://stackoverflow.com/, and ask "where can I see an implementation of the normal order evaluation strategy, or at the very least written down formally?"  
> **username_0**: Since when is defining something formally not a "research level" matter? Any decent scientific article that proves anything either builds on formal definitions by someone else or begins with formal definitions…  
> **username_1**: In the present case the formal definition is not very challenging.  
> **username_0**: I never thought it to be challenging, I'm just wondering if there may be a subtle difference between my understanding of a perfectly understandable informal explanation and an hypothetically canonical formal definition. But let's face it, there's never a difference between the interpretation of something informal and its formal counterpart…  
> **username_1**: Well, for what is worth, I don't quite understand what your definition is supposed to accomplish. Normal-form evaluation should be some sort of a transition system, and you seem to be defining a function which takes a term and returns either the empty set or a term. That's a bit strange. Are you using the empty set as "no answer"?  
> **username_0**: As I describe it, the function returns the redex that the reduction order "selects" and, yes, the empty set would then mean "nothing".  

---

## 0 answers

