<p>To answer your question we need some machinery and concepts from the theory of programming languages, so that we can actually make your question well posed, and then answer it.</p>

<p>You are asking whether two pieces of code are <a href="http://en.wikipedia.org/wiki/Observational_equivalence" rel="nofollow"><strong>observationally equivalent</strong></a>.</p>

<p>It is usually quite hard to determine observational equivalence with direct methods (and the sort of arguments you attempted will not work). A common one is to use <strong>adequate</strong> <a href="http://en.wikipedia.org/wiki/Denotational_semantics" rel="nofollow">denotational semantics</a>. Adequacy means: "If $p$ and $q$ have the same denotation then they are observationally equivalent". </p>

<p>In your case, the traditional <a href="http://en.wikipedia.org/wiki/Domain_theory" rel="nofollow">domain-theoretic</a> denotational semantics, for instance using $\omega$-cpos, will do the job. In the denotational semantics the difference between the two evaluation orders is manifested by the fact that in the applicative order (also known as call-by-value) every function is <em>strict</em> (it maps the bottom element to the bottom element), while under the normal order evaluation (also known as call-by-name) one may define non-strict function.</p>

<h3>First method</h3>

<p>A simple calculation shows that for the call-by-name semantics the denotation of <code>if</code> is a map $f : \{0,1,\bot\} \times D \times D \to D$, where $D$ is a domain, defined by
$$f(b,x,y) = 
\begin{cases}
\bot &amp; \text{if $b = \bot$}\\
x &amp; \text{if $b = 0$}\\
y &amp; \text{if $b = 1$}
\end{cases}
$$
while the denotation of <code>if-new</code> is exactly the same. Because denotational semantics is adequate, we may conclude that <code>if</code> and <code>if-new</code> are observationally equivalent.</p>

<p>It is instructive to see what the denotation is for the strict semantics (applicative order). The semantics of <code>if</code> remains the same, while the semantics of <code>if-new</code> is a map $g : \{0,1,\bot\} \times D \times D \to D$, where $D$ is a domain, defined by
$$g(b,x,y) = 
\begin{cases}
\bot &amp; \text{if $b = \bot$ or $x = \bot$ or $y = \bot$}\\
x &amp; \text{if $b = 0$}\\
y &amp; \text{if $b = 1$}
\end{cases}
$$
This is <em>not</em> sufficient to conclude that <code>if</code> and <code>if-new</code> are observationally inequivalent (because the denotational semantics is not fully abstract), but you already gave a specific example which shows that they are different under applicative order.</p>

<h3>Second method</h3>

<p>The first method is an application of the general rule that denotationally equal programs are observationally equal. It requires us to always deal with domain theory. Another method is to derive useful <em>general</em> laws that we can then use to argue about observational equivalence. In your case we need the law of <strong>$\beta$-equivalence</strong>, which says that
<code>((lambda (x) e1) e2)</code> is observationally equal to <code>e1</code> with <code>e2</code> substituted for <code>x</code>. This law does <em>not</em> hold under applicative order, but it does for normal order. So we may calculate:</p>

<ul>
<li><code>(if-new p a b)</code> is observationally equivalent to</li>
<li><code>((lambda (x y z) (if x y z)) p a b)</code> is observationally equivalent to</li>
<li><code>((lambda (y z) (if p y z)) a b)</code> is observationally equivalent to</li>
<li><code>((lambda (z) (if p a z)) b)</code> is observationally equivalent to</li>
<li><code>(if p a b)</code></li>
</ul>

<p><strong>Caveat:</strong> I am doing all this under the assumption that we are working in a fragment of Scheme which is purely functional (no side effects other than divergence).</p>

CC BY-SA 3.0
2014-10-19T10:05:41.207Z
Thanks. This is a brilliant answer. What I attempted to was lame actually. Thanks
Jatin
CC BY-SA 3.0
2014-10-19T10:45:13.960Z
Is there any normal based scheme implementation where I can try running for fun?
Jatin
CC BY-SA 3.0
2014-10-19T15:23:03.083Z
That would be Haskell.
Andrej Bauer
CC BY-SA 3.0
2014-10-19T09:45:06.750Z
2014-10-19T09:56:27.827Z
2014-10-19T09:56:27.827Z
Andrej Bauer
<p>I have been reading <code>SICP</code> and have been thinking over a thing for quite some time related to evaluation using Substitution with <code>Applicative-order</code> vs <code>Normal-Order</code>.</p>

