Where we're goingBasics of Induction (Review)SyntaxInduction on SyntaxOperational SemanticsCIS 500Software FoundationsFall 2006September 18AdministriviaIHW3 is available now; due next Monday.IAcceptable submission formats:IPDF generated by LaTeX (preferred!)IPDF generated in some other way, e.g. Word (if you must)Iascii (as a last resort)Inot raw Word files or handwrittenIIf you foresee a lot of technical writing in your future, youshould consider learning how to use LaTeX now.IRecitations started last week.IReview recitations: Ask questions, see examples worked out.ReadingsAs mentioned before, you should try to at least look at the readingfor a particular lecture before that lecture.We’re starting with Chapter 3 of the textbook. Chapter 2 containssome mathematical preliminaries which we assume you are familiarwith.Where we’re goingGoing Meta...The functional programming style used in OCaml is based ontreating programs as data — i.e., on writing functions thatmanipulate other functions as their inputs and outputs.Everything in this course is based on treating programs asmathematical objects — i.e., we will be building mathematicaltheories whose basic objects of study are programs (and wholeprogramming languages).Jargon: We will be studying the metatheory of programminglanguages.Warning!The material in the next couple of lectures is more slippery than itmay first appear.“I believe it when I hear it” is not a sufficient test of understanding.A much better test is “I can explain it so that someone elsebelieves it.”“You never really misunderstand somethinguntil you try to teach it...”— Anon.Basics of Induction (Review)InductionPrinciple of ordinary induction on natural numbers:Suppose that P is a predicate on the natural numbers.Then:If P(0)and, for all i, P(i) implies P(i + 1),then P(n) holds for all n.ExampleTheorem: 20+ 21+ ... + 2n= 2n+1− 1, for every n.Proof: Let P(i) be “20+ 21+ ... + 2i= 2i +1− 1.”IShow P(0):20= 1 = 21− 1IShow that P(i ) implies P(i + 1):20+ 21+ ... + 2i +1= (20+ 21+ ... + 2i) + 2i +1= (2i +1− 1) + 2i +1by IH= 2 · (2i +1) − 1= 2i +2− 1IThe result (P(n) for all n) follows by the principle of(ordinary) induction.Shorthand formTheorem: 20+ 21+ ... + 2n= 2n+1− 1, for every n.Proof: By induction on n .IBase case (n = 0):20= 1 = 21− 1IInductive case (n = i + 1):20+ 21+ ... + 2i +1= (20+ 21+ ... + 2i) + 2i +1= (2i +1− 1) + 2i +1IH= 2 · (2i +1) − 1= 2i +2− 1Complete InductionPrinciple of complete induction on natural numbers:Suppose that P is a predicate on the natural numbers.Then:If, for each natural number n,given P(i) for all i < nwe can show P(n),then P(n) holds for all n.Complete versus ordinary inductionOrdinary and complete induction are interderivable — assumingone, we can prove the other.Thus, the choice of which to use for a particular proof is purely aquestion of style.We’ll see some other (equivalent) styles as we go along.SyntaxSimple Arithmetic ExpressionsHere is a BNF grammar for a very simple language of arithmeticexpressions:t ::= termstrue constant truefalse constant falseif t then t else t conditional0 constant zerosucc t successorpred t predecess oriszero t zero testTerminology:It here is a metavariableAbstract vs. concrete syntaxQ: Does this grammar define a set of character strings, a set oftoken lists, or a set of abstract syntax trees?A: In a sense, all three. But we are primarily interested, here, inabstract syntax trees.For this reason, grammars like the one on the previous slide aresometimes called abstract grammars. An abstract grammar definesa set of abstract syntax trees and suggests a mapping fromcharacter strings to trees.We then write terms as linear character strings rather than treessimply for convenience. If there is any potential confusion aboutwhat tree is intended, we use parentheses to disambiguate.Abstract vs. concrete syntaxQ: Does this grammar define a set of character strings, a set oftoken lists, or a set of abstract syntax trees?A: In a sense, all three. But we are primarily interested, here, inabstract syntax trees.For this reason, grammars like the one on the previous slide aresometimes called abstract grammars. An abstract grammar definesa set of abstract syntax trees and suggests a mapping fromcharacter strings to trees.We then write terms as linear character strings rather than treessimply for convenience. If there is any potential confusion aboutwhat tree is intended, we use parentheses to disambiguate.Q: So, aresucc 0succ (0)(((succ (((((0))))))))“the same term”?What aboutsucc 0pred (succ (succ 0))?A more explicit form of the defini tionThe set T of terms is the smallest set such that1. {true, false, 0} ⊆ T ;2. if t1∈ T , then {succ t1, pred t1, iszero t1} ⊆ T ;3. if t1∈ T , t2∈ T , and t3∈ T , thenif t1then t2else t3∈ T .Inference rulesAn alternate notation for the same definition:true ∈ T false ∈ T 0 ∈ Tt1∈ Tsucc t1∈ Tt1∈ Tpred t1∈ Tt1∈ Tiszero t1∈ Tt1∈ T t2∈ T t3∈ Tif t1then t2else t3∈ TNote that “the smallest set closed under...” is implied (but oftennot stated explicitly).Terminology:Iaxiom vs. ruleIconcrete rule vs. rule schemeTerms, concretelyDefine an infinite sequence of sets, S0, S1, S2, . . . , as follows:S0= ∅Si +1= {true, false, 0}∪ {succ t1, pred t1, iszero t1| t1∈ Si}∪ {if t1then t2else t3| t1, t2, t3∈ Si}Now letS =[iSiComparing the definitionsWe have seen two different presentations of terms:1. as the smallest set that is closed under certain rules (T )Iexplicit inductive definitionIBNF shorthandIinference rule shorthand2. as the limit (S) of a series of sets (of larger and larger terms)What does it mean to assert that “these presentations areequivalent”?Comparing the definitionsWe have seen two different presentations of terms:1. as the smallest set that is closed under certain rules (T )Iexplicit inductive definitionIBNF shorthandIinference rule shorthand2. as the limit (S) of a series of sets (of larger and larger terms)What does it mean to assert that “these presentations areequivalent”?Induction on SyntaxWhy two definitions?The two ways of defining the set of terms are both useful:1. the definition of terms as the smallest set with a certainclosure property is compact and easy to read2. the definition of the set of terms as the limit of a sequencegives us an induction principle for proving things aboutterms...Induction on TermsDefinition: The depth of a term t is the