Proving Programs Right — Invariants, Induction & Termination

proof by mathematical induction

Picture an infinite line of dominoes. You want to argue they will all fall. You do not push each one — there are infinitely many. Instead you show two things: the first domino falls, and each domino, if it falls, knocks over the next. Together these guarantee every domino falls, all the way down the line. Mathematical induction is this exact move turned into a proof technique for statements that hold for every natural number n: prove it for the smallest n, and prove that truth at n forces truth at n+1.

Formally, to prove 'P(n) holds for all n >= n0', you prove the base case P(n0), then the inductive step 'for all n >= n0, if P(n) then P(n+1)'. The assumption 'P(n)' inside the step is the induction hypothesis. Once both are done, P holds for n0, hence n0+1, hence n0+2, and so on for every n — captured in one finite argument. A tiny example: to show 1 + 2 + ... + n = n(n+1)/2, the base case n=1 gives 1 = 1*2/2; the step assumes the formula at n and adds (n+1): n(n+1)/2 + (n+1) = (n+1)(n+2)/2, the formula at n+1. Done for all n.

Induction is the engine under most correctness and running-time proofs in algorithms: loop invariants are induction over iterations, recursion correctness is induction over input size, and recurrences like T(n) = 2T(n/2) + n are solved by guessing a bound and verifying it by induction. The honest caveat: induction proves a statement is true, but gives no intuition for why or how to discover the right statement — and a single gap (a missing base case, or a step that secretly needs a smaller case you did not assume) silently invalidates the whole thing.

Claim: a binary tree of height h has at most 2^(h+1) - 1 nodes. Base h=0: a single node, and 2^1 - 1 = 1. Step: a height-(h+1) tree is a root plus two subtrees of height <= h, so at most 1 + 2(2^(h+1) - 1) = 2^(h+2) - 1 nodes. True for all h.

Base case + inductive step = truth for every n, in one finite argument.

Never skip the base case: a valid inductive step with no true base proves nothing (the dominoes never start falling). Equally, the step must actually use only the hypothesis it assumes.

Also called
inductionweak induction歸納法