CS221/321, Fall, 201 Homework 8 Solution 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). -------------------------------- New frames: Pair([],e) | Pair(v,[]) | Fst([]) | Snd([]) New transition rules: The "simple" idea is to add (11) (Pair(e1,e2), k) => (e1, Pair([],e2)::k) (12) (v1, Pair([],e2)::k) => (e2, Pair(v1,[])::k) (13) (v2, Pair(v1,[])::k) => (Pair(v1,v2), k) but we can't apply these rules unconditionally because then rule (11) would be applicable to the result of rule (13), because v1 and v2 are, after all, expressions, and we could get into an infinite loop. So we have to make these rules conditional: (11) (Pair(e1,e2), k) => (e1, Pair([],e2)::k) if e1 not a value (12) (Pair(v1,e2), k) => (e2, Pair(v1,[])::k) if v1 a value and e2 not a value (13) (v2, Pair(v1,[])::k) => (Pair(v1,v2), k) States of the form (Pair(v1,v2), k) where v1 and v2 are values (and hence Pair(v1,v2) is a value) will transition by one of the other rules, (3), (4), (5), or (10), or will be terminal if k = nil. The transition rules for Fst and Snd are: (14) (Fst(e), k) => (e, Fst([])::k) (15) (Snd(e), k) => (e, Snd([])::k) (16) (Pair(v1,v2), Fst([])::k) => (v1,k) (17) (Pair(v1,v2), Snd([])::k) => (v2,k) 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)))]) --------------------------- Answer: Num(13). 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 : (τ, τ') (s1) -------------------------- ⊦ (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. ---------------------------------- Rules for stack typing: (k1) ⊦ [] : (τ, τ) (for any τ) ⊦ f: (τ1, τ2) ⊦ s : (τ2, τ3) (k2) ------------------------------ ⊦ f::s : (τ1, τ3) Frame typing: ⊦ e2 : τ ⊦ e3 : τ (f-If) --------------------------- ⊦ If([],e2,e3) : (Bool, τ) We are taking advantage of the fact that the branch expressions e2 and e3 will be closed, and in general, evey frame will be closed. The Let frame typing rule is special, since the type of the body is dependent on a type assigned to the let-bound variable. Thus the Let rule is parameterized on a type τ1 for the bound variable. [x: τ1] ⊦ e2 : τ (f-Let) ------------------------- (for any τ1) ⊦ Let(x,[],e2) : (τ1, τ) (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)). -------------------------------- Prop: ⊦ (e,k) : τ & (e,k) => (e',k') ==> ⊦ (e',k') : τ Proof: By case analysis (Not Induction!) on the rule used for the transition (e,k) => (e',k'). We will do the three cases involving If. Case: by rule (6). Then e = If(e1,e2,e3), e' = e1 k' = If([],e2,e3)::k By inversion of (1) ⊦ (If(e1,e2,e3), k) : τ there exists a τ1 such that (2) ⊦ If(e1,e2,e3) : τ1 (3) ⊦ k : (τ1, τ) (4) ⊦ e1 : Bool and (5) ⊦ e2 : τ1 and (6) ⊦ e3 : τ2 by Inversion of (2) (7) ⊦ If([],e2,e3) : (Bool, τ1) by (f-If) (8) ⊦ If([],e2,e3)::k: (Bool, τ) by (k2) (9) ⊦ (e1, If([],e2,e3)::k) : τ by (s1) [X] Case: by rule (7). Then e = Bool true k = If([],e2,e3)::k1 for some e2,e3 e' = e2 k' = k1 We assume ⊦ (e,k) : τ for some τ. I.e. (1) ⊦ (Bool(true), If([],e2,e3)::k1) : τ (2) ⊦ Bool(true) : Bool (3) ⊦ If([],e2,e3)::k1 : (Bool, τ) (4) ⊦ If([],e2,e3) : (Bool, τ') and (5) ⊦ k1 : (τ', τ) for some τ', by Inversion of stack typing (6) ⊦ e2: τ' by Inversion of the If frame typing rule (7) ⊦ (e,k1) : τ by stack typing rule [X] 4 [20]. Give the proof of the (RE6) case in the proof of Theorem 6.1 (Preservation) from Lecture 11. ----------------------------------- We assume the hypotheses: (H1) (M,e) ↦ (M',e') (H2) Λ ⊦ (M,e): τ Base Case: (H1) is derived using rule (RE6). Then (1) e = DRef(l) for some location value l (2) e' = M(l) (3) M' = M (5) Λ ⊦ (M,DRef(l)) : τ by (1) and (H2) (6) Λ;∅ ⊦ l : Ref(τ) by (5) and Inversion of (RT2) (7) Λ(l) = τ by (6) and Inversion of (RT4) (8) ⊦ M:Λ by (5) and Defn 6.2 (9) Λ; ∅ ⊦ M(l) : τ by (7), (8) and Defn 6.1 (10) Λ; ∅ ⊦ e' : τ by (2) and (9) (11) Λ ⊦ (M',e') : τ by (3),(8),(10) and Defn 6.2. (12) Λ ⊆ Λ' and Λ' ⊦ (M',e') : τ where Λ' = Λ. [X] 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.] --------------------------------- (Λs.Λt.λx.s.x)[t] or TApp(TFun(s,TFun(t,Fun(x,s,x))), TVar t) Reduction of the TApp produces: Λt.λx.t.x and the substituted t has been captured by the inner Λt binding. This has the slight problem that the second type variable t is free. If we want a closed expression, we just add an outer Λt to bind it: Λt.(Λs.Λt.λx.s.x)[t] Typing this expression yields: ∀t.(∀t.t → t) and the first t in t → t is a captured instance of the outer Λt. ====================================================================== 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