Learn · The Concrete Discrete Math of Real Systems

seedling

The Loop That Proves Forever

Mathematical induction is the loop invariant you already trust, recursion is the same proof walking downward, and a data type's constructors quietly write its proof plan for you.

discrete-math, proof, induction, recursion, loop-invariants, learn

Induction plays a central role in discrete mathematics and computer science.

— Eric Lehman, F. Thomson Leighton, and Albert R. Meyer, Mathematics for Computer Science, 2015

Chapter 3 showed why testing cannot grant “always.” This chapter grants it. You will recognize induction as the same three-part argument as a loop invariant, prove the sum $1+2+\cdots+n$ , use strong induction when a step needs several earlier facts, and derive a structural proof from the constructors of a list or tree.

The loop you already believe

Consider a loop that sums the first $n$ positive integers. Just before iteration $k$ , the variable total should equal the sum of the numbers strictly before $k$ :

$\text{total}=1+2+\cdots+(k-1).$

That sentence is a loop invariant: true before the first iteration, preserved by one execution of the body, and useful when the loop ends.

Invariant — a property that remains true across every permitted step of a process. Learn more in the state-machine chapters of MIT's text.

Before the loop, $k=1$ and the sum before $k$ is empty, so total is

If the sentence is true before iteration $k$ , adding $k$ makes

total equal $1+\cdots+k$ , exactly the sentence needed before iteration $k+1$ . When $k=n+1$ , the invariant says total is $1+\cdots+n$ .

That proof has three moves:

establish the claim at the beginning;
show one valid step preserves it;
conclude it holds after any finite number of steps.

Those are not merely similar to mathematical induction. They are mathematical induction, with program state in place of an integer.

Note

Who named the method. Augustus De Morgan (1806–1871) introduced the term “mathematical induction” in an 1838 encyclopedia article, but the proof pattern is far older: related arguments appear in ancient and medieval mathematics, and Blaise Pascal used an explicit inductive step in the seventeenth century. Attribution here is to the modern name, not to a lone invention.

Commit to the load-bearing line.

The induction principle. If $P(0)$ is true, and for every nonnegative $k$ , $P(k)$ implies $P(k+1)$ , then $P(n)$ is true for every nonnegative integer $n$ .

The first obligation is the base case. The second is the inductive step. Inside that step, assuming $P(k)$ is the induction hypothesis. It is not assuming the theorem. It is proving that truth at one rung is enough to reach the next. The base case supplies the first rung.

For every nonnegative integer $n$ ,

$1+2+\cdots+n = \frac{n(n+1)}{2}.$

For $n=0$ , both sides are 0. Now assume the formula holds at $n=k$ : $1+\cdots+k=k(k+1)/2$ . Add the next term:

$1+\cdots+k+(k+1) = \frac{k(k+1)}{2}+(k+1) = \frac{(k+1)(k+2)}{2}.$

That is the claimed formula with $k+1$ in place of $k$ . The base case and inductive step therefore establish the formula for every nonnegative $n$ .

In plain English: the formula starts true, and adding the next integer turns one correct instance into the next. No integer can be the first failure, because its predecessor would force it to work.

Remove the base case and the argument can float forever without touching the ground. “If everyone in line receives a token, the next person does too” distributes no tokens by itself. Remove the step and you have one tested example. Use a step that proves $P(k)$ from $P(k)$ and you have a circle, not progress.

Strong induction is ordinary induction with a larger toolbox

Sometimes the next case needs more than its immediate predecessor. To prove every integer greater than 1 factors into primes, take an integer $n$ . If it is prime, stop. If composite, write $n=ab$ with $2\le a,b<n$ . The proof needs the claim for both smaller factors, not merely for $n-1$ .

Strong induction assumes all earlier cases while proving the next. It is not logically stronger than ordinary induction; it packages the history the step naturally consumes. A recursive function that calls itself on several smaller inputs asks for exactly this proof shape.

Well-founded — having no infinite descent. Recursion terminates when every call moves downward in a well-founded order. Learn more.

The data type writes the proof

A list is built in two ways: it is empty, or it is one item followed by a smaller list. Therefore a proof about every list has two obligations: prove it for the empty list; then prove that adding one item preserves it. That is structural induction.

Reversing a finite list twice returns the original list.

The reverse of the empty list is empty, so reversing twice returns it. Now assume reversing a smaller list $xs$ twice returns $xs$ . A nonempty list has the form $x:xs$ . Reversing moves $x$ to the end; reversing again moves it back to the front and, by the induction hypothesis, restores $xs$ . Therefore the whole list is restored.

In plain English: there are no secret third kinds of list. Once the proof covers empty and “one more item,” it covers every finite list the constructors can make.

For a binary tree, the constructors demand a leaf case and a node case whose hypothesis applies to both children. For an expression tree, each syntax constructor becomes a proof branch. The shape of the data is the shape of the recursion, the fold, and the proof.

This is the chapter's second click: induction is not tied to counting. It follows construction. Integers are merely the first recursively constructed objects most books show.

The honest limits

Induction proves a correctly stated predicate, including a useless one. A loop invariant that says total > 0= may be easy to preserve and too weak to establish the result. Strengthening the invariant is often the creative step.

Induction also needs progress in a well-founded direction. A recursive call on an input that is merely “different,” rather than provably smaller, supplies no termination argument. Finally, the proof covers the mathematical model; integer overflow, mutation, and I/O belong in that model if the implementation can exhibit them.

Lessons

Induction and a loop-invariant proof share one skeleton: initialize, preserve, conclude.
The induction hypothesis licenses one step; the base case anchors the chain.
Strong induction matches recursion that depends on several smaller cases.
Structural induction follows a value's constructors, so the data type supplies the proof cases.
Termination requires descent in a well-founded order, and correctness requires an invariant strong enough to imply the result.

Practice

Retrieval — what testing still cannot buy.

Discrimination — choose the proof shape.

Transfer — find the missing obligation.

The objects under the proof

Induction follows the way an object is constructed. That raises the next question: what exactly is the space of objects we are constructing? A settings screen multiplies choices; constraints remove regions; partitions declare which differences matter; bijections let us count a space without listing it.

The proof license is now earned. Next we use it on the first structure.

References

Lehman, Leighton & Meyer. “Mathematics for Computer Science.” MIT OpenCourseWare, 2015. — the epigraph, induction chapters, and the invariant principle in one open text
Floyd. “Assigning Meanings to Programs.” Proceedings of Symposia in Applied Mathematics, 1967. — the foundational program-verification treatment behind inductive assertions and invariants
Noether. “Idealtheorie in Ringbereichen.” Mathematische Annalen, 1921. — a primary historical source for ascending-chain reasoning; read much later, when well-founded arguments have become familiar

Chapter 4 of The Concrete Discrete Math of Real Systems — mathematical induction, strong and structural induction, loop invariants, recursive definitions, and proofs of programs.