CMSC 221/321 Homework set 4 Solutions Reading: Lecture 6. 4.1. [20] In Homework 3.1 you were asked to show that all evaluations of closed expressions in SAEL[SSv] terminate. The same idea used for SEA[SS] worked: the size (appropriately defined) of expressions were reduced by any transition. What about SEAL[SSn] (bind-by-name let)? (a) Show that the straightforward generalization of the size idea fails for SEAL[SSn] by giving an example where a transition yields a larger expression. (b) Try to define some more subtle measure of size of expression that might work as a basis for showing termination. [Hint: think about numbers and relative positions of Let nodes in the abstract syntax tree. This is rather difficult.] Solution: (a): Define a function size as in the proof of Homework 3.1: size (Num n) = 0 size (Var x) = 0 size (Bapp(bop, e1, e2) = size(e1) + size(e2) + 1 size (Let(x, e1, e2) = size(e1) + size(e2) + 1 Let e = Let(x, Bapp(+, 3, 5), Bapp(*, x, x). Then e ↦ Bapp(*, Bapp(+, 3, 5), Bapp(+, 3, 5)) = e' and we see that size(e) = 3 = size(e'), so in this case a transition does not reduce the size. In fact, the size can increase, as in the case where e = Let(x, Bapp(+, 3, 5), Bapp(*, x, Bapp(+, x, x)) where size(e) = 4, and e ↦ e' where size(e') = 5. (b): This is rather involved, but here is a sketch. We order the original let subexpressions of an expression e according to how they can affect one another. E.g. let1 < let2 if reducing let1 can cause let2 to be multiplied. During transitions, we maintain an ordered list of the counts of (duplicates) of these original let subexpressions, ordered by the above relation. We then prove that these lists, ordered lexicographically, get smaller with each let reduction. This lexicographic ordering of let occurrence counts is well founded, so it can only decrease a finite number of times before it is exhausted (all the counts are 0, and hence all the let expression have been eliminated). The remaining let-free expression terminates as before for SAE. ---------------------------------------------------------------------- 4.2. [10] Verify that fact = Yv Fact defines the factorial in CBV semantics by hand calculating (fact 2) using the Fun[SSv] rules. Follow the example of the calculation of (fact 2) using the CBN Y combinator in Lecture 6. Solution: We modify the CBN version given in Lecture 6. Let Fact = λg.λx. if x = 0 then 1 else x * g(x - 1) Then we would expect the factorial function fact to satisfy fact = Fact fact i.e. fact should be a fixed-point of the "generator" functional F. So lets try fact = Yv Fact where Yv = λf.(λx.f(λy.(xx)y))(λx.f(λy.(xx)y)) Now lets try computing fact 2: fact 2 = (Yv Fact) 2 ↦ (λx.Fact(λy.xxy))(λx.Fact(λy.xxy)) 2 = g g 2 where g = λx.Fact(λy.xxy) ↦ Fact(λy.ggy) 2 = Fact f 2 where f = λy.ggy (a value!) (1) ↦ (λx. if x = 0 then 1 else x * f(x - 1)) 2 (2) ↦ if 2 = 0 then 1 else 2 * f(2 - 1) ↦ if false then 1 else 2 * f(2 - 1) ↦ 2 * f(2 - 1) ↦ 2 * f(1) (3) ↦ 2 * (g g 1) ↦ 2 * (Fact f 1) ↦ 2 * (λx. if x = 0 then 1 else x * f(x - 1)) 1 ↦ 2 * (if 1 = 0 then 1 else 1 * f(1 - 1)) ↦ 2 * (if false then 1 else 1 * f(1 - 1)) ↦ 2 * (1 * f(1 - 1)) ↦ 2 * (1 * f(0)) ↦ 2 * (1 * g g 0) ↦ 2 * (1 * (Fact f 0)) ↦ 2 * (1 * (λx. if x = 0 then 1 else x * f(x - 1)) 0) ↦ 2 * (1 * (if 0 = 0 then 1 else 0 * f(0 - 1))) ↦ 2 * (1 * (if true then 1 else 0 * f(0 - 1))) ↦ 2 * (1 * 1) ↦ 2 * 1 ↦ 2 Notes: (1) g g ↦ Fact f in CBV, since g is a value (2) CBV β-reduction, since f is a falue (3) We are properly following CBV for the application f(2-1) by evaluating the arguement (2-1) first. ---------------------------------------------------------------------- 4.3. [25] Define a CR reduction system for CBV Fun (Call-By-Value). Use this CR system to evaluate: App(Fun(x,Bapp(Plus, Num 2, Var x)), Num 3) Solution: ------------------------------------------------------------ Fun[CRv]: ------------------------------------------------------------ Contexts: C := [] | Bapp(bop, C, e) | Bapp(bop, Num(n), C) | Let(x, C, e) | If(C, e1, e2) | App(C, e) | App(v, C) (v a value expression) Redex rules: (1) Bapp(bop, Num n, Num m) ↦ Num p where p = prim(bop,n,m) (2) Let(x, v, e) ↦ [v/x]e (3) If(Bool(true), e1, e2) ↦ e1 (4) If(Bool(false), e1, e2) ↦ e2 (5) App(Fun(x,e), v) ↦ [v/x]e ------------------------------------------------------------ e = App(Fun(x,Bapp(Plus, Num 2, Var x)), Num 3) = C1[App(Fun(x,Bapp(Plus(Num 2, Var x))), Num 3)] where C1 = [] ↦ C1[Bapp(Plus, Num 2, Num 3)] (redex rule (5)) = Bapp(Plus, Num 2, Num 3) = C2[Bapp(Plus, Num 2, Num 3)] where C2 = [] ↦ C2[Num 5] = Num 5 ---------------------------------------------------------------------- 4.4. [25] Define a CEK abstract machine for CBV Fun. Solution: ------------------------------------------------------------ Fun[CEKv] ------------------------------------------------------------ Values: v ::= NumVal(n) | BoolVal(b) | FunVal(x, e, E) -- closure Frames: f ::= Bapp(bop, [], e2, E) | Bapp*(bop, n, []) | Let(v, [], e2, E) | If([], e1, e2, E) | App([], e2, E) | App*(v1, []) Stack/Context: k = nil | f :: k Environments: E ∈ env = (variable * value) list emptyEnv : env = [] look : variable * env -> Nat look (v, []) = undef look (v, ((v',n):env)) = if v=v' then n else look(v, env) bind : variable * Nat * env -> env bind (v, n, env) = (v,n)::env States: s = (e, E, k) or (v, E, k) Initial states: (e, emptyEnv, []) (where e is an expression to be evaluated, and [] is the empty stack) Final states: (v, E, []) (where value v is the final result) Transition rules: (1) (Bapp(bop,e1,e2), E, k) => (e1, E, Bapp(bop,[],e2,E)::k) (2) (NumVal(n), E, Bapp(bop,[],e2,E')::k) => (e2, E', Bapp*(bop,n,[])::k) (3) (NumVal(n), E, Bapp*(bop,NumVal(m),[])::k) => (NumVal(p), E, k) where p = prim(bop,m,n) (4) (Let(v,e1,e2), E, k) => (e1, E, Let(v, [], e2, E)::k) (5) (v, E, 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) (BooVal(true), E, If([],e2,e3,E')::k) => (e2, E', k) (8) (BooVal(false), E, If([],e2,e3,E')::k) => (e2, E', k) (9) (App(e1,e2), E, k) => (e1, E, App([],e2,E)::k) (10) (v, E, App([],e2,E')::k) => (e2, E', App*(v,[])::k) (11) (v, E, App*(FunVal(x,e,E'),[])::k) => (e, bind(x,v,E'), k) (12) (Var(x), E, k) => (look(x,E), E, k) (13) (Num n, E, k) => (NumVal n, E, k) (14) (Bool b, E, k) => (BoolVal b, E, k) (15) (Fun(x,e), E, k) => (FunVal(x,e,E), E, k) ------------------------------------------------------------------ Notes: Because our values now include closures (FunVal), we can no longer treat values as a subset of expressions. So we have to define a new value type separate from, but partially overlapping the expression type. A second version ---------------- Observe that the environment components of the result state of transition rules (3), (6), (13), (14), and (15) are not going to used, and similarly for the starting state of the rules (2), (3), (5), (8), (9), (11), and (12) the environment component does not appear in the result state. These are the states where the control component (the first element of the state triple) is a value being returned as an intermeditae result rather than an expression to be evaluated. We could therefore divide the state set into two components: (e, E, k) - states where we are beginning to evaluate expr e (v, k) - where we are returning value v as an intermediate result We can distinguish these two forms by calling the first "expression states", abbreviated as "e-states",and the second form "value states" or "v-states". The modified rules, with redundant environment components removed, will then be as follows: (1) (Bapp(bop,e1,e2), E, k) => (e1, E, Bapp(bop,[],e2,E)::k) (2) (NumVal(n), Bapp(bop,[],e2,E')::k) => (e2, E', Bapp*(bop,n,[])::k) (3) (NumVal(n), Bapp*(bop,NumVal(m),[])::k) => (NumVal(p), k) where p = prim(bop,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) (BoolVal(true), If([],e2,e3,E')::k) => (e2, E', k) (8) (BoolVal(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*(FunVal(x,e,E'),[])::k) => (e, bind(x,v,E'), k) (12) (Var(x), E, k) => (look(x,E), k) (13) (Num n, E, k) => (NumVal n, k) (14) (Bool b, E, k) => (BoolVal b, k) (15) (Fun(x,e), E, k) => (FunVal(x,e,E), k) Here we find that the transitions can be characterized as follows: e-state => e-state: (1), (4), (7), (9) the analysis transitions e-state => v-state: (12), (13), (14), (15) evaluating variables and "value expressions" v-state => v-state: (3) reducing Bapp redexes v-state => e-state: (2), (5), (7), (8), (10), (11) shift transitions ((2), (10)) and reductions ((5), (7), (8), (11)) ---------------------------------------------------------------------- 4.5. [20] Write an SML program implementing the Fun[CEKv] machine from problem 4.4. Test Fun programs to evaluate will be provided later. Solution: For implementation in SML, it is more convenient to use the second variant of the rules in Homework 4.4 above, where the states have been split into e-states and v-states. Otherwise there is a complication in defining the type of a unified state, since the first component could be a value or and expression. hw_4_5.sml implements the split-state version.