CS611 Lecture 05 Inductive Proofs 9/10/01Scribe: Hongzhou Liu and Misha Zatsman Lecturer: Andrew Myers1OverviewInduction is used to prove hard things:• equivalence of semantics• termination• determinism• equivalence of programs• equivalence of expressions (used in optimization)2 EquivalenceWinskel gives the following definition of equivalence of programs and commands:c1∼ c2: ∀σ, σ0c1,σ0⇓σ ⇐⇒ c2,σ0⇓σWe can also state the definition in small-step semantics:c1∼ c2: ∀σ, σ0c1,σ0→∗skip,σ⇐⇒c2,σ0→∗skip,σIf we only care about some of the output we can simply compare a projection of σ . Also we can restrictthe input to a subset: Σ⊂ Σ so that our rule only holds ∀σ, σ0∈ Σ.Equivalence of commands is a little trickier than equivalence of programs. If c1∼ c2then any programc that contains c1should be equivalent to the same program with c2in place of c1.We define a command context to be a program with a hole in it. We can give the context a command toinsert in the hole and we get a program. Here’s a sample command context:ifx<ythen (y:=x-y, []) else skipFormally stated, a command context is a function C :Com→ Com. We can define it using BNF:C ::= [] |C; c | c; C|if b then C else c | if b then c else C|while b do C∀C, C[c1] ∼C[c2] is called “term equivalence”. A term is an expression representing a computation. Adeclaration is an example of an expression not representing computation. In Imp all expressions are terms.3 Types of Induction3.1 Standard InductionP (1) ∀n ≥ 1 .P(n) ⇒ P (n +1)∀n ≥ 1 .P(n)13.2 Course-of-Value InductionP (1) ∀n ≥ 1 . (∀m ∈ [1..n] .P(m)) ⇒ P (n +1)∀n ≥ 1 .P(n)Note that course-of-value induction on P (n) is the same as performing standard induction on P(n) ≡∀m ∈[1..n] .P(m).3.3 Structural Induction(∀e≺ e.P(e)) ⇒ P (e)∀e.P(e),whereeis a subexpression of eNote that the base cases (axioms) of structural induction are included for free in this definition. Sinceaxioms have no premises, the induction hypothesis is vacuously true; thus, the induction hypothesis gives usno help in proving the property holds for the base cases.3.4 Well-founded Induction∀a.(∀a≺ a.P(a)) ⇒ P (a)∀a.P(a)Well-founded induction is a generalization of induction, and it is used to show a ∈ A ⇒ P (a). We need≺ to be a well-founded relation, meaning there are no infinite descending chains: ... ≺ a3≺ a2≺ a1.Thiscondition implies that ≺ is irreflexive and that there are no cycles in the ≺ relation. Note that the lack ofinfinite descending chains does not imply that A is finite.We can derive normal induction from well-founded induction by choosing A ≡ N, x ≺ y ≡ x +1=y andcourse-of-values induction by choosing A ≡ N, x ≺ y ≡ x<y3.5 Induction on DerivationSuppose that α represents any provable assertion and we would like to show that P (α)holdsforallsuchassertions. For each such α there must be a proof tree:...α1...α2...α3αWe define the well-founded relation ≺ on proof trees as:D1≺ D2⇐⇒ D1is contained in D2One example from the proof tree above would be if we call D the tree concluding α, D1the proof treeconcluding α1and D2the proof tree concluding α2. D1≺ D and D2≺ D,butD2≺ D1(in general). Weobtain the following rule from well-founded induction:∀α.(∀i ∈ 1..n . P (αi)) ⇒ P (α)∀α.P(α)We can use induction on derivations to prove determinism of IMP. Determinism is:∀σ, σ1,σ2c, σ⇓σ1∧c, σ⇓σ2⇒ σ1= σ2Let:α ≡c, σ⇓σ12P (α) ≡∀σ2c, σ⇓σ2⇒ σ1= σ2The only tricky part of determinism is proving while statements to be deterministic, since the conclusionis contained is structurally identical to one of its premises. Assuming we have proven everything else to bedeterministic (notably boolean expressions) the proof is rather simple when we use induction on derivations:b, σ⇓true c, σ⇓σ3while b do c, σ3⇓σ1while b do c, σ⇓σ1b, σ⇓true c, σ⇓σ4while b do c, σ4⇓σ2while b do c, σ⇓σ2σ3= σ4by the induction hypothesis, therefore the two while expressions in the premises are also equivalent.By the induction hypothesis (since they have smaller proof trees) the expression is deterministic and thereforethey evaluate to the same value, therefore σ1=
View Full Document
Unlocking...