CMSC 221/321 Homework set 1 Solutions by Dave MacQueen and Lamont Samuels Homework 1.0 [15] ------------- 1.0.1 From Prop 1 from the Induction tutorial: A poset 〈A,≤〉is well founded iff it satisfies the DCC, which states there does not exist an infinite descending chain of elements of A. Consider the sequence S(n) = (a^n)b (n∈N), (range S = {b,ab,aab,aaab,…} ⊆ A*). Note that: s(0) < s(1) < s(2) < ... and in general s(i) < s(i - 1). Thus, S forms an infinite descending chain and therefore A* is not well founded since it contains a infinite descending chain S. 1.0.2 (Solution by Nick Seltzer) Let S(0) = S Let ai be any element of S(i). Let S(i+1) = Si/{ai}. S(i+1)is a proper subset of Si, so this is a descending chain. Also, at each stage, if S(i) is infinite then S(i+1) is also infinite, because removing a finite subset from an infinite set leaves an infinite set. So we can show by induction on i that S(i) is infinite for all i, and thus nonempty, so S(i+1) can always be defined, and the sequence is infinite. (This argument, if fully formalized, requires the "Axiom of Choice".) Therefore {S(i) | i ∈ Nat} is an infinite descending chain. Homework 1.1 [45] ------------ Prove that small-step (transition) evaluation for SAE always terminates. Hint: Think about the size of expressions. Each step of reduction strictly decreases the size of the expression, given the right definition of size. So define a size function size: expr → Nat Proof: Define the function size: SAE -> Nat that computes the number of binary operators in an exression as follows: size(Num(n)) = 0 size(Plus(e1,e2)) = 1 + size(e1) + size(e2) size(Times(e1,e2)) = 1 + size(e1) + size(e2) Lemma 1: For any transition e ↦ e', size(e) > size(e'). We'll first rephrase this in terms of derivations, where Der = the set of derivations for SAE[SS] as defined in Lecture 2: A derivation has a finite,concrete structure analagous to an expression. In fact, we can define an abstract grammar for derivations just as we do for expressions. For the SAE[SS] semantics, the grammar of derivations can be given by: n : Nat e : expr [SAE] d : Deriv d ::= R1(n1, n2) -- Rule 1 | R2(d, e) -- Rule 2 | R3(n, d) -- Rule 3 | R4(n1, n2) -- Rule 4 | R5(d, e) -- Rule 5 | R6(n1, d) -- Rule 6 Each derivation d ∈ Deriv has a conclusion, which is transition judgement e ↦ e'. We call e the "source", and e' the "target" of the transition. These can be computed from the concrete representation of the derivation as constructed by the derivation grammar above: G1: source(R1(n1,n2)) = Plus(Num(n1), Num(n2)) G2: source(R2(d,e)) = Plus(source(d),e) G3: source(R3(n,d)) = Plus(Num(n),source(d)) G4: source(R4(n1,n2)) = Times(Num(n1),Num(n2)) G5: source(R5(d,e)) = Times(source(d),e) G6: source(R6(n,d)) = Times(Num(n),source(d)) G7: target(R1(n1,n2)) = Num(n1+n2) G8: target(R2(d,e)) = Plus(target(d),e) G9: target(R3(n,d)) = Plus(Num(n),target(d)) G10: target(R4(n1,n2)) = Num(n1*n2) G11: target(R5(d,e)) = Times(target(d),e) G12: target(R6(n,d)) = Times(Num(n),target(d)) We can formulate inductive proofs over derivations based on the Inductive Principle given in Lecture 2. Here is our first example. We want to prove that when a transition is made, the size of the expression is reduced: Lemma 1: ∀e. ∀e'. e ↦ e' ⇒ size(e) > size(e') If we try to formalize an inductive proof of this Lemma, we run into a difficulty in deciding what we should do induction on. The statement involves two related expressions e and e'. We could try do this by structural induction on e, but then we have to figure out how to deal with e': the proposition is ∀e. P(e) where P(e) = ∀e'. e ↦ e' ⇒ size(e) > size(e') It's possible to prove this by induction on e, but it gets a bit messy. We can simplify things by rephrasing the Lemma as follows, where we have just one element to deal with, a transition derivation d. Lemma 1: ∀d ∈ Deriv. size(source(d)) > size(target(d)) Proof. By induction on the structrue of derivations. We will consider only derivations involving Plus expressions, since the cases for Times expressions are similar. (0) P(d) = size(source(d)) > size(target(d)). defn (1) ∀d ∈ Deriv. P(d) TBS (2) Case on structure of d (4) d = R1(n1,n2) case hyp (5) source(d) = Plus(n1,n2) defn source (G1) (6) target(d) = m (where m = n1+n2) defn target (G7) (7) size(source(d)) = size(Plus(n1,n2)) = 1 defn size (8) size(target(d)) = size(m) = 0 defn size (9) size(source(d)) > size(target(d) (7,8) QED 4 (10) d = R2(d',e) case hyp (11) size(source(d')) > size(target(d')) I.H. (12) source(d) = Plus(source(d'), e) defn source (G3) (13) target(d) = Plus(target(d'), e) defn target (G9) (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(d',n) case hyp (18) size(source(d')) > size(target(d')) I.H. (19) source(d) = Plus(Num n, source(d')) defn source (G4) (20) target(d) = Plus(Num n, target(d')) defn target (G10) (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 [analogous cases for R4, R5, R6 are omitted] (24) ∀d ∈ Der. P(d) (IP for Der) QED 1 The following is a "Progress" lemma, assuring us that we can find a transition for any compound expression. Lemma 2: ∀e. size(e) > 0 ⇒ ∃ e'. e ↦ e'. Proof: By induction on the structure of e. (0) P(e) = size(e) > 0 ⇒ ∃ e'. e ↦ e' defn (1) ∀e.P(e) TBS (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 = Plus(e1,e2) case defn (8) P(e1) I.H. (9) P(e2) I.H. (10) Cases on structure e1 (11) Case: e1 = Num(n1) case hyp (12) Cases on structure e2 (13) Case: e2 = Num(n2) case hyp (14) e = Plus(Num n1, Num n2) (11,13) (15) e ↦ Num(n1+n2) SAE[SS](1) (16) P(e) (15) QED[13] (17) Case: e2 = Plus(e3,34) case hyp (18) size(e2) > 0 defn size (19) ∃ e2'. e2 -> e2' (9) (20) e -> Plus(Num(n1), e2') SAE[SS](4) (21) P(e) (20) QED[17] (22) Case: e2 = Times(e3,34) case hyp (23) P(e) (similar 17) QED[22] (24) P(e) (16,21,23) QED[11] (25) Case: e1 = Plus(e11,e12) case hyp (26) size(e1) > 0 defn size (27) ∃ e1'. e1 -> e1' (8) (28) e -> Plus(e1', e2) SAE[SS](3) (29) P(e) (27) QED[24] (30) Case: e1 = Times(e11,e12) case hyp (31) P(e) (similar 24) QED[29] (32) P(e) (7,24,29,31) QED[7] (33) Case e = Times(e1,e2) case hyp (34) P(e) (similar 7) QED[32] (35) P(e) (2,6,32,34) QED[2] (36) ∀e.P(e) (34) ∀-intro ------ Now, with these two Lemmas, we are close to our goal. We want to show that Prop: ∀e. ∃n. e ↦* Num n Here is the informal proof "by induction on the size of e". Actually, it is by well founded induction (course of values induction) on the size of e. First a little reminder about ↦* (the transitive closure of the transition relation ↦). ↦* is defined inductively as follows: Defn: Inductively defined relation e ↦* e': (1) ∀ e. e ↦* e (2) ∀ e1, e2, e3. e1 ↦ e2 & e2 ↦* e3 ⇒ e1 ↦* e3 [This is essentially the same as the inductive definition using inference rules given in the Appendix of Lecture 2.] The thing to note is that in order to show that e1 ↦* e2 holds, we do not need to construct or exhibit any particular transition sequence from e1 to e2, we just need to find an e such that e1 ↦ e and e ↦* e2 and apply clause (2) [unless e1 = e2, in which case we use clause (1)]. Proof: (informal) Let P(e) = ∃n. e ↦* Num n. Let e be some expression: IH: ∀e'. size(e') < size(e) => P(e') There are two cases: If size(e) = 0, then e = Num(m) for some m, and so e ↦* e by the base rule (1) for the defn of ↦*, and so P(e). [Here we did not need the IH.] If size(e) > 0, then by Lemma 2, e ↦ e' for some e', and by Lemma 1, size(e') < size(e). Hence by IH, P(e'), i.e, e' ↦* Num n for some n. But then e ↦* Num n by the induction rule (2) in the defn of ↦*. QED --------------------- Here is a formal version of this same proof. We have to reformulate the Lemma as a statement about natural numbers. Lemma 3: ∀ n. P(n), where P(n) == ∀ e. size(e) = n => ∃ m. e ↦* Num(m) Proof: By well founded induction on n ∈ Nat. (0) P(n) = ∀ e. size(e) = n => ∃ m. e ↦* Num(m) defn (1) ∀ n. P(n) TBS (2) Let n ∈ Nat defn (3) ∀n'. n' < n => P(n') I.H. (4) Case on n = 0 (5) Case: true (n = 0) (6) Let e ∈ SAE defn* (7) size(e) = n = 0 hyp (8) ∃m. e = Num(m) defn size (9) e ↦* Num(m). ↦*(1) (9) ∃m. e ↦* Num(m) ∃-intro (10) size(e) = n => ∃m. e ↦* Num(m) (7), => intro (11) ∀e. size(e) = n => ∃m. e ↦* Num(m) ∀-intro (12) P(n) (0) QED[5] (13) Case: false (n > 0) case defn (14) Let e ∈ SAE defn (15) size(e) = n > 0 hyp (16) ∃e'. e ↦ e' Lemma 2 (17) size(e') < size(e) Lemma 1 (18) P(size(e')) (3,13) (19) size(e') = size(e') defn function (20) ∃m. e' ↦* Num(m) (11,12) (21) e ↦* Num(m) ↦*(2) (22) ∃m. e ↦* Num(m) ∃-intro (23) size(e) = n => ∃m. e ↦* Num(m) (15), => intro (24) ∀e. size(e) = n => ∃m. e ↦* Num(m) (14,23) ∀-intro (25) P(n) (0) QED[13] (26) P(n) (4,12,25) (5) ∀n. P(n) ∀-intro QED[1] Now, to finish the main proof: (0) P(e) = ∃m. e ↦* Num(m) defn (1) ∀e. P(e) TBS (2) Let e ∈ SAE defn (3) P(size(e)) Lemma 3 (4) size(e) = size(e) = reflexive (5) ∃ m. e ↦* Num(m) (2,3) (6) ∀e. ∃ m. e ↦* Num(m) (1), ∀-intro (7) ∀e. P(e) (0) QED[1] ---------------------------------------------------------------------- Homework 1.2 [30] ----------------- Prove that the transistion relation is deterministic: for any e ∈ expr, there exists at most one e' such that e ↦ e'. (Hint: Do induction on the derivation of the transition e ↦ e', with case analysis on the last rule used in the derivation. See the discussion of rule induction in the Induction Tutorial.) The formal statement of that ↦ is deterministic is: Prop: ∀ e.∀ e1.∀ e2. e ↦ e1 & e ↦ e2 => e1 = e2. As for Lemma 1 in Homework 1.1, we can restate the proposition for as a property of derivations instead of triples of expressions: Prop: ∀d ∈ Deriv.∀d' ∈ Deriv. source(d) = source(d') => target(d) = target(d'). Proof: We will consider only Plus expressions, since the same reasoning applies to Times expressions (0) P(d) = source(d') = source (d) => target(d') = target(d) defn (1) ∀d∈ Deriv.P(d) TBS (1.5) Cases on d (2) Case: d = R1(n1,n2) case hyp (3) source(d) = Plus(Num n1, Num n2) (G1) (4) target(d) = Num (n1+n2) (G7) (5) Let d' ∈ Deriv defn (6) source(d') = source(d) hyp (7) d' = R1(n1,n2) (6), G1 (8) target(d') = Num(n1 + n2) (G7) (9) target(d') = target(d) (4,8) (10) source(d') = source(d) => target(d') = target(d) (6,9) => intro (11) P(d) QED[2] (12) Case: d = R2(d1,e2) case hyp (13) Let e1 = source(d1) defn (14) Let e1' = target(d1) defn (15) source(d) = Plus(e1,e2) (13,G2) (16) target(d) = Plus(e1',e2) (9,G8) (17) P(d1) I.H. (18) Let d' ∈ Deriv defn (19) e1 compound (13), defn source (20) source(d') = source(d) = Plus(e1,e2) hyp (21) d' = R2(d2,e2) for some d2 (19,21) defn source (22) source(d') = Plus(source(d2),e2) (21,G2) (23) Plus(source(d2), e2) = Plus(e1,e2) (20,22) (24) source(d2) = e1 (cancel Plus) (25) source(d2) = source(d1) (13,24) (26) target(d2) = target(d1) (25,17) (27) target(d') = Plus(target(d2),e2) (21,G8) (28) target(d') = Plus(e1',e2) (26,14) (29) target(d') = target(d) (16,28) (29) source(d') = source(d) => target(d') = target(d) (20,29, => intro) QED (30) Case: 2 = R3(n1,d1) case hyp (31) Let e2 = source(d1) defn (32) Let e2' = target(d1) defn (33) source(d) = Plus(Num n1,e2) (21,G3) (34) target(d) = Plus(Num n1,e2') (22,G9) (35) P(d1) I.H. (36) Let d' ∈ Deriv defn (37) e2 compound (31) defn source (38) source(d') = source(d) = Plus(Num n1,e2) hyp (39) d' = R3(n1,d2) for some d2 (31,38) defn source (40) source(d') = Plus(Num n1, source(d2)) (39,G3) (41) Plus(Num n1, source(d2)) = Plus(Num n1,e2) (38,40) (42) source(d2) = e2 (cancel Plus) (43) source(d2) = source(d1) (31,42) (44) target(d2) = target(d1) (35,43) (45) target(d') = Plus(Num n1,target(d2)) (39,G9) (46) target(d') = Plus(Num n1,e2') (32,45) (47) target(d') = target(d) (34,46) (48) source(d') = source(d) => target(d') = target(d) (38,47, => intro) QED [analogous cases for R4, 45, 46 omitted] (49) P(d) (2,12,30) (50) ∀d. P(d) (49, ∀-intro) QED[1] Homework 1.3 [10] ------------ Write an SML program implementing the size function on SAE exprs that you defined for Homework 1.1. Test it on a small but representative sample of expressions. datatype expr = Num of int | Plus of expr * expr | Times of expr * expr (* size: expr -> int *) fun size (Num n) = 0 | size (Plus(e1,e2)) = 1 + size e1 + size e2 | size (Times(e1,e2)) = 1 + size e1 + size e2 Total: 100 points