CMSC 221/321
Solutions for Final Exam
12/8/2011

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

Values:

   v ::= ... | PAIR(v1,v2)

Frames:

   f ::= ... Pair([],e2) | Pair*(v1,[]) | Fst([]) | Snd([])

   also, Bapp and Bapp* frames eliminated

Stack: no change

Environments: no change

Rules:

(1)  [omit] (Bapp(bop,e1,e2), E, k) =>  ...

(2)  [omit] (NUM(n), Bapp(prim,[],e2,E')::k) => ...

(3*) (PAIR(NUM(n),NUM(m)), App*(PRIM(p),[])::k)  =>  (NUM(r), k)
      where r = prim(p,m,n)

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

(5)  (v, Let(x,[],e2,E')::k)             =>  (e2, bind(x,v,E'), k)

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

(7)  (BOOL(true), If([],e2,e3,E')::k)    =>  (e2, E', k)

(8)  (BOOL(false), If([],e2,e3,E')::k)   =>  (e2, E', k)

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

(10) (v, App([],e2,E')::k)               =>  (e2, E', App*(v,[])::k)

(11) (v, App*(FUN(x,τ,e,E),[])::k)       =>  (e, bind(x,v,E), k)

(12) (Var(x), E, k)                      =>  (look(x,E), k)

(13) (Num n, E, k)                       =>  (NUM n, k)

(14) (Bool b, E, k)                      =>  (BOOL b, k)

(15) (Fun(x,τ,e), E, k)                  =>  (FUN(x,τ,e,E), k)

(new rules)

(16) (Pair(e1,e2), E, k)                 =>  (e1, E, Pair([],e2,E)::k)

(17) (v1, Pair([],e2,E)::k)              =>  (e2, E, Pair*(v1,[])::k)

(18) (v2, Pair*(v1,[])::k)               =>  (PAIR(v1,v2), k)

(19) (Fst(e), E, k)                      =>  (e, E, Fst([])::k)

(20) (PAIR(v1,v2), Fst([])::k)           =>  (v1, k)

(21) (Snd(e), E, k)                      =>  (e, E, Snd([])::k)
 
(20) (PAIR(v1,v2), Snd([])::k)           =>  (v2, k)

======================================================================

2(a)[5]

(21) (Rec(f,τ1,τ2,x,e), E, k)            =>  (REC(f,x,e,E), k)

2(b)[10]

(22) (v2, App(v1,[])::k) => (e, bind(x,v2,(bind(f,v1,E)), k)
     where v1 = REC(f,x,e,E)

2(c)[10] Compute App(f,Num(1)) using the CEKv machine,

    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'll drop Num, Var, and Prim constructors for brevity, as well as 
NUM, BOOL, and PRIM value constructors.  Type components, which play
no role in the computation here, will also be omitted.

(0) (App(Rec(g,x,If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1))))),1),[],[])
(1) => (Rec(g,x,If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1))))),[],[App([],1,[]])
(2) => (REC(g,x,If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1)))),[]),[],[App([],1,[]])
(3) => (1,[],[App*(G,[],[]])
       G = REC(g,x,If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1)))),[])
(4) => (If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1)))), E1, [])
       E1 = [(x,1),(g,G)]
(5) => (App(Eq,Pair(x,0)),E1,K1)
       K1 = [IF([],0,App(g,App(Minus,Pair(x,1))),E1)]
