15-312 Foundations of Programming LanguagesRecitation 2: Rule InductionDaniel Spoonhowerspoons+@csSeptember 3, 20031 Matching ParenthesesRecall from lecture our original definition (through inference rules) of the lan-guage of matching parentheses.ε MM1s1M s2Ms1s2MM2s M(s) MM3Recall also our “parser” for this language, given in terms in the following judg-ment and inference rules.0 B εB1k + 1 B sk B (sB2k − 1 B sk B )sB3(k > 1)We would like to show that the languages defined by M and B are one and thesame, and we began in lecture with a proof of the following: if s M then 0 B s.We will continue today be showing inclusion in the opposite direction. Inparticular, thatTheorem 1. If 0 B s then s M .Proof. By rule induction on the derivation of 0 B s. We consider each case inturn.(Rule B1) Then s = ε.s M By M1(Rule B2) Then s = (s0.k + 1 B s0Subderivation?1What’s gone wrong? Normally, this is the point of the proof where we’dcleverly apply the induction hypothesis – why can we not do so in this case?What, according to a recent lecture, are our alternatives if we find ourselvesstuck in such a situation?The first answer here is to generalize the induction hypothesis. To claim theequivalence of the languages M and B, our theorem is strong enough, but it isnot strong enough for us to carry out our proof. Let’s try it again.Theorem 1 (Revised). If k B s then ( · · · (| {z }ks M .Proof. By rule induction on the derivation of k B s. We consider each case inturn.(Rule B1) (as above)(Rule B2) Then s = (s0.k + 1 B s0Subderivation( · · · (| {z }k+1s0M By i.h.( · · · (| {z }ks M Since s = (s0.(Rule B3) Then s = )s0and k > 1.k − 1 B s0Subderivation( · · · (| {z }k−1s0M By i.h.() M By M1, M3( · · · (| {z }k−1()s0M By ???We’re so close this time! We’d like to conclude ( · · · (| {z }k−1()s0M (equivalently( · · · (| {z }k)s0M ) , but we’re not quite there yet. Intuitively, this should work out:we should be able to add a pair of (balanced) parentheses anywhere within astring of whose parentheses are already matched. (Are you convinced? Trysome examples.) We’ll use another strategy from lecture: we’ll prove a lemma!To keep the syntax under control, I’ll use l, r, and c instead of just s to standfor strings of parentheses.Lemma 2. If l r M and c M then l c r M .(Before you read on, think about how we will go about proving this? Byinduction? Over what?)2Proof. By rule induction on the derivation of l r M . We consider each case inturn.(Rule M1) Then l r = ε.c M By assumptionl c r M Since l = r = ε(Rule M2)One might think that the derivation of l r M looks something like this:...l M...r Ml r MWhy is this not the case? Just because we have chosen to break our stringinto two parts l and r doesn’t mean that they each have matching parentheses.(Think about where we’d like to use this lemma and about a statement of theform l B r. Must l (in particular) and r have matching parentheses?)To complete this case, we must consider a number of subcases, one for eachway that l r might be broken down into two strings of matching parentheses.First we take the case where l is split.(Rule M2, Subcase 1) Let l = l1l2....l1M...l2r Ml1l2r Ml2c r M By i.h.l1l2c r M By M2l c r M Since l = l1l2(Rule M2, Subcase 2) Let r = r1r2....l r1M...r2Ml r1r2M(as above)(What if the split really was between l and r? Do we need a separate case forthis?)3(Rule M3)Again, we must consider each of the ways that l r might be split in a derivationthat ends with...s M(s) M(Rule M3, Subcase 1) Let l = (l0and r = r0)....l0r0M(l0r0) Ml0r0M Subderivationl0c r0M By i.h.(l0c r0)M By M3l c r M Since l = (l0and r = r0)(Rule M3, Subcase 2) Let l = ε and r = (r0).l r M By assumptionr M Since l = εc r M By M2l c r M Since l = ε(Rule M3, Subcase 3) Let l = (l0) and r = ε. (as above)Given this lemma, we can now return to our main theorem. In fact, we nowhave all the right tools to complete the proof: the last case goes through easilyusing our new lemma.1.1 Alternatives to Rule Induction?We have focused this time on rule induction, but there are other properties ofstrings that we might reason about. In many cases, we might want to carry outsome proof by reasoning inductively over the lengths of strings. (Quick: thinkof a handful from 212!) Reconsider the case from our lemma where we split linto two pieces l1and l2. The end of the derivation looked something like this:...l1M...l2r Ml1l2r M4What if l1= l2= ε? Then l2r is not any shorter than l1l2r! If we were toreason about the lengths of the strings in this case, we could not apply theinduction hypothesis. Here (and in many proofs in this class) rule inductionwill prove to be the better