Unformatted text preview:

CIS 301: Lecture Notes on InductionTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversityApril 29, 2004These notes are written as a supplement to [1, Sect. 16.1&16.3], but can beread independently.1 Demystifying InductionConsider a loop of the form while B do C od, and assume that we know1ψ is established by the preamble of the loop (1)if with B true, ψ holds prior to C, then ψ also holds after C (2)Then we can infer thatψ is an invariant of the loop. (3)That is, each time control reaches B, ψ holds.1Using the framework of CIS 301: Lecture Notes on Program Verification (Part I),available at http://www.cis.ksu.edu/~tamtoft/CIS301/Spring04/verificationI.pdf,this amounts to (1) and (2) below being valid annotations.{ψ} (1)while B do{ψ ∧ B} WhileTrueC{ψ} (2)od1Now observe that2• (1) amounts to saying that ψ holds after 0 iterations;• (2) amounts to saying that if ψ holds after k iterations, then after k+1iterations ψ also holds;• (3) amounts to saying that after any number (≥ 0) of loop iterations,ψ holds.We thus have the followingPrinciple 1 (Induction on Iterations). Assume that for a given loop,• ψ holds after 0 iterations; and• if ψ holds after k iterations then, after k + 1 iterations, ψ also holds.Then, for all k ≥ 0, after k iterations, ψ will hold.2 Induction on Natural NumbersPrinciple 1 carries over to a general principle:Principle 2 (Induction on Natural Numbers). Assume Q is such that• Q(0) holds; and• for all natural numbers k, if Q(k) holds then also Q(k + 1) holds.Then, for all natural numbers k, Q(k) holds.This is the rule mentioned in [1, p. 454]; in Fitch format, it can be writtenQ(0)...∀k((Nat(k) ∧ Q(k)) → Q(k + 1))...B∀k(Nat(k) → Q(k))2When we say that ψ holds after k iterations, we mean that if the loop iterates at leastk times then ψ holds after the k’th iteration. If control exits from the loop earlier, or ifone of the first k iterations gives rise to infinite computation (due to a subloop), then itis vacuously true that “ψ holds after k iterations”.2Here Nat is a predicate that is true on exactly the numbers 0, 1, 2, 3, 4, . . ..It is instructive to note that a sentence ∀k(Nat(k) → Q(k)) might also beprovable using a “General Conditional Proof”:k Nat(k)...Q(k)B ∀k(Nat(k) → Q(k))But such an approach is less likely to succeed, since when proving Q(k)for an arbitrary k, we now cannot assume Q(k − 1). On the other hand, ageneral conditional proof may be the only way to establish ∀k(P (k) → Q(k))in the case where the objects satisfying P do not have any “structure”.Example 2.1 ([1, p. 454]). We want to prove that for all natural numbersn we have1 + · · · + n =n(n+1)2With LHS and RHS given byLHS(n) = 1 + · · · + nRHS(n) =n(n + 1)2the claim is that for all natural numbers n we have Q(n) where Q(n) is givenby LHS(n) = RHS(n). We prove that by induction:Basis step. We must establish Q(0), that is LHS(0) = RHS(0). SinceLHS(0) = 0 (as the sum of zero numbers is 0), this follows since RHS(0) =0·12= 0.Inductive step. We can assume that Q(n) holds, that is LHS(n) = RHS(n),and must prove that Q(n + 1) holds. But this follows sinceLHS(n + 1) = (1 + · · · + n) + (n + 1) = LHS(n) + (n + 1)= RHS(n) + (n + 1) =n(n + 1)2+ (n + 1)=n(n + 1) + 2(n + 1)2=(n + 1)(n + 2)2= RHS(n + 1)where the third equality follows from the induction hypothesis.32.1 Alternative formulationsWe could choose another starting point:Q(1)...∀k((Nat(k) ∧ Q(k)) → Q(k + 1))...B∀k(Nat(k) → Q(k))assuming that Nat does hold only on 1, 2, 3, 4, . . . but not on 0. But it isimportant to be consistent, unlike the formulation of Proposition 4 in [1,p.454] which—even though 0 just earlier on the page has been declared thefirst natural number—implicitly assumes that the first n natural numbersare 1, . . . , n.A somewhat different perspective is offered by the following rule3, calledcourse-of-values induction:∀k(∀m(m < k → Q(m)) → Q(k))...B∀kQ(k)To justify the validity of this rule, assume (in order to arrive at a contra-diction) that the conclusion does not hold. That is, there exists naturalnumbers not satisfying Q. Let k be the least such number. That is, for allm < k we have Q(m). But then our premise tells us that also Q(k), yieldingthe desired contradiction. (A variation of this proof, where we do a proofby cases depending on whether k = 0 or k > 0, can be used to establish thevalidity of the original induction principle.)Note that to establish the premise needed for course-of-values induction, aproof of the following form is probably needed:k ∀m(m < k → Q(m))...Q(k)∀k(∀m(m < k → Q(m)) → Q(k))3For simplicity, we implicitly assume that all entities are natural numbers.4We now give an example that illustrates the usefulness of course-of-valuesinduction. Consider the Fibonacci numbers given byfib(0) = 1fib(1) = 1fib(n) = fib(n − 1) + fib(n − 2) for n ≥ 2Theorem 2.2. If n + 1 is divisible by 3, then fib(n) is an even number,otherwise fib(n) is an odd number.Proof. We shall employ course-of-values induction; there is thus no basestep but “only” the inductive step where we have to establish that for anarbitrary n, if (with Q the property mentioned in the theorem) Q(m) holdsfor all m < n then also Q(n) holds. We have to do a case analysis.Case 1: n = 0 or n = 1. Then n + 1 is not divisible by 3, and accordinglyfib(n) = 1 which is odd.Case 2: n + 1 is divisible by 3. Then neither (n − 1) + 1 nor (n − 2) + 1 isdivisible by 3. Our induction hypothesis thus tells us that fib(n − 1) andfib(n − 2) are both odd. As fib(n) = fib(n − 1) + fib(n − 2), this implies thatfib(n) is even, as desired.Case 3: n > 2 and n + 1 is not divisible by 3. Then exactly one of (n−1)+1and (n − 2) + 1 is divisible by 3. Our induction hypothesis then tells us thatexactly one of fib(n − 1) and fib(n − 2) is even. As fib(n) = fib(n − 1) +fib(n − 2), this implies that fib(n) is odd, as desired.Note that the last two steps could not have been carried out using theoriginal principle of induction (Principle 2), where we in order to establishQ(n) can assume only Q(n − 1) but not Q(n − 2).3 Induction on ListsLists, a very important data structure, are inductively defined as follows:base clause: List(nil) holds;inductive clause: if List(x) and v is a value then also List(vc x).5That is, a list is either empty (nil), or a value v in front of a list; here valuescould be


View Full Document

K-State CIS 301 - Lecture Notes

Download Lecture Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?