Correctness of Recursive Algorithms by Induction

A recursive algorithm solves a problem by reducing it to one or more smaller instances of the same problem, together with a base case that is solved directly without recursion. Correctness of such an algorithm cannot be verified by unrolling all possible executions, since the recursion tree can be arbitrarily deep or arbitrarily branching. Instead we use induction: we prove a statement `P(n)` — "the algorithm produces the correct output on any input of size `n`" — by establishing it for the smallest sizes (the base case of the proof, matching the base case of the algorithm) and then showing that if `P(k)` holds for all relevant smaller sizes `k < n`, then `P(n)` holds too. This is where the analogy to loop invariants becomes precise. A loop invariant is a statement that is true before the loop, preserved by every iteration, and yields correctness on exit. A recursive proof is a statement that is true on base cases, preserved by every recursive call (in the sense that correct subresults imply a correct combined result), and yields correctness for the top-level call. The loop invariant "walks forward" through iterations; the recursive invariant "walks backward" through shrinking subproblems, terminating at the base case. Both are instances of the same inductive principle, just applied to different control structures. Three flavors of induction appear in practice, and choosing the right one is often the whole difficulty of the proof:

• Simple induction on an integer parameter — used when each call reduces a single integer measure by exactly 1 (e.g., recursion on `n` and `n − 1`), such as computing a factorial or a Fibonacci number by naive recursion.
• Strong induction — used when a call may reduce the measure by more than 1, or depends on multiple prior cases (e.g., `T(n)` calls itself on `n/2` for merge sort, or on `n−1` and `n−2` for Fibonacci). Here the inductive hypothesis must be "`P(k)` holds for all `k < n`," not just "`P(n−1)` holds."
• Structural induction — used when the input is not a single number but a recursively defined structure: a list (empty list, or head plus smaller list), a binary tree (leaf, or root plus two smaller subtrees), or a recursive grammar. The induction is on the size or depth of the structure, and the base case matches the structure's own base case (empty list, leaf node).

In every flavor, the crucial discipline is: the inductive step is allowed to assume the algorithm behaves correctly on strictly smaller inputs — this assumption is the induction hypothesis, not something to be reproven — and must show only that the current level's combination of subresults is correct, using recursion depth or structure size as the measure that must strictly decrease toward the base case.

The general recipe for proving a recursive algorithm correct has five components, mirrored directly in the pseudocode below for a canonical example: recursive merge sort. 1. Identify the recursive structure. State precisely what shrinks on each call and by how much (the measure), and confirm the measure is a nonnegative integer that strictly decreases — this guarantees termination and gives a well-founded induction. 2. State the specification `P(n)`. Precisely describe what "correct" means for input size `n` (e.g., "returns a sorted permutation of the input array"). 3. Prove the base case(s). Show directly, without recursion, that `P(n)` holds for the smallest size(s) the algorithm handles without calling itself. 4. State and use the inductive hypothesis (IH). Assume `P(k)` holds for all sizes `k` strictly smaller than `n` that the algorithm might recurse on. 5. Prove the inductive step. Using the IH on the recursive call(s), show that the way the algorithm combines the subresults yields a correct result for size `n`. ``` Algorithm MERGESORT(A, lo, hi) // Sorts A[lo..hi] in place (inclusive bounds). if lo >= hi then return // Base case: 0 or 1 elements, already sorted mid = floor((lo + hi) / 2) MERGESORT(A, lo, mid) // Recursive call 1: sorts left half MERGESORT(A, mid+1, hi) // Recursive call 2: sorts right half MERGE(A, lo, mid, hi) // Combine: linear-time merge of two sorted halves return Algorithm MERGE(A, lo, mid, hi) // Precondition: A[lo..mid] and A[mid+1..hi] are each individually sorted. // Postcondition: A[lo..hi] is sorted, and is a permutation of its original elements. L = copy of A[lo..mid] R = copy of A[mid+1..hi] i = 0; j = 0; k = lo while i < length(L) and j < length(R) do if L[i] <= R[j] then A[k] = L[i]; i = i + 1 else A[k] = R[j]; j = j + 1 k = k + 1 while i < length(L) do A[k] = L[i]; i = i + 1; k = k + 1 while j < length(R) do A[k] = R[j]; j = j + 1; k = k + 1 ``` The proof of `MERGESORT` proceeds exactly along the five steps above.

