670 Midterm sample solution
Q1) Details are left out.
a) and c) are valid, i.e. proof trees exists.
b) is invalid. Note that x:Int but x:=true requires x:Bool.
Q2)
a)
do c while e is equivalent to c ; while e do c
b)
while e do c is equivalent to if e then (do c while e)
else skip
c)
typing rule:
G |- c:Cmd G |- e:Bool
----------------------------
G |- do c while e : Cmd
operational semantics
S |- c => S' S' |- e => True
S' |- do c while e => S''
----------------------------
S |- do c while e => S''
S |- c => S' S' |- e => False
--------------------------------
S |- do c while e => S'
Q3)
a)
G |- ex : Ex
-----------------
G |- raise ex : Cmd
G |- ex : Ex G |- c1 : Cmd G |- c2 : Cmd
-----------------------------------------------
G |- handle ex = c1 in c2 : Cmd
b)
I introduce a new exception `fac' for the factorial function
var in:= 0 in
var out := 0 in
handle fac = x:= in; -- we assign the input value to x
if x = 0 then out:=1 -- equivalent to return 1
else var n:=1 in
(while (x > 1) do
(n:= n*x; x:= x-1;))
out:= n; -- equivalent to return n
in
in:= 10;
raise fac;
res1:= out;
in: = 5;
raise fac;
res2:= out;
c)
We can't encode the recursive definition of factorial because
within the exception handler we can't raise the exception itself.
We could change the semantics of exceptions and allow for
a `recursive' raise. In fact, this is described in ImpException.hs
4)
a) see lecture notes
b) take Omega = (lambda x. x x) (lambda x. x x)
then (lambda x. lambda y. y) Omega terminates under CBN but
doesn't terminate under CNV