CIS 301: Lecture Notes on InductionTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversityApril 22, 2008These notes are written as a supplement to [1, Sect. 16.1&16.3], but can beread independently.1 Loop Invariants: Induction in DisguiseConsider 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, e ach time control reaches B, ψ holds.1Using the framework of CIS 301: Lecture Notes on Program Verification, available athttp://www.cis.ksu.edu/~tamtoft/CIS301/Spring08/verification.pdf, this amountsto (1) and (2) below being valid assertions.{ψ} (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 predicate3that 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”:kNat(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 canno t 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 cas e 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),3Alternatively, we could define Nat to hold only on 1, 2, 3, 4, . . . but not on 0. Our choicedo e s not matter much as long as we are consistent, unlike the formulation of Proposition 4in [1, p.454] which—even though 0 just earlier on the page has been declared the firstnatural numbe r—impl ici tly assumes that the first n natural numbers are 1, . . . , n.3and 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.2.1 Alternative formulationsSometimes, we need to use another starting point than zero, say m0:Q(m0) ∧ Nat(m0)...∀k((Nat(k) ∧ k ≥ m0∧ Q(k)) → Q(k + 1))...B∀k((Nat(k) ∧ k ≥ m0) → Q(k))Below is an application of this principle, with m0= 3.Theorem 2.2. For a k-polygon (k ≥ 3), the sum of its angles is given by(k − 2) · 180 degrees.Proof. (Informal.) For the basis step, we must consider k = 3; the claim isthat the sum of the angles in a triangle is 180 degrees. But this is a factfrom elementary geometry.For the inductive step, consider a (k + 1)-polygon P . It is not hard to seethat P can be split into a triangle and a k-polygon; the sum of the angles inthe former is 180 degrees (cf. above), and the sum of the angles in the latteris (k −2) ·180 degrees (by the induction hypothesis). Therefore, the sum ofthe angles in P is 180 + (k − 2) · 180 = ((k + 1) − 2) · 180, as desired.A somewhat different perspective is offered by the following rule4:4For simplicity, we implicitly assume that all entities are natural numbers.4Principle 3 (Course-of-values induction). In order to prove that Q(k) holdsfor all natural numbers k, it suffices to show the following property for all k:given that Q holds for all numbers less than k, Q also holds for k. Expressedin Fitch notation:∀k(∀m(m < k → Q(m)) → Q(k))...B ∀kQ(k)To justify the validity of course-of-values induction, assume (in order toarrive at a contradiction) that the conclusion does not hold. That is, thereexists natural numbers not satisfying Q. Let k be the least such number.That is, for all m < k we have Q(m). But then our premise tells us that alsoQ(k), yielding the desired contradiction. (A variation of this proof, wherewe do a proof by cases depending on whether k = 0 or k > 0, can be usedto establish the validity of the original induction principle.)Note that to establish the premise required for course-of-values induction, aproof of the follow ing form is probably needed:k ∀m(m < k → Q(m))...Q(k)∀k(∀m(m < k → Q(m)) → Q(k))We now give an example that illustrates the usefulness of course-of-valuesinduction. We shall consider the Fibonacci numbers5given byfib(n) = case n of0 ⇒ 11 ⇒ 1m + 2 ⇒ fib(m + 1) + fib(m)Theorem 2.3. If n + 1 is divisible by 3, then fib(n) is an even number,otherwise fib(n) is an odd number.5See http://en.wikipedia.org/wiki/Fibonacci number (which uses a slightly differ-ent definiti on) for a survey of some properties of these.5Proof. We shall employ course-of-values induction. There is thus no basestep, but “only” the inductive step. Here we have to establish, for an arbi-trary n, with Q the property mentioned in the theorem, that if Q(m)