CMSC 221/321 Homework Set 2 Solutions By Dave MacQueen and Lamont Samuels 2.0: Reading: Lectures 3 and 4. 2.1: (Lectures 2,3) Evaluate (2 + 3 * 4) * (5 * 6) by hand using (a) SAE[BS], (b) SAE[SS], (c) SAE[CR], and (d) SEA[CK]. The representation of the expression in SAE abstract syntax is: Times(Plus(Num 2, Times(Num 3, Num 4)), Times(Num 5, Num 6)) (a) SAE[BS] ---------- (1) --------- (1) Num 3 ⇓ 3 Num 4 ⇓ 4 --------- (1) -------------------------- (3) --------- (1) --------- (1) Num 2 ⇓ 2 Times(Num 3, Num 4) ⇓ 12 Num 5 ⇓ 5 Num 6 ⇓ 6 ----------------------------------------- (2) --------------------------- (3) Plus(Num 2, Times(Num 3, Num 4)) ⇓ 14 Times(Num 5, Num 6) ⇓ 30 ------------------------------------------------------------------------------- (3) Times(Plus(Num 2, Times(Num 3, Num 4)), Times(Num 5, Num 6)) ⇓ 420 (b) SAE[SS]. There are 4 transitions, each with its own derivation: ------------------------------ (2) Times(Num 3, Num 4) ↦ Num 12 -------------------------------------------------------- (4) Plus(Num 2, Times(Num 3, Num 4)) ↦ Plus(Num 2, Num 12) ---------------------------------------------------------------------------------------------------------------- (3) 1. Times(Plus(Num 2, Times(Num 3, Num 4)), Times(Num 5, Num 6)) ↦ Times(Plus(Num 2, Num 12), Times(Num 5, Num 6)) ------------------------------ (1) Plus(Num 2, Num 12) ↦ Num 14 -------------------------------------------------------------------------------------- (3) 2. Times(Plus(Num 2, Num 12), Times(Num 5, Num 6)) ↦ Times(Num 14, Times(Num 5, Num 6)) ------------------------------ (2) Times(Num 5, Num 6) ↦ Num 30 ------------------------------------------------------------ (6) 3. Times(Num 14, Times(Num 5, Num 6)) ↦ Times(Num 14, Num 30) ---------------------------------- (2) 4. Times(Num 14, Num 30) ↦ Num 420 (c) SAE[CR] Times(Plus(Num 2, Times(Num 3, Num 4)), Times(Num 5, Num 6)) = C1[Times(Num 3, Num 4)], where C1 = Times(Plus(Num 2, []), Times(Num 5, Num 6)) ↦ C1[Num 12] = Times(Plus(Num 2, Num 12), Times(Num 5, Num 6)) = C2[Plus(Num 2, Num 12)], where C2 = Times([], Times(Num 5, Num 6)) ↦ C2(Num 14) = Times(Num 14, Times(Num 5, Num 6)) = C3[Times(Num 5, Num 6)], where C3 = Times(Num 14, []) ↦ C3[Num 30] = Times(Num 14, Num 30) = C4[Times(Num 14, Num 30)], where C4 = [] ↦ C4[Num 420] = Num 420 (d) SAE[CK] (Times(Plus(Num 2, Times(Num 3, Num 4)), Times(Num 5, Num 6)), []) => [A] (Plus(Num 2, Times(Num 3, Num 4)), Times([], Times(Num 5, Num 6))::[]) => [A] (Num 2, Plus([], Times(Num 3, Num 4))::Times([], Times(Num 5, Num 6))::[]) => [S] (Times(Num 3, Num 4), Plus*(Num 2, [])::Times([], Times(Num 5, Num 6))::[]) => [A] (Num 3, Times([], Num 4)::Plus*(Num 2, [])::Times([], Times(Num 5, Num 6))::[]) => [S] (Num 4, Times*(Num 3, [])::Plus*(Num 2, [])::Times([], Times(Num 5, Num 6))::[]) => [R] (Num 12, Plus*(Num 2, [])::Times([], Times(Num 5, Num 6))::[]) => [R] (Num 14, Times([], Times(Num 5, Num 6))::[]) => [S] (Times(Num 5, Num 6), Times*(Num 14, [])::[]) => [A] (Num 5, Times([], Num 6)::Times*(Num 14, [])::[]) => [S] (Num 6, Times*(Num 5, [])::Times*(Num 14, [])::[]) => [R] (Num 30, Times*(Num 14, [])::[]) => [R] (Num 420, []) 2.2: (Lecture 4) Use both SAEL[CRv] and SAEL[CRn] to compute the value of the following expression: e = let x = 4 in let y = 2 + 3 in x * (let z = 2 + x in z * z) SAEL Abstract Syntax representation: e = Let(x, Num 4, Let(y, Plus(Num 2, Num 3), Times(x, Let(z, Plus(Num 2, x), Times(z, z))))) But for compactness we will perform the computation using concrete syntax notation. (1) evaluation under SAEL[CRv]. e = C1[e] where C1 = [] (e is a redex) ↦ C1[let y = 2 + 3 in 4 * (let z = 2 + 4 in z * z)] = C2[2+3] where C2 = let y = [] in 4 * (let z = 2 + 4 in z * z) ↦ C2[5] = let y = 5 in 4 * (let z = 2 + 4 in z * z) = C3[let y = 5 in 4 * (let z = 2 + 4 in z * z)] where C3 = [] ↦ C3[4 * (let z = 2 + 4 in z * z)] = 4 * (let z = 2 + 4 in z * z) = C4[2+4] where C4 = 4 * let z = [] in z * z ↦ C4[6] = 4 * let z = 6 in z * z = C5[let z = 6 in z * z] where C5 = 4 * [] ↦ C5[6 * 6] = 4 * (6 * 6) = C6[6 * 6] where C6 = 4 * [] (same as C5) ↦ C6[36] = 4 * 36 = C7[4 * 36] where C7 = [] ↦ C7[144] = 144 (2) evaluation under SAEL[CRv] e = C1[e] where C1 = [] (e is a redex) ↦ C1[let y = 2 + 3 in 4 * (let z = 2 + 4 in z * z)] = let y = 2 + 3 in 4 * (let z = 2 + 4 in z * z) = C2[let y = 2 + 3 in 4 * (let z = 2 + 4 in z * z)] where C2 = [] ↦ C2[4 * (let z = 2 + 4 in z * z)] = 4 * (let z = 2 + 4 in z * z) = C3[let z = 2 + 4 in z * z] where C3 = 4 * [] ↦ C3[(2 + 4) * (2 + 4)] = 4 * ((2 + 4) * (2 + 4)) = C4[2 + 4] where C4 = 4 * ([] * (2 + 4)) ↦ C4[6] = 4 * (6 * (2 + 4)) = C5[2 + 4] where C5 = 4 * (6 * []) ↦ C5[6] = 4 * (6 * 6) = C6[6 * 6] where C6 = 4 * [] ↦ C4[36] = 4 * 36 = C7[4 * 36] where C7 = [] ↦ C5[144] = 144 2.3: (Lecture 3) For SAE[CR], show that for any expression e, there is a unique context C and redex r such that e = C[r]. First, there is an inaccuracy in the statement of the proposition, since if e is a value expression of the form Num(n), it does not contain a redex subexpression and there can be no C[r] factoring. So the statement needs to be amended to: Prop: If e is a non-value expression in SEA, then there exists a unique context C and redex r such that e = C[r]. Proof by induction on the structure of e. (0) P(e) = e a value or ∃!C,r. e = C[r] Defn (1) ∀e. P(e) TBS (2) Cases on structure of e (3) [Base] case: e = Num(n). e is a value. case hypo (4) P(e). logic, QED[3] (7) [Ind] case: e = Plus(e1,e2) case hypo (8) P(e1) I.H. (9) P(e2) I.H. (10) Cases on value property of e1 & e2 (11) Case: e1 & e2 are values. e1 = Num n1 & e2 = Num n2 case hypo (12) e is a redex. (11), defn redex (13) let r = e, C = [] defn (14) e = C[r] defn C[r] (15) assume e = C'[r'] (r' a redex) hypo (16) case on structure C' (17) case C' = Plus([],e2) case hypo (18) r' = Num n1 (15) defn C[r] (19) r' not a redex [X] contradiction (15) (20) case C' = Plus(e1,[]) case hypo (21) r' = Num n2 (15) defn C[r] (22) r' not a redex [X] contradiction (15) (23) case C' = [] case hypo (24) r' = e = r (15) defn C[r] (25) C' = C, r' = r (23,24) (26) e = C'[r'] => C' = C, r' = r (15,16) => Intro (27) ∃!C,r. e = C[r] (14,26) (28) P(e) QED[11] (29) Case: e1 is a value & e2 is not a value e1 = Num n1. case hypo (30) ∃ unique C2,r. e2 = C2[r] (9) (31) let C = Plus(Num n1,C2) defn (32) e = C[r] (7,30) defn C[r] (33) assume e = C'[r'] hypo (34) C' = Plus(Num n1, C2') (7,33), defn context (35) e2 = C2'[r'] (33,34) defn C[r] (36) C2' = C2, r' = r (30) uniqueness (37) C' = C, r' = r (31,34) (38) e = C'[r'] => C' = C & r' = r (33,37) => Intro (39) ∃!C,r. e = C[r] (32,38) (40) P(e) QED[29] (41) Case: e1 is not a value. case hypo (42) ∃ unique C1,r. e1 = C1[r] (8) (43) let C = Plus(C1,e2) defn (44) e = C[r] (7,42) (45) assume e = C'[r'] hypo (46) C' = Plus(C1', e2) (7,45) defn context (47) e1 = C1'[r'] (45,46) defn C[r] (48) C1' = C1, r' = r (42) uniqueness (49) C' = C, r' = r (43,48) (50) e = C'[r'] => C' = C & r' = r (45,49) => Intro (51) ∃!C,r. e = C[r] (44,50) (52) P(e) QED[41] (53) P(e) (54) [Ind] Case: e = Times(e1,e2) case hypo (55) P(e) (similar 7) QED 23 (56) ∀e. P(e) (3,7,54) IP, QED[0] Notes: (14) "defn C[r]" refers to the definition of the wrapping function _[_] that recombines a context and redex into the original expression. (56) IP is the Induction Principle for induction over structure of SAE expressions.