Ordinary induction uses only the previous case: from P(k) you derive P(k + 1). Many problems, however, break down into smaller cases that are not necessarily "the previous one": a number factors into any two smaller numbers, a tree splits into subtrees of different sizes. For these cases there are more flexible variants of induction. And the same idea, applied to loops in a program, is called a loop invariant, the main tool for proving that an iterative algorithm does what it promises.
Strong induction
In strong (or complete) induction the inductive step may assume that the property holds for all values from n₀ up to k, not only for k:
- Base case: prove P(n₀) (sometimes several base cases are needed).
- Step: assuming P(n₀), P(n₀ + 1), …, P(k), prove P(k + 1).
Example: prime factorisation
Statement: every integer n ≥ 2 is either prime or a product of primes.
Base case: 2 is prime.
Step: consider k + 1 and assume the statement holds for every integer from 2 to k. If k + 1 is prime, we are done. Otherwise k + 1 = a · b with 2 ≤ a, b ≤ k. By the inductive hypothesis both a and b are products of primes, and so is their product.
Example: 4- and 5-cent stamps
Statement: any postage of n ≥ 12 cents can be made up with 4-cent and 5-cent stamps.
Base cases: 12 = 4 + 4 + 4; 13 = 4 + 4 + 5; 14 = 4 + 5 + 5; 15 = 5 + 5 + 5.
Step: for k + 1 ≥ 16, the value k + 1 − 4 = k − 3 is at least 12 and therefore, by hypothesis, can be made up. Adding one 4-cent stamp gives k + 1.
Four base cases are needed here, because the step "jumps back" by four.
Structural induction
Many objects in computing are defined recursively: lists, trees, expressions, logical formulas. Structural induction proves a property for all objects of such a type:
- prove the property for the basic objects (the empty list, a leaf);
- prove that if it holds for the components, it holds for the object built from them.
Example: in every binary tree where each internal node has exactly two children, the number of leaves exceeds the number of internal nodes by one. A single leaf has 1 leaf and 0 internal nodes. A tree built from a root with two subtrees, which by hypothesis have lᵢ = iᵢ + 1 leaves each, has l₁ + l₂ = i₁ + i₂ + 2 leaves and i₁ + i₂ + 1 internal nodes: the difference is still 1.
Loop invariants
A loop invariant is a property that holds before entering a loop and that every iteration preserves. It is proved like an induction on the number of iterations, in three parts:
- Initialisation: the invariant holds before the first iteration.
- Maintenance: if it holds at the start of an iteration, it also holds at the end.
- Conclusion: when the loop ends, the invariant combined with the exit condition implies the desired result.
On top of these comes a proof of termination, usually by finding a non-negative integer quantity that strictly decreases on every pass.
Example: the maximum of an array
def maximum(a):
m = a[0]
i = 1
while i < len(a):
if a[i] > m:
m = a[i]
i += 1
return m
Invariant: at the start of each iteration, m is the maximum of a[0], …, a[i − 1].
- Initialisation: with i = 1, m = a[0] is the maximum of a[0] alone.
- Maintenance: if m is the maximum of the first i elements, after comparing with a[i] it is the maximum of the first i + 1; then i increases by 1 and the invariant holds again.
- Conclusion: the loop ends with i = len(a), so m is the maximum of the whole array.
- Termination: the quantity len(a) − i decreases by 1 on every pass and cannot go below zero.
Example: fast exponentiation
def power(b, e):
r = 1
while e > 0:
if e % 2 == 1:
r = r * b
b = b * b
e = e // 2
return r
Call the initial values B and E. The invariant is r · bᵉ = Bᴱ. At the start r = 1 and the product equals Bᴱ. If e is even, b becomes b² and e is halved: b²⁽ᵉ/²⁾ = bᵉ, unchanged. If e is odd, r absorbs one factor b, then b² raised to (e − 1)/2 accounts for the rest. At the end e = 0, so r = Bᴱ. The number of iterations is proportional to the number of bits of E, which is why this algorithm underlies modular exponentiation in cryptography.
Why it is worth the effort
When a loop doesn't work, the defect is almost always an invariant that breaks at the edges: the first element, the last, the empty array. Writing it as an assertion costs little and prevents many errors.
In short
- Strong induction uses the hypothesis on all smaller values, not just the previous one.
- When the step jumps back several positions, several base cases are needed.
- Structural induction proves properties of recursively defined lists, trees and formulas.
- A loop invariant is proved through initialisation, maintenance and conclusion, plus termination.
- Bugs in loops are often invariants that break at the edges.