Homework 6 Solution

1.
Write the typing rules for these new constructs in the style of the
lecture. The rules you write should correspond to the type-checker
from Homework 5.

-------------------
TE |- true : bool

-------------------
TE |- false : bool


TE  |-  e1 : bool     TE  |-  e2 : t1   TE |- e3 : t1
---------------------------------------------------------
TE  |-  (if e1 then e2 else e3) : t1

TE  |-  e1 : int
-----------------------------
TE  |-  (zero?(e1)) : bool

2.  Add preconditions to the following two evaluation rules to
propagate RuntimeError:

[if-wrong]

(eval E e1) = v (not true or false)
---------------------------------------------------------
(eval E (if e1 then e2 else e3)) = RuntimeError

[zero?-wrong]

(eval E e) = v (not i)
------------------------------------------
(eval E zero?(e)) = RuntimeError

3.
What two new rules should we add for type checking values? 

true : bool

false : bool

4.  
Extend the proof of type preservation to include cases for the rules
[true], [if-true], and [if-wrong]

The type preservation theorem reads:
If eval E e = v and if E ~ TE and TE |- e : t then v : t. 

We prove this by induction on evaluation. Therefore, for each case of
evaluation, we can assume that this theorem holds for any (eval E' e')
= v' above the line.

[true]
  --------------------
  (eval E true) = true

In this case, assume that E ~ TE and TE |- true : t. Because there is
only one rule for typing the expression "true", we know that t is
bool.  Therefore we must show that the value "true" also has type
bool, which follows from the rule in part 3.


[if-true]
   (eval E e1) = true
   (eval E e2) = v
   ------------------
   (eval E (if e1 then e2 else e3)) = v 

In this case, we assume that E ~ TE and TE |- if e1 then e2 else e3 :
t. We want to show that v has type t. Because there is only one way to
type if expressions, we know that it also must be the case that
TE |- e1 : bool     
TE |- e2 : t   
TE |- e3 : t
By induction we know that the theorem hold for (eval E e2) = true.
Because TE |- e2 : t (where E ~ TE by assumption) then by induction we
can conclude that v : t.

[if-wrong]

   (eval E e1) = v (not true or false)
   ---------------------------------------------------------
   (eval E (if e1 then e2 else e3)) = RuntimeError

In this case, assume that TE |- if e1 then e2 else e3 : t. We will not
be able to show that RuntimeError has type t (it doesn't have any
type) so we will show that assuming the term type checks leads to a
contradiction.

If it does typecheck, then because there is only one way to type if 
expressions, we know that it  also must be the case that
TE |- e1 : bool     
TE |- e2 : t   
TE |- e3 : t

By induction, v : bool.  However, v is not true or false, and none of
the other values (integers or proc's) have type bool. This is a
contradiction, so we are done.