<p>Suppose, I have defined my own <code>if-new</code> clause which is supposed to behave exactly as <code>if</code></p>

<pre><code>(define (if-new predicate a b) 
        (cond (predicate a)(else b)))
</code></pre>

<p>This is not same as <code>if</code> in a runtime that evaluates in <code>Applicative-Order</code>. Example:</p>

<pre><code>(define (p) (p))
(if (= 0 0) 0 (p)) ; This evaluates to 0.

; In case of 'if-new`
(if-new (= 0 0) 0 (p)) ; Infinite self-recursive iterative loop
</code></pre>

<p>But say it was evaluated in <code>Normal-order</code> then it will evaluate to <code>0</code>.</p>

<p>So can I say, for a runtime which evaluates in <code>Normal-Order</code>, is <code>if-new</code> same as <code>if</code>?</p>

<p>PS: I could not think of any counter examples. I tried to solve it mathematically by proof of contradiction but I am not sure of its correctness.</p>

<p>Proof by Contradiction: Hypothesis: A runtime which evaluates in <code>Normal-Order</code>, <code>(if-new p a b)</code> is not same as <code>(if p a b)</code>
               where p,a,b are deterministic expressions and pure procedures. (i.e. when evaluated they return the same value always)</p>

<p>Then ∃(p a b) such that (if-new p a b) => x1 and (if p a b) => x2. And x1 != x2 (=> represents evaluation)</p>

<p>a' represents that a has been evaluated.</p>

<p>Case-1: p whenever evaluated, returns true</p>

<pre><code>   (if-new p a b) =&gt; (cond (p a)(else b)) =&gt; (cond (p' a)(else b)) =&gt; a'

   (if p a b) =&gt; p' =&gt; a'
</code></pre>

<p>Case-2: p whenever evaluated, returns false</p>

<pre><code>   (if-new p a b) =&gt; (cond (p a)(else b)) =&gt; (cond (p' a)(else b)) =&gt; b'

   (if p a b) =&gt; p' =&gt; b'
</code></pre>

<p>In each of the case, both the expressions provide the same result. This is a contradiction as our assumption suggests they are different. Hence proved</p>

CC BY-SA 3.0
2014-10-19T09:26:55.663Z
Not everyone on this planet knows what "SICP" refers to.
Andrej Bauer
<functional-programming><lisp><scheme>
Can we design our own `if` clause in Normal Order evaluation
Jatin
# Can we design our own `if` clause in Normal Order evaluation

(Asked by: username_0 on 2014-10-19)

I have been reading SICP and have been thinking over a thing for quite some time related to evaluation using Substitution with Applicative-order vs Normal-Order.
Suppose, I have defined my own if-new clause which is supposed to behave exactly as if
(define (if-new predicate a b) 
        (cond (predicate a)(else b)))

This is not same as if in a runtime that evaluates in Applicative-Order. Example:
(define (p) (p))
(if (= 0 0) 0 (p)) ; This evaluates to 0.

; In case of 'if-new`
(if-new (= 0 0) 0 (p)) ; Infinite self-recursive iterative loop

But say it was evaluated in Normal-order then it will evaluate to 0.
So can I say, for a runtime which evaluates in Normal-Order, is if-new same as if?
PS: I could not think of any counter examples. I tried to solve it mathematically by proof of contradiction but I am not sure of its correctness.
Proof by Contradiction: Hypothesis: A runtime which evaluates in Normal-Order, (if-new p a b) is not same as (if p a b)
               where p,a,b are deterministic expressions and pure procedures. (i.e. when evaluated they return the same value always)
Then ∃(p a b) such that (if-new p a b) => x1 and (if p a b) => x2. And x1 != x2 (=> represents evaluation)
a' represents that a has been evaluated.
Case-1: p whenever evaluated, returns true
   (if-new p a b) => (cond (p a)(else b)) => (cond (p' a)(else b)) => a'

   (if p a b) => p' => a'

Case-2: p whenever evaluated, returns false
   (if-new p a b) => (cond (p a)(else b)) => (cond (p' a)(else b)) => b'

   (if p a b) => p' => b'

In each of the case, both the expressions provide the same result. This is a contradiction as our assumption suggests they are different. Hence proved

**Tags:** functional-programming, lisp, scheme
> **Comments:**
> **username_1**: Not everyone on this planet knows what "SICP" refers to.  

---

## 1 answers

### Answer by username_1 on 2014-10-19. Score: 5 | Accepted answer

To answer your question we need some machinery and concepts from the theory of programming languages, so that we can actually make your question well posed, and then answer it.

You are asking whether two pieces of code are [**observationally equivalent**](http://en.wikipedia.org/wiki/Observational_equivalence).

It is usually quite hard to determine observational equivalence with direct methods (and the sort of arguments you attempted will not work). A common one is to use **adequate** [denotational semantics](http://en.wikipedia.org/wiki/Denotational_semantics). Adequacy means: "If $p$ and $q$ have the same denotation then they are observationally equivalent".

In your case, the traditional [domain-theoretic](http://en.wikipedia.org/wiki/Domain_theory) denotational semantics, for instance using $\omega$-cpos, will do the job. In the denotational semantics the difference between the two evaluation orders is manifested by the fact that in the applicative order (also known as call-by-value) every function is *strict* (it maps the bottom element to the bottom element), while under the normal order evaluation (also known as call-by-name) one may define non-strict function.

### First method

A simple calculation shows that for the call-by-name semantics the denotation of `if` is a map $f : \{0,1,\bot\} \times D \times D \to D$, where $D$ is a domain, defined by
$$f(b,x,y) =
\begin{cases}
\bot & \text{if $b = \bot$}\\
x & \text{if $b = 0$}\\
y & \text{if $b = 1$}
\end{cases}
$$
while the denotation of `if-new` is exactly the same. Because denotational semantics is adequate, we may conclude that `if` and `if-new` are observationally equivalent.

It is instructive to see what the denotation is for the strict semantics (applicative order). The semantics of `if` remains the same, while the semantics of `if-new` is a map $g : \{0,1,\bot\} \times D \times D \to D$, where $D$ is a domain, defined by
$$g(b,x,y) =
\begin{cases}
\bot & \text{if $b = \bot$ or $x = \bot$ or $y = \bot$}\\
x & \text{if $b = 0$}\\
y & \text{if $b = 1$}
\end{cases}
$$
This is *not* sufficient to conclude that `if` and `if-new` are observationally inequivalent (because the denotational semantics is not fully abstract), but you already gave a specific example which shows that they are different under applicative order.

### Second method

The first method is an application of the general rule that denotationally equal programs are observationally equal. It requires us to always deal with domain theory. Another method is to derive useful *general* laws that we can then use to argue about observational equivalence. In your case we need the law of **$\beta$-equivalence**, which says that
`((lambda (x) e1) e2)` is observationally equal to `e1` with `e2` substituted for `x`. This law does *not* hold under applicative order, but it does for normal order. So we may calculate:

* `(if-new p a b)` is observationally equivalent to
* `((lambda (x y z) (if x y z)) p a b)` is observationally equivalent to
* `((lambda (y z) (if p y z)) a b)` is observationally equivalent to
* `((lambda (z) (if p a z)) b)` is observationally equivalent to
* `(if p a b)`

**Caveat:** I am doing all this under the assumption that we are working in a fragment of Scheme which is purely functional (no side effects other than divergence).

> **Comments:**
> **username_0**: Thanks. This is a brilliant answer. What I attempted to was lame actually. Thanks  
> **username_0**: Is there any normal based scheme implementation where I can try running for fun?  
> **username_1**: That would be Haskell.  

---

