CS221/321, Fall 2011 Midterm Solutions Total of 100 points possible. 1 [10]. Free and bound variables, free variable capture. (a) For the following expression λx. let y = x + y in let x = let u = 5 in x + u * y in (λw.x + u) (let z = w + 2 in z * y) (i) underline all occurrences of free variables; (ii) number all variable binding occurrences, placing the number above the variable; (iii) write the number of the associated binding occurrence beneath each bound occurrence of a variable. 1 E.g. let a = 3 in a + b 1 - Solution: the annotated expression is 1 2 λx. let y = x + y 1 - 3 4 in let x = let u = 5 in x + u * y 3 4 2 5 6 in (λw.x + u) (let z = w + 2 in z * y) 3 - - 6 2 --------------- (b) Give the expression resulting from the substitution [e1/x]e2, where e1 = let y = x + u in λv. x + y + z e2 = let y = λx. x + u in let u = 3 in (λz. x + v) u use the minimal number of α-conversions (that is, changes in bound variable names) needed to avoid any free variable captures. I suggest bound variable changes of the form a to a’ (i.e. just add primes). Solution: [e1/x]e2 = let y = λx. x + u in let u' = 3 in (λz'.(let y = x + u in λv. x + y + z) + v) u' We had to α-convert the let-bound u and the λ-bound z in e2 to avoid capturing the free variables u and z appearing in e1. They remain free in the result expression. ---------------------------------------------------------------------- 2 [15] Inductive principles. For each of the inductively defined data structures (i.e., sets of terms) below, write the corresponding Inductive Principle as a logical formula. (a) lists of natural numbers: list ::= Nil | Cons(nat, list) where nat ranges over the natural numbers (nat ∈ Nat). Solution: (P(Nil) & (* base case *) ∀l ∈ list. (P(l) => ∀n ∈ Nat. P(Cons(n,l)))) (* induction case *) => ∀l ∈ list. P(l) ---------------- (b) derivations of the relation s ↦* s', according to the rules s ↦ s0 s0 ↦* s' ---------------- (1) --------------------- (2) s ↦* s s ↦* s' as given in the Appendix of Lecture 2 (where ↦ is a transition relation over some given set of states S). Solution: The set of Derivations can be defined as abstract terms by the abstract syntax: D ::= R1(s) (rule (1) for state s ∈ S) | R2(s,D') (rule (2) for state s, subderivation D') with the proviso that R2(s,D') is a valid derivation term only if s ↦ source(D') for the given transition relation. Functions source and target are defined on derivations as follows: source(R1(s)) = s target(R1(s) = s source(R2(s,D)) = s target(R2(s,D)) = target(D). The Induction Principle for derivations of s ↦* s' is: (∀s. P(R1(s)) & ∀D. (P(D) => ∀s.(s ↦ source(D) => P(R2(s,D))))) => ∀D. P(D) where s ranges over states in S, and D ranges over derivations. ---------------------------------------------------------------------- 3. [35] Inductive proof. Prove the following property of the relation ↦* of 2(b) above. Assume is a transition system (Lecture 2, Appendix). Prop: For any s1,s2,s3 in S, s1 ↦* s2 and s2 ↦* s3 => s1 ↦* s3. I.e. ↦* is a transitive relation on S. Solution: The proof is by induction on the derivation of the first hypothesis: s1 ↦* s2. But it best to rephrase the proposition directly in terms of derivations, as defined in question 2(b) above: ∀D. ∀D1. target(D) = source(D1) => ∃D2. source(D2) = source(D) & target(D2) = target(D1) or ∀D. P(D), where P(D) = ∀D1. target(D) = source(D1) => ∃D2. source(D2) = source(D) & target(D2) = target(D1) Case: D = R1(s). Assume D1 is such that source(D1) = s = target(D). Let D2 = D1. Then source(D2) = source(D1) = s = source(D) & target(D2) = target(D1). [X] Case: D = R2(s,D0). We can assume D is valid, i.e. source(D0) = s, since if source(D0) /= s the inductive clause of the I.P. is true vacuously. I.H. P(D0) Let D1 be such that source(D1) = target(D) = target(D0). Then by I.H., ∃D2. source(D2) = source(D0) & target(D2) = target(D1). Let D3 = R(s,D2) for such a D2. Then source(D3) = s = source(D) & target(D3) = target(D2) = target(D1). [X] ---------------------------------------------------------------------- 4. [15] SEAL[CEKv] computation. Give the complete transition sequence to evaluate the expression let y = 2 + 5 in y * 3 using the SEAL[CEKv] abstract machine (Lecture 5, Figure 2.12). Solution: As usual, we'll omit the Num and Var constructors. The number of the rule used in each transition is at the left margin. e = Let(y, Bapp(Plus,2,5), Bapp(Times,y,3) (e, E0, []) (where E0 = emptyEnv = []) (4) => (Bapp(Plus, 2, 5), E0, Let(y,[],Bapp(Times,y,3),E0)::[]) (1) => (2, E0, Bapp(Plus,[],5,E0)::Let(y,[],Bapp(Times,y,3),E0)::[]) (2) => (5, E0, Bapp*(Plus,2,[])::Let(y,[],Bapp(Times,y,3),E0)::[]) (3) => (7, E0, Let(y,[],Bapp(Times,y,3),E0)::[]) (5) => (Bapp(Times,y,3), E1, []) where E1 = bind(y,7,E0) = [(y,7)] (1) => (y, E1, Bapp(Times,[],3,E1)::[]) (6) => (7, E1, Bapp(Times,[],3,E1)::[]) (2) => (3, E1, Bapp*(Times,7,[])::[]) (3) => (21, E1, []) ---------------------------------------------------------------------- 5. [25] Suppose that for some expressions e, e', and stack k, we have (e, k) =>* (e', k) in the SEAL[CKv] machine. How could e and e' be related? [Hint 1: Think of what the top frame (if any) of k could possibly be. Hint 2: There are 5 possibilities.] Solution: [Note: The hints are unfortunately misleading, especially the second one suggesting there were 5 possible situations. Actually, the 3 situations below cover all the possibilities.] What we are looking for are the machine configurations that allow some number of transitions to occur, resulting in a state with the same stack as the original state. (1) e' = e and (e, k) =>* (e, k) in 0 transitions. (2) For any compound (non-value) expression e, and any stack k, there is a transition sequence (e, k) =>* (Num(n), k) where e evaluates to Num(n). Note that e will always be a closed, and therefore self-contained, expression for any state (e, k). e can be a Bapp or Let expression. (3) The initial state is of the form (Let(v,e1,e2), k) i.e. the lhs of the rule (7) transition: (Let(v,e1,e2), k) => (e1, Let*(v, [], e2)::k) (by rule (7)) now we are in situation (4) above, and a transition sequence leads to the state where we have just evaluated e1: (e1,Let*(v, [], e2)::k) =>* (Num(m), Let*(v, [], e2)::k) and now by rule (8) we have (Num(m), Let*(v, [], e2)::k) => ([m/v]e2, k) so we have restored the original stack k.