(6) => (Eq,E1,App([],Pair(x,0),E1)::K1)
(7) => (Eq,(App([],Pair(x,0),E1)::K1)    (PRIM(Eq))
(8) => (Pair(x,0),E1,App*(Eq,[])::K1)
(9) => (x,E1,Pair([],0,E1)::App*(Eq,[])::K1)
(10) => (1,Pair([],0,E1)::App*(Eq,[])::K1)
(11) => (0,E1,Pair(1,[])::App*(Eq,[])::K1)
(12) => (0,Pair(1,[])::App*(Eq,[])::K1)     (NUM(0))
(13) => (PAIR(1,0),App*(Eq,[])::K1)
(14) => (false,K1)
(15) => (App(g,App(Minus,Pair(x,1))),E1,[])
(16) => (g,E1,[App([],App(Minus,Pair(x,1)),E1)])
(17) => (G,[App([],App(Minus,Pair(x,1)),E1)])
(18) => (App(Minus,Pair(x,1)),E1,[App*(G,[])])
... (x-1: similar to (5)-(14), but with Minus instead of Eq)
(19) => (0,[App*(G,[])])
(20) => (If(App(Eq,Pair(x,0)),0,App(g,App(Minus,Pair(x,1)))), E2, [])
       E2 = [(x,0),(g,G)]
... (evaluating x=0 to get true this time, similar to (5) through (14))
(21) => (true, [If([],0,App(g,App(Minus,Pair(x,1))),E2)])
(22) => (0, E2, [])  (Num(0))
(23) => (0, [])    (NUM(0) -- final state)


================================================================================
3[10]. Typing rule for Rec expressions

     Γ, f:τ1 → τ2, x: τ1 ⊦ e : τ2
  --------------------------------------
     Γ ⊦ Rec(f, τ1, τ2, x, e) : τ1 → τ2 


================================================================================
4(a)[25]. Typing rules for TFun[*] CEKv machine

Values:

     ⊦ NUM(n) : Int
     ⊦ BOOL(n) : Int
     ⊦ PRIM(p) : Σ(p)
    
           Γ, x:τ1 ⊦ e : τ2
   ----------------------------  where  ⊦ E: Γ 
     ⊦ FUN(x,τ1,e,E) : τ1 → τ2

Environments:

       ⊦ v : τ     ⊦ E : Γ 
  ----------------------------
     ⊦ bind(x,v,E) : x:τ, Γ

Frames:

         Γ ⊦ e : τ'     ⊦ E : Γ  
(F1) -----------------------------
       App([],e,E) : (τ' → τ, τ)


           ⊦ v : τ' → τ
(F2) ------------------------
       App*(v,[]) : (τ', τ)


	 Γ ⊦ e : τ'     ⊦ E : Γ  
(F3) -----------------------------
       Pair([],e,E) : (τ, τ * τ')


		⊦ v : τ
(F4) -----------------------------
       Pair*(v,[]) : (τ', τ * τ')


Stacks: as before (in Hw 8.3)

(K1)  
     --------------------   (for arbitrary τ1, τ2)
       ⊦ nil : (τ1, τ2)
  

       ⊦ f : (τ1, τ2)    ⊦ k : (τ2, τ3)
(K2) -----------------------------------
                ⊦ f::k : (τ1, τ3)


States:

        Γ ⊦ e : τ'    ⊦ E : Γ    ⊦ k : (τ', τ)
(S1) -----------------------------------------  (e-states)
                   ⊦ (e,E,k) : τ


	⊦ v : τ'     ⊦ k : (τ', τ)
(S2) ------------------------------  (v-states)
	     ⊦ (v,k) : τ


================================================================================
4(b)[25]. App cases in proof of Preservation for type CEKv machine

Lemma [Preservation].
   ⊦ s1 : τ  &  s1 => s2  ==>  ⊦ s2 : τ

Proof:
Case 1: s1 = (App(e1,e2), E, k)  (rule (9))
  (1) s2 = (e1, E, App([],e2,E)::k)
  (2) ⊦ s1 : τ   (hyp)
  (3) let Γ = type(E)  (the unique Γ s.t. ⊦ E : Γ)
  (4) Γ ⊦ e1 : τ1 → τ2  and
  (5) Γ ⊦ e2 : τ1  and
  (6) ⊦ k : (τ2, τ)  (Inversion of (2), for some τ1, τ2)
  (7) ⊦ App([],e2,E) : (τ1 → τ2, τ2)  (F3)
  (8) ⊦ App([],e2,E) :: k : (τ1 → τ2, τ)  (S2)
  (9) ⊦ (e1, E, App([],e2,E)::k) : τ  by (S1)
  (10) ⊦ s2 : τ   [QED]

Case 2: s1 = (v1, App([],e,E)::k) (rule (10))
  (1) s2 = (e, E, App*(v1,[])::k)
  (2) ⊦ v1 : τ1 → τ2  and 
  (3) ⊦ App([],e,E) : (τ1 → τ2, τ2)  and
  (4) ⊦ k : (τ2, τ)  (Inversion, for some τ1, τ2)
  (5) Γ ⊦ e: τ1 where Γ = type(E)  (Inversion of (3))
  (6) ⊦ App*(v1, []) : (τ1, τ2)  (F2)
  (7) ⊦ App*(v1, []) :: k : (τ1, τ)
  (8) ⊦ (e, E, App*(v1,[])::k) : τ  (S1)
  (9) ⊦ s2 : τ    [QED]

Case 3: s1 = (v2, App*(v1,[])::k)  (rule yy)
Then there are two subcases:

  Case 3.1: v1 = PRIM(p)
   (1) s2 = (v5, k) where v5 = prim(p,v3,v4)
   (2) Σ(p) = Int * Int ↦ τ1 where τ1 ∈ {Int, Bool}
   (3) Then v2 = PAIR(v3,v4). (Inversion, canonical forms)
   (4) ⊦ k : (τ1, τ) and ⊦ v5 : τ1   (Inversion)
   (5) ⊦ (v5, k) : τ (S2)
   (6) ⊦ s2 : τ    [QED]

  Case 3.2: v1 = FUN(x,e,E)
   (1) ⊦ FUN(x,τ1,e,E) : τ1 → τ2 and
   (2) ⊦ App*(v1,[]) : (τ1, τ2) and
   (3) ⊦ k : (τ2, τ)  by Inversion
   (4) ⊦ v2 : τ1
   (4) s2 = (e, bind(x,v2,E), k)
   (5) Γ, x:τ1 ⊦ e : τ2  where Γ = type(E)
   (6) bind(x,v2,E) : Γ, x: τ2
   (7) ⊦ (e, bind(x,v2,E), k): τ, i.e ⊦ s2: τ   [QED]