Measure. Let `n = hi − lo + 1` be the number of elements in the subarray. Both recursive calls operate on strictly smaller subarrays (sizes `⌈n/2⌉` and `⌊n/2⌋`, each less than `n` whenever `n ≥ 2`), so the measure strictly decreases and eventually reaches 0 or 1, where the base case fires. This establishes termination.

Specification `P(n)`. For every subarray of length `n`, `MERGESORT` rearranges it into sorted order using exactly the original elements (a permutation).

Base case. If `lo ≥ hi`, the subarray has at most one element, and a single element (or an empty range) is trivially sorted; the algorithm returns without modifying anything, which is correct.

Inductive hypothesis. Assume `P(k)` holds for every `k < n` — every call to `MERGESORT` on a subarray of length strictly less than `n` correctly sorts that subarray.

Inductive step. For a subarray of length `n ≥ 2`, `MERGESORT` calls itself on the left half (length `< n`, by IH now correctly sorted) and the right half (length `< n`, by IH now correctly sorted). We must show `MERGE` combines two sorted subarrays into one sorted array containing exactly the same elements. This is argued separately by an ordinary loop-invariant proof on `MERGE`'s three `while` loops (the invariant: at the top of each iteration, `A[lo..k−1]` holds the `k − lo` smallest elements of `L ∪ R` seen so far, in sorted order) — precisely the technique from Loop Invariants and Correctness Proofs used here as the "combine" lemma inside a recursive proof. Given that lemma, `MERGE` produces a fully sorted `A[lo..hi]`, so `P(n)` holds. By induction, `P(n)` holds for all `n ≥ 0`. ∎ This example illustrates the general pattern precisely: recursive correctness proofs almost always compose with loop-invariant proofs, because the "combine" step inside a recursive call is frequently iterative.

Correctness argument, generalized. The proof pattern above is an instance of strong induction on a well-founded measure `μ`, where `μ(input)` is a nonnegative integer (here, subarray length) such that every recursive call is made on an input with strictly smaller `μ`. The general theorem is: > If (1) `μ` is a nonnegative integer for every valid input, (2) the algorithm is correct on every input with `μ = 0` (or the smallest handled value), and (3) for every input with `μ = n > 0`, correctness of the algorithm on all inputs with `μ < n` implies correctness on the input with `μ = n`, then the algorithm is correct on every valid input. This is the strong induction principle applied to the well-ordering of the natural numbers: since `μ` cannot decrease forever, every input eventually reduces, through a finite chain of recursive calls, to a base case. Because the natural numbers are well-ordered (every nonempty subset has a least element), there is no infinite descending chain, so the recursion is guaranteed to terminate — this is exactly what rules out infinite loops in a correctly structured recursive proof. Structural induction is the same theorem with `μ` chosen to be the size of a recursively defined structure rather than an arbitrary integer — number of nodes in a tree, length of a list, number of internal grammar productions — and the base case matches the structure's own atomic case (empty list `nil`, leaf node, terminal symbol). Because these structures are themselves defined inductively (a tree is either a leaf or a root with subtrees), structural induction is in fact the natural proof method: the shape of the proof mirrors the shape of the data definition exactly.

Why strong (not simple) induction is usually required. Simple induction only licenses assuming `P(n−1)`. Merge sort's recursive calls are on `⌈n/2⌉` and `⌊n/2⌋`, neither of which is `n − 1` in general — so a proof using only "assume `P(n−1)`" is invalid; we must assume `P(k)` for all `k < n`. This is precisely why algorithms like merge sort, quicksort, binary search, and tree recursion require strong induction, while simple recursions like naive factorial only need simple induction (each call is exactly `n − 1`).

Complexity is a byproduct of the same decomposition. The identical recursive breakdown used for the correctness proof — "the problem of size `n` reduces to two problems of size `n/2` plus `O(n)` combining work" — is exactly the recurrence ``` T(n) = 2 T(n/2) + O(n), T(1) = O(1) ``` which the Setting Up Recurrence Relations treatment solves (via recursion trees or the Master Theorem) to `T(n) = O(n log n)`. This is not a coincidence: the recursive structure that makes the proof tractable is the same structure that makes the runtime analysis tractable, because both are reading off the same self-reduction.

Honest tradeoffs. Structural/inductive proofs establish partial correctness conditional on termination separately from termination itself — both must be argued, and it is a common error to prove one and assume the other. Also, an inductive correctness proof says nothing about numerical stability, memory usage, or performance under adversarial inputs (e.g., quicksort's worst case); those require separate analysis. Finally, induction proves correctness of the algorithm as specified, not of any particular implementation — an off-by-one error in array indexing can violate the very invariant the proof assumed, so the proof and the code must be checked against each other line by line, not just at the level of the algorithm's idea.

Trace the correctness argument concretely for computing the `n`-th Fibonacci number recursively, a case where strong induction with two base cases is unavoidable because the recursive call depends on two previous values, not one. ``` Algorithm FIB(n) if n == 0 then return 0 // Base case 1 if n == 1 then return 1 // Base case 2 return FIB(n-1) + FIB(n-2) // Recursive step: depends on TWO smaller cases ```

Specification. `P(n)`: "`FIB(n)` returns the `n`-th Fibonacci number," where `F(0)=0`, `F(1)=1`, `F(k)=F(k−1)+F(k−2)` for `k ≥ 2`.

Base cases. `FIB(0)` returns `0 = F(0)` directly; `FIB(1)` returns `1 = F(1)` directly. Both match the definition without recursion — `P(0)` and `P(1)` hold.

Inductive hypothesis (strong form). Assume for some `n ≥ 2` that `P(k)` holds for every `k` with `0 ≤ k < n`. In particular `P(n−1)` and `P(n−2)` both hold — this is why strong induction is required: simple induction (assume only `P(n−1)`) is not strong enough to also license using `P(n−2)`.

Inductive step. `FIB(n)` computes `FIB(n−1) + FIB(n−2)`. Since `n − 1 < n` and `n − 2 < n`, the IH applies to both: `FIB(n−1)` returns `F(n−1)` and `FIB(n−2)` returns `F(n−2)`. So the sum returned is `F(n−1) + F(n−2) = F(n)` by the mathematical definition of Fibonacci numbers. Thus `P(n)` holds. By strong induction, `P(n)` holds for all `n ≥ 0`. ∎ (Note this proof says nothing about efficiency — `FIB` as written recomputes overlapping subproblems exponentially many times, a fact revealed only by the recurrence `T(n) = T(n−1) + T(n−2) + O(1)`, whose solution is `Θ(φⁿ)`, foreshadowing why memoization matters.) Now trace the values, not just the proof, to see the induction in action for `n = 5`:

Each row's "computed" value becomes an available fact — via the induction hypothesis — for every later row that calls it, exactly mirroring how the inductive step is stated abstractly above: correctness at each level is assumed available, not rediscovered.

The formal marriage of recursion and induction traces to the foundations of computability and recursive function theory in the early twentieth century, later crystallized into a practical engineering discipline for verifying programs.

Every production sorting library that uses divide-and-conquer (Timsort's merge phases, introsort's quicksort core) relies on exactly this style of proof to guarantee output is a correctly sorted permutation, not merely "usually sorted." Compiler front ends use recursive-descent parsers whose correctness — that they accept exactly the strings generated by a grammar — is proved by structural induction on the grammar's production rules. Database engines that maintain balanced trees (B-trees, red-black trees) prove that recursive insertion and rebalancing routines preserve tree invariants (sortedness, balance) via induction on tree height or node count. File-system and compression tools that recursively walk directory trees or parse nested data formats (JSON, XML) rely on structural induction over the recursive grammar of the format to argue the parser handles arbitrarily deep nesting correctly. Formal verification tools (Coq, Isabelle/HOL, Dafny) mechanize exactly this reasoning, requiring programmers to supply the measure and the inductive step explicitly before a recursive function is accepted as verified, turning the informal proof sketch taught here into machine-checked certainty.

Ask the tutor: Can you show me how strong induction handles a recursive algorithm with three or more recursive calls, like a ternary search or a recursive matrix-multiplication scheme?