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