We want to show that if e is in tail form, then evaluating e with
call-by-name (CBN) and evaluating e with call-by-value (CBV) will
always produce the same result.

With our reduced language (no effects like printing or variable
assignment) the biggest difference between CBN and CBV is in
termination: i.e. the expression

loop = ((lambda (x) (x x)) (lambda (x) (x x)))

loop is an infinite loop with both CBN and CBV evaluation.

(eval-cbv ((lambda (x) 3) loop) env) is an infinite loop.
(eval-cbn ((lambda (x) 3) loop) env) is 3.

What we want to prove is that if  e is in tail form,
and env1 corresponds to env2 then 

(eval-cbv e env1) = v1  iff (eval-cbn e env2) = v2

and v1 corresponds to v2.

This is getting really technical. Why is it not 
env1 = env2 ?  Why is it not v1 = v2?

cbn-eval uses a different sort of environment than cbv-eval.
For CBN, the environment needs to store computations, i.e. 
pairs of expressions and environments.

(apply-env env x) = (e, env')
(cbn-eval e env') = v
---------------------
(cbn-eval x env) = v

(cbn-eval e1 env) = (closure x e1' env')
(cbn-eval e1' (extend-env env' x (e2, env))) = v
----------------------------
(cbn-eval (e1 e2) env) = v

So we can't just use the same environment when we evaluate with CBN
and CBV. But they can't be just any two environments, or the theorem
won't hold. So what is the relationship between the two environments?

Definition
cbv-env is compatible with cbn-env  if they have the same domain, and 
if (apply-env cbv-env x) = v1 and  (apply-env cbn-env x) = (e,env') 
then 
   (cbn-eval e env') = v2  where v1 is compatible with v2.

Ack, what about values. Why isn't it v1 = v2.  The problem is with
closures. They store environments. The environments stored with 
CBV will be different than the environments with CBN. 

Definition 
v1 is compatible with v2 if they are equal, or if v1 = closure e env1
and v2 = closure e env2 and env1 is compatible with env2.

Because compatibility is so close to equality, we'll use the notation 
v1 == v2 to mean that v1 is compatible with v2.

Ok. We've now understand the statement of the theorem. How do we prove
it?

In order to tell whether an expression is in tail form, we need to be
able to tell whether an expression is simple. Recall the definition of 
tail-form:

An exp is in tail-form if all non-tail positions are simple.

Therefore, we first need to prove a property about simple expressions.

-------------------------------------------------------------------

Lemma: If env1 is compatible with env2 and e is simple then 
(eval-cbv e env1) == (eval-cbn e env2) 
or both evaluations will produce a type error. 

Note, this is a *really* strong theorem. The evalation of simple
expressions will always terminate. But that was our motivation when we
defined simple expressions.

To make this theorem easier to prove, we will make the following
assumption: all expressions are well-typed, so no type errors will
occur. We can strengthen this theorem to untypable expressions by
adding the *wrong* value so that we can explicitly distinguish between
non-termination and type errors.

How do we prove this theorem? By structural induction on the
expression e. Here are a few of the cases.

Case: e is a number, i

(eval-cbv i env1) = i
(eval-cbn i env2) = i

Great! numbers are very easy.

Case: e is a variable, x

(eval-cbv x env1) = (apply-env env1 x)

(apply-env env x) = (e, env')
(eval-cbn e env') = v
-------------------------------
(eval-cbn x env2) = v

By the definition of compatible environments, we know that 
(apply-env env1 x) is compatible with v.

Case: e is a primitive application, (+ e1 e2) where e1 and e2 are
simple.

(eval-cbv e1 env1) = i1
(eval-cbv e2 env1) = i2
-------------------------------
(eval-cbv (+ e1 e2) env1) = i1 + i2

(eval-cbn e1 env1) = j1
(eval-cbn e2 env1) = j2
-------------------------------
(eval-cbn (+ e1 e2) env1) = j1 + j2

By induction, i1 == j1 and i2 == j2. So we get the same result in both
cases.

Case: e is (lambda (x1 ...) e')

(eval-cbv (lambda (x1 ...) e') env1) = (closure (x1 ...) e' env1)
(eval-cbn (lambda (x1 ...) e') env2) = (closure (x1 ...) e' env2)

These are compatible values as env1 is compatible with env2.

Case: e is (let ((x ex) ...) e') where ex and e' are simple.

By induction, (eval-cbv ex env1) = v1 and  (eval-cbn ex env2) = v2 
and v1 == v2.

So (extend env1 x v1) is compatible with (extend env2 x (ex, env2)).
So by induction,

(eval-cbv e' (extend env1 x v1)) 
  == (eval-cbv e' (extend env2 x (ex,env2)))

Which is the result of evaluating a let expressin.

Case: e is (e1 e2). Impossible, because applications are not simple.

-------------------------------------------------------------------

With this property of simple expressions, we can prove the main
theorem.

Theorem: If e is typeable and in tail form and env1 is compatible with
env2 then (eval-cbv e env1) = v1 iff (eval-cbn e env2) = v2 and
v1 == v2.

Note: the statement of this theorem lets the evaluation of e go into
an infinite loop, but both forms of evaluation must go into an
infinite loop.

The (=>) direction is actually true for all expressions for this
simple language.  We'll prove the (<=) direction by induction on
(eval-cbn e env1) = v1.  A few of the cases are below.

Case: the cbn evaluation is 
(cbn-eval (lambda (x) e) env2) = (closure x e env2)

In that case the cbv evaluation is
(cbv-eval (lambda (x) e) env1) = (closure x e env1)

Because we assumed that the environments are compatible, we know that 
the values are compatible.

Case: the cbn evaluation is 
(cbn-eval e1 env2) = (closure x e1' env2')
(cbn-eval e1' (extend-env env2' (e2, env2)) env') = v'
----------------------------
(cbn-eval (e1 e2) env2) = v'

How does cbv evaluate an application?

(cbv-eval e1 env1) = (closure x e1' env1')
(cbv-eval e2 env1) = v2
(cbv-eval e1' (extend env1' x v2)) = v
-------------------------
(cbv-eval (e1 e2) env1) = v

We want to show that v == v'

Because the expression is in tail form, we know that e1 and e2 are
both simple.

By previous lemma (cbv-eval e1 env1) = (cbn-eval e1 env2) and
	               (cbv-eval e2 env1) = (cbn-eval e2 env2).

Then (cbv-eval e1 env1) = (closure x e1' env1')
     (cbn-eval e1 env2) = (closure x e1' env2')
And env1' and env2' are compatible.

So the environments:

(extend env1' x (cbv-eval e2 env1)) and 
(extend env2' x (e2, env2)) are compatible.

So by induction:

(cbv-eval e1' (extend env1' x v2)) = v
and
(cbn-eval e1' (extend-env env2' (e2, env2)) env') = v'
and 
v = v'
which is what we wanted to show.

Case: the cbn evaluation of e is 

(cbv-eval e2 (extend env2 x (e1,env2))) = v'
------------------------------------
(cbv-eval (let (x e1) e2) env2) = v'

In that case the cbv-evaluation works like this:

(cbv-eval e1 env1) = v1
(cbv-eval e2 (extend env1 x v1)) = v
------------------------------------
(cbv-eval (let (x e1) e2) env1) = v

We know e1 is simple. So by the previous lemma, 

(cbv-eval e1 env1) = (cbn-eval e1 env2)

So the environments

(extend env1 x v1)) and (extend env2 x (e1,env2))) are compatible.

So by induction v = v'