CMSC 221/321 Homework Set 3 Solutions By Dave MacQueen and Lamont Samuels Reading: Lecture 5. 3.1: [25] Prove that SAEL[SSv] (small-step bind-by-value semantics for SAEL) always terminates. You should be able to do this by modifying your proof of termination for SAE[SS] in Homework 1.1. (You can just give the new parts of the proof that deal with the new language features, i.e. let expressions.) (Solution by Jacob Sachs) size(Num(n)) = 0 size(Var(v)) = 0 size(Bapp(bop,e1,e2)) = 1 + size(e1) + size(e2) size(Let(x, e1, e2)) = 1 + size(e1) + size(e2) Rule Constructors: The derivations using the SEAL[SSv] rules can be thought of as terms constructed using the following constructors, each representing the application of an inferrence rule. The set Der[↦] of derivations is given by the abstract grammar: d ::= R1(bop,n1,n2) (Rule (1)) | R2(bop,d,e) (Rule (2)) | R3(bop,n,d) (Rule (3)) | R2(x,d,e) (Rule (4)) | R2(x,n,e) (Rule (5)) G1: source(R1(bop,n1,n2)) = Bapp(bop, Num n1, Num n2) G2: source(R2(bop,d,e)) = Bapp(bop, source(d), e) G3: source(R3(bop,n,d)) = Bapp(bop, Num n, source(d)) G4: source(R4(x,d,e)) = Let(x, source(d), e) G5: source(R5(x,n,e)) = Let(x, Num n, e) G6: target(R1(bop,n1,n2)) = Num prim(bop,n1,n2) G7: target(R2(bop,d,e)) = Bapp(bop, target(d), e) G8: target(R3(bop,n,d)) = Bapp(bop, Num n, target(d)) G9: target(R4(x, d, e)) = Let(x, target(d), e) G10:target(R5(x, n, e)) = [Num n/x]e ------------------------------------------------------------- Lemma 1: ∀e. ∀e'. e ↦ e' ⇒ size(e) > size(e') We restate the lemma in terms of derivations. ∀d ∈ Der[↦]. size(source(d)) > size(target(d)) Proof. By induction on the structrue of derivations. (0) P(d) = size(source(d)) > size(target(d)). defn (1) ∀d ∈ Deriv. P(d) TBS (2) Cases on structure of d (4) d = R1(bop,n1,n2) case hyp (5) source(d) = Bapp(bop,n1,n2) defn source (G1) (6) target(d) = p (where p = prim(bop,n1,n2)) defn target (G6) (7) size(source(d)) = size(Bapp(bop,n1,n2)) = 1 defn size (8) size(target(d)) = size(p) = 0 defn size (9) size(source(d)) > size(target(d)) (7,8) QED 4 (10) d = R2(bop,d',e) case hyp (11) size(source(d')) > size(target(d')) I.H. (12) source(d) = Bapp(bop,source(d'), e) defn source (G2) (13) target(d) = Bapp(bop,target(d), e) defn target (G7) (14) size(source(d)) = 1 + size(source(d')) + size(e) defn size (15) size(target(d)) = 1 + size(target(d')) + size(e) defn size (16) size(source(d)) > size(target(d)) (11,14,15) QED 10 (17) d = R3(bop,n,d') case hyp (18) size(source(d')) > size(target(d')) I.H. (19) source(d) = Bapp(bop, Num n, source(d')) defn source (G3) (20) target(d) = Bapp(bop, Num n, target(d')) defn target (G8) (21) size(source(d)) = 1 + size(source(d')) defn size (22) size(target(d)) = 1 + size(target(d')) defn size (23) size(source(d)) > size(target(d)) (18,21,22) QED 17 (24) d = R4(x,d',e) case hyp (25) size(source(d')) > size(target(d')) I.H. (26) source(d) = Let(x, source(d'), e) defn source (G4) (27) target(d) = Let(x, target(d'), e) defn target (G9) (28) size(source(d)) = 1 + size(source(d')) + size(e) defn size (29) size(target(d)) = 1 + size(target(d')) + size(e) defn size (30) size(source(d)) > size(target(d)) (25,28,29) QED 24 (31) d = R5(x,n,e) case hyp (32) source(d) = Let(x, Num n, e) defn source (G5) (33) target(d) = [Num n/x]e defn target (G10) (34) size(source(d)) = size(Let(x,n,e)) = 1 + size(e) defn size (35) size(target(d)) = size([Num n/x]e) = size(e) defn size, defn subst (36) size(source(d)) > size(target(d)) (34,35) QED 31 (37) ∀d ∈ Der. P(d) (IP for Der) QED 1 ------------------------------------------------------------- Lemma 2: ∀e. e closed & size(e) > 0 ⇒ ∃ e'. e ↦ e'. e ::= Num(n) | Var(v) | Bapp(bop, e, e) | Let(v, e, e) Proof: By induction on the structure of e. (0) P(e) = e closed & size(e) > 0 ⇒ ∃ e'. e ↦ e' defn (1) ∀e.P(e) TBS (1.1) assume e closed hyp (2) Cases on structure of e (3) Case: e = Num(n) case hyp (4) size(e) = 0 defn size (5) not(size(e) > 0) defn > (6) P(e) vacuously QED 3 (7) Case: e = Var(v) case hyp (8) e not closed defn closed (9) impossible contradicts (1.1) (11) Case: e = Bapp(bop,e1,e2) case hyp (12) P(e1) I.H. (13) P(e2) I.H. (13.1) e1 closed (1.1) defn closed (13.2) e2 closed (1.1) defn closed (14) Cases on structure e1 (15) Case: e1 = Num(n1) case hyp (16) Cases on structure e2 (17) Case: e2 = Num(n2) case hyp (18) e = Bapp(bop, Num n1, Num n2) (15,17) (19) e ↦ prim(bop,n1,n2) SAEL[SSv](1) (20) P(e) (19) QED 17 (21) Case: e2 = Bapp(bop, e3, e4) case hyp (22) size(e2) > 0 defn size (23) ∃ e2'. e2 ↦ e2' (IH 13,13.2,22) (24) e ↦ Bapp(bop,n1,e2') SAEL[SSv](3) (25) P(e) (24) QED 21 (26) Case: e2 = Let(v, e5, e6) case hyp (27) size(e2) > 0 defn size (28) ∃ e2'. e2 ↦ e2' (IH 13,13.2,27) (29) e ↦ Bapp(bop,n1,e2') SAEL[SSv](3) (30) P(e) (29) QED 26 (31) P(e) (20,25,30) QED 15 (32) Case: e1 = Bapp(bop,e11,e12) case hyp (33) size(e1) > 0 defn size (34) ∃ e1'. e1 -> e1' (IH 12,13.1,33) (35) e ↦ Bapp(bop,e1',e2) SAEL[SSv](2) (36) P(e) (35) QED 32 (37) Case: e1 = Let(v,e11,e12) case hyp (38) size(e1) > 0 defn size (39) ∃ e1'. e1 -> e1' (IH 12,13.1,38) (40) e ↦ Bapp(bop,e1',e2) SAEL[SSv](2) (41) P(e) (40) QED 37 (42) P(e) (31,36,41) QED 11 (43) Case: e = Let(v, e1, e2) case hyp (44) P(e1) I.H. (46) Cases on structure e1 (47) Case: e1 = Num(n1) case hyp (48) e = Let(v, n1, e2) (43,47) (49) e ↦ [n1/v]e2 SAEL[SSv](5) (50) P(e) (49) QED 47 (51) Case: e1 = Bapp(bop,e3,e4) case hyp (52) size(e1) > 0 defn size (53) ∃ e1'. e1 -> e1' (IH 44) (54) e ↦ Let(v,e1',e2) SAEL[SSv](4) (55) P(e) (54) QED 51 (56) Case: e1 = Let(v,e11,e12) case hyp (57) size(e1) > 0 defn size (58) ∃ e1'. e1 -> e1' (IH 44) (59) e ↦ Let(v,e1',e2) SAEL[SSv](4) (60) P(e) (59) QED 56 (61) P(e) (50,55,60) QED 43 (62) P(e) (6,10,42,61) QED 2 (63) ∀e.P(e) (61) ∀-intro The proof of Lemma 3 and the solution to the main proof remains the same. 3.2: [25] Write an SML program that implements SAEL[BSn] (that is, a big-step evaluator for SAEL with subst-by-name semantics). See file: hw_3_2.sml