CMSC 221/321 Fall 2011
Final Exam

1.[20] Define a CEKv machine for TFun[*].

----------------------------------------------------------------------
Fig 1: abstract syntax of TFun[*]
----------------------------------------------------------------------
   var ::= x, y, z, ...    (alphanumeric variables + symbolic variables)
   n ::= 0, 1, 2, ...    (natural numbers)
   b ::= true | false
   p ::= Plus | Times | Minus | Eq | Lt | Gt ...  (primitive operators)

   τ ::= Int | Bool | τ → τ | τ * τ 

   e ::= Num(n) | Bool(b) | Prim(p) | Var(var) |     -- atomic expressions
         If(e, e, e) |
         Let(x, e, e) |
         Fun(x, τ, e) |
         App(e, e)
         Pair(e, e) | Fst(e) | Snd(e)
----------------------------------------------------------------------

----------------------------------------------------------------------
Fig 2: Values
----------------------------------------------------------------------

   val := NUM(n) | BOOL(b) | PRIM(p)
        | FUN(var,τ,e,E) | PAIR(val,val)

   E ∈ env := (var * val) list   (association list environments)
   empty = nil
   look: var * env → val  -- as usual
   bind: var * val * env  -- as usual

Primitive operators take pairs as arguments:
   e.g. Plus : Int * Int → Int.
----------------------------------------------------------------------

Extend the solution of Hw 4.4 (provided as an Appendix to this Final)
by giving all additional or modified frames and transition rules. Note
that you will not have Bapp expressions or frames, since these are
covered by ordinary App plus Pair. Note also that the value
constructor names used here and in the Appendix (NUM, etc) differ
slightly from their names in hw4_sol.txt (NumVal, etc). Also, the
parameter type τ included in the FUN value (function closure) is
useless during evaluation, but will be necessary in Problem 4.


2. Add an expression construct Rec to TFun[*]:

   e ::= ... | Rec(f,τ1,τ2,x,e)   (f,x ∈ var)

to denote recursive functions. This corresponds to the μ-construct
described in Lecture 9 and is an alternative to the Letrec construct
included in PTFun (as implmented in ptfun.tgz).

   Rec(f,τ1,τ2,x,e) == μf:(τ1 → τ2).λx:τ1.e

The corresponding value construct for recursive function values
is

   val ::= ...  REC(f,x,e,E)   (where E ∈ env is a closure environment)

Give new CEKv transition rules for:

(a) [5] Evaluating Rec expressions to REC values.

(b) [10] Function application reduction where the function value is 
a REC(f,x,e,E) [Hint: use the environment trick --rebind f to the
REC value in the environment used to evaluate the body expression e).

(c) [10] use the extended CEKv machine to evaluate:

    App(f,Num(1))

    where f = Rec(g,Int,Int,x,
                  If(App(Prim(Eq),Pair(Var(x),Num(0))),
                     Num(0),
                     App(Var(g),App(Prim(Minus),Pair(Var(x),Num(1))))))

   i.e. f = μg:Int->Int. λx:Int. if x=0 then 0 else g(x-1)

For brevity, you can use concrete syntax (e.g.

   x-1 for App(Prim(Minus),Pair(Var(x),Num(1))))

and introduce abbreviations for repeated expressions and environments.


3. [10] Give the typing rule for expressions of the form
Rec(f,τ1,τ2,x,e) (see Lecture 9 for a related rule for μ-expressions).


4. (a) [25] Repeat the development Hw 8.3 for the CEKv machine of
Problem 1. This involves giving rules for typing

  (1) values
  (2) enviroments 

(where these two are mutually recursive, since values can contain
environments, and environments map variables to values)

  (3) frames
  (4) stacks
  (5) states (both e-states and v-states)

We assume that we can use the typing of TFun[*] expressions. Also note
that the type of an environment will be a type environment (context)
Γ.

Just give the frame typing rules for frames involving App and Pair.

(b) [25] State the Preservation Lemma for typed CEKv states, and
prove the cases where App is involved.


Bonus: [20] State and prove any two cases of the Progress Lemma
for typed CEKv.