Can we design our own `if` clause in Normal Order evaluation

Question

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

Answer 1

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.

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. Adequacy means: "If $p$ and $q$ have the same denotation then they are observationally equivalent".

In your case, the traditional domain-theoretic 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).