In this homework, you will extend the proof of type soundness that we talked about in class to a language with boolean values.
Consider an extension of the simply-typed language given in lecture that includes the boolean values true and false, the zero? primitive, and if. It also includes a new type "bool", and true and false are possible values of evaluation.
e ::= i | proc (t x) e | (e1 e2) | (e1 + e2) | true | false | if e1 then e2 else e3 | zero?(e) v ::= i | ProcVal(t,x,e,E) | true | false | RuntimeError t ::= int | t1 -> t2 | boolThe following new rules describing the evaluation of these new terms (for convenience, each rule has a name in square brackets):
[true] (eval E true) = true [false] (eval E false) = false [if-true] (eval E e1) = true (eval E e2) = v ------------------ (eval E (if e1 then e2 else e3)) = v [if-false] (eval E e1) = false (eval E e3) = v ------------------ (eval E (if e1 then e2 else e3)) = v [zero?-zero] (eval E e1) = 0 ------------------ (eval E zero?(e1)) = true [zero?-nonzero] (eval E e1) = i (not 0) -------------------------- (eval E zero?(e1)) = false
[if-wrong] ??????? ------------------------------ (eval E (if e1 then e2 else e3)) = RuntimeError [zero?-wrong] ?????? ------------------------------- (eval E zero?(e)) = RuntimeError