CS221/321, Fall, 2011
Homework 8
Due Wednesday, November 30, 5pm

[This is the CS221/321 Final Exam from 2010. This is not a timed
exercise, but see if you can write a draft version of your solutions
in around 2 hours, as practice for this year's final.]

1 [20]. Provide the missing frames and transition rules for products
and projections to complete the CK abstract maching for the Tfun(→,*)
language defined in the Appendix. Be careful, and test your solution,
because the "obvious" transition rules may not work (think about the
difference between Pair and App).

2 [10]. The following is a state of the CK machine for TFun(→,*) in
the midst of computing the value of an expression.
Give the final value when this CK computation is completed, if any.

  (App (Prim(plus),Pair(Num 1,Num 2)),
   [Pair ([],Num 2),
    App (Prim gt, []),
    If([],
       Fun ("x",Int,App (Prim(plus),Pair(Var "x",Num 5))),
       Fun ("y",Int,App (Prim(minus),Pair(Var "y",Num 5)))),
    Let ("f",[],Var "f"),
    App ([], App (Prim(times),Pair(Num 2,Num 4)))])

3(a) [15]. Define a typing judgement for CK states for Tfun(→,*)
having the form:

   ⊦ (e,k) : τ 

This judgement will be defined in terms of typing judgements for
frames and stacks. There will be a rule

     ⊦ e : τ    ⊦ k : (τ, τ')
   --------------------------
 	 ⊦ (e,k) : τ'

where judgements for frames and stacks will involve two types (an
input type describing the hole, and an output type describing the
return value of the frame/stack). The return type of the stack should
remain fixed and equal to the type of the initial expression. Just
give a sample frame typing rule for the If([],e2,e3) frame.

(b) [20]. State a Preservation Theorem for the CK machine with respect
to the state typing judgement from part (a), and set up a proof of
this theorem, giving details for the cases relating to If expressions
(transition rules (6) and (7) for the CK machine - (8) would be the
same as (7)).

4 [20]. Give the proof of the RE(6) case in the proof of Theorem 6.1
(Preservation) from Lecture 11.

5 [15]. Give an example of a PTFun expression where type-checking
would result in a free-variable capture if α-conversion is not used in
the type-checker when performing substitution of type expressions for
type variables. [This should be a fairly simple one-liner involving
polymorphism.]


======================================================================
Appendix: TFun(→,*)

1. Abstract Syntax

   x ::= x, y, z, f, g, ...   (alphanumeric variables)
   n ::= 0, 1, 2, ...         (natural numbers)
   b ::= true, false          (booleans)
   p ::= plus, times, minus, eq, lt, gt    (primops)

   τ ::= Int | Bool | τ → τ

   e ::= Num(n)  | Bool(b) | Prim(p) |      -- constant expressions
         Var(x) |
         If(e1, e2, e3) |
         Let(x, e1, e2) |
         Fun(x, τ, e) |
         Rec(τ1, τ2, f, x, e) |             -- μf:τ1→τ2.λx:τ1.e
         App(e1, e2) | 
         Pair(e1,e2) | Fst(e) | Snd(e)

   v ::= Num(n)  | Bool(b) | Prim(p) |
         Fun(x, τ, e) | Rec(τ1, τ2, f, x, e) |
         Pair(v1,v2)


2. Small-step transition semantics

             ( v = primApply(p,n1,n2) )
(1)  --------------------------------------------
      App(Prim(p), Pair(Num(n1),Num(n2)))  ↦  v 


(2)  App(Fun(x,τ,e), v2) ↦ [v2/x]e


       ( v1 = Rec(τ1,τ2,f,x,e) )
(2)  ----------------------------
      App(v1,v2) ↦ [v1,v2/f,x]e


              e1 ↦ e1' 
(3)  ----------------------------
      App(e1,e2) ↦ App(e1',e2)


              e2 ↦ e2'
(4)  ---------------------------
      App(v1,e2) ↦ App(v1,e2')


 (5)  Let(x, v1, e2) ↦ [v1/x]e2


                  e1 ↦ e1'
(6)  -----------------------------------
      Let(x, e1, e2) ↦ Let(x, e1', e2)


(7)  If(Bool(true),e2,e3) ↦ e2


(8)  If(Bool(false),e2,e3) ↦ e3
 

                e1 ↦ e1' 
(9)  -------------------------------
      If(e1,e2,e3) ↦ If(e1',e2,e3)


                e1 ↦ e1' 
(10)  -----------------------------
       Pair(e1,e2) ↦ Pair(e1',e2)


                e2 ↦ e2'
(11)  -----------------------------
       Pair(v1,e2) ↦ Pair(v1,e2')


(12)  Fst(Pair(v1,v2)) ↦ v1


(13)  Snd(Pair(v1,v2)) ↦ v2


            e ↦ e'
(14)  -------------------
       Fst(e) ↦ Fst(e')


            e ↦ e'
(15)  -------------------
       Snd(e) ↦ Snd(e')


where primApply(p,n1,n2) applies the primitive operation
p to (n1,n2) and returns the resulting value as a constant
expression.


----------------------------------------------------------------------
CK abstract machine for TFun(→,*)  [incomplete]

Frames: 

   f ::= App([],e) | App(v1,[]) |
         Let(x,[],e) | 
         If([],e2,e3) |
         ...              -- missing frames for Pair, Fst, Snd

Stacks:

   k ::= frame list


States:
 
   s ::= (e,k)

   Initial: (e,nil)
   Final: (v,nil)


Transition Rules:

(1) (Pair(Num(n1),Num(n2)), App(Prim(p),[]::k) => (v,k)
    where v = primApply(p,n1,n2)

(2) (App(e1,e2),k) => (e1, App([],e2)::k)

(3) (v1, App([],e2)::k) => (e2, App(v1,[])::k)

(4) (v2, App(Fun(x,τ,e),[])::k) => ([v2/x]e, k)

(5) (v2, App(Rec(τ1,τ2,f,x,e),[])::k) => ([v1,v2/f,x]e, k)
    where v1 = Rec(τ1,τ2,f,x,e)

(6) (If(e1,e2,e3), k) => (e1, If([],e2,e3)::k)

(7) (Bool(true), If([],e2,e3)::k) => (e2,k)

(8) (Bool(false), If([],e2,e3)::k) => (e3,k)

(9) (Let(x,e1,e2), k) => (e1, Let(x,[],e2)::k)

(10) (v1, Let(x,[],e2)::k) => ([v1/x]e2, k)

...  -- missing rules for Pair, Fst, Snd