I have been reading
SICP and have been thinking over a thing for quite some time related to evaluation using Substitution with
Suppose, I have defined my own
if-new clause which is supposed to behave exactly as
(define (if-new predicate a b) (cond (predicate a)(else b)))
This is not same as
if in a runtime that evaluates in
(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
So can I say, for a runtime which evaluates in
if-new same as
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
(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