Skip to main content

Recursive Correctness by Strong Induction

What This Concept Is​

A recursive algorithm is correct when:

  1. The base case returns the correct answer directly.
  2. The inductive step shows that, assuming every recursive call on a strictly smaller input returns the correct answer, the non-recursive work at the current call combines those answers into the correct result for the current input.

That is strong induction, phrased in code. Unlike ordinary induction (which assumes the hypothesis only at $n-1$), strong induction assumes the hypothesis for all sizes less than $n$. This matches reality: a recursive call may be on size $n-1$, $n/2$, $n/3$, or anything smaller, and a single proof shape covers all of them.

The skeleton of a recursive-correctness proof:

  • State the pre/postcondition precisely (what input is accepted; what output is claimed).
  • Choose an induction variable (input size, string length, number of nodes, depth, lexicographic order).
  • Prove the base case first by direct computation.
  • Prove the inductive step, citing the induction hypothesis on each recursive call and arguing the non-recursive work preserves the postcondition.

Pair this with a termination argument (concept 7): correctness is only meaningful for functions that halt.

Why It Matters Here​

Divide-and-conquer, tree recursion, and backtracking are only trustworthy when their correctness is proved by induction on input size. "I ran it on a few cases" is not a proof for a function whose behavior depends on recursive calls you did not trace. A working mergesort that you cannot explain inductively is a mergesort you cannot safely modify.

Strong induction is also the unifying skeleton for DP correctness (cluster 4): the recurrence is an induction schema and the proof that OPT(state) = combine(OPT(smaller states)) is the inductive step. A weak recursive-correctness instinct will reliably produce wrong DP transitions.

Concrete Example​

Example 1 (mergesort).

def merge_sort(A):
    if len(A) <= 1:
        return A
    mid = len(A) // 2
    left = merge_sort(A[:mid])
    right = merge_sort(A[mid:])
    return merge(left, right)

Claim. merge_sort(A) returns a sorted permutation of $A$.

Induction variable. $n = \text{len}(A)$.

Base case. $n \le 1$. A zero- or one-element list is already sorted, and the function returns it unchanged. Both "permutation" and "sorted" hold.

Inductive step. Assume the claim holds for every list strictly shorter than $A$. Since A[:mid] and A[mid:] have length $\lfloor n/2 \rfloor$ and $\lceil n/2 \rceil$, both $< n$, by IH left and right are sorted permutations of A[:mid] and A[mid:]. A separate lemma - merge returns a sorted permutation of the concatenation of two sorted inputs - completes the argument: the result is a sorted permutation of $A$. $\square$

The proof has two duties: rely on the inductive hypothesis for the recursive calls, and prove the non-recursive work (merge) does the right thing on its precondition. Forgetting the second duty is the most common failure.

Example 2 (binary exponentiation).

def power(x, n):
    if n == 0: return 1
    if n % 2 == 0:
        half = power(x, n // 2)
        return half * half
    return x * power(x, n - 1)

Claim. power(x, n) returns $x^n$ for $n \ge 0$.

Base case. $n = 0$ returns 1, which is $x^0$.

Inductive step. Assume the claim for all $m < n$. If $n$ is even, $n/2 < n$, so half = $x^{n/2}$ by IH; half * half = $x^n$. If $n$ is odd, $n - 1 < n$, so power(x, n - 1) = $x^{n-1}$ by IH; multiplying by $x$ yields $x^n$. $\square$

Note the proof uses the hypothesis at $n/2$ for even $n$ and at $n-1$ for odd $n$; strong induction is essential because ordinary "$n-1$ only" induction would not cover the even case without extra work.

Common Confusion / Misconceptions​

  • "The base case is obvious, skip it." The induction collapses without it. Even when the base case is "obviously trivial," write it down - skipping is how vacuously-correct proofs of wrong algorithms get published.
  • "Induction hypothesis at the same size." Using the IH on something that is not strictly smaller is exactly how non-terminating recursions get declared "correct." Always state why the recursive argument shrinks.
  • "Correctness covers termination." It does not. A function that recurses forever is vacuously correct under the inductive hypothesis; see concept 7 for the necessary termination argument.
  • "Strong induction is fancier, use it only when needed." Strong induction is the default for recursion. Ordinary induction works only when the recursive call is always at size $n - 1$.
  • "If it passes tests, the proof is unnecessary." Tests check the cases you chose. Induction checks the infinite family.
  • "Mutual recursion breaks induction." It doesn't; you induct on a joint measure (sum of sizes, lexicographic pair, tree depth). The hypothesis must cover all mutual callees at every smaller value of that measure.

How To Use It​

For any recursive algorithm:

  1. State the pre/postcondition in one line each.
  2. Identify the induction variable (size of input, depth of recursion, lexicographic rank).
  3. Verify the base case directly.
  4. Write the inductive hypothesis explicitly: "assume the function is correct for all sizes less than the current size."
  5. Describe what each recursive call returns under the IH.
  6. Prove the non-recursive work combines those returns into the correct output (this is often a separate lemma, like merge's correctness).
  7. Confirm termination separately (concept 7).
  8. When debugging, the proof's first broken step is usually the exact place where the bug lives.

Transfer / Where This Shows Up Later​

  • S1 M5 (problem solving) taught "reduce to a smaller instance." Strong induction is the verification framework for that reduction.
  • S4 (systems) uses induction to prove lock-free recursion (e.g., recursive mutex acquire/release), and it underlies correctness proofs for cache-oblivious recursive layouts.
  • S5 (OS) proves recursive directory operations and filesystem consistency by induction on directory depth.
  • S6 (databases) proves query optimizer transformations (selectivity pushdown, join reordering) by induction on the plan tree.
  • S7 (architecture) uses the same schema when verifying a refactor preserves behavior module-by-module: each module's new form is correct given its callees' new forms (induction on the dependency DAG).
  • S8 (distributed systems) proves replication / consensus protocols by induction on decided log entries.

Concept 12 (optimal substructure) is the optimization-flavored version: prove the recurrence is optimal, not just correct.

Within this semester: S2 M2 proves correctness of quicksort partition and of merge by induction on input length; S2 M3 proves Dijkstra's invariant ("settled set always contains correct distances") by induction on iteration count; S2 M4 uses induction on DP state rank for every transition proof.

Check Yourself​

  1. Why does recursive correctness almost always use strong induction, not ordinary induction?
  2. In mergesort, why do you need a separate lemma about merge?
  3. What part of the proof depends on the recursive calls being on strictly smaller inputs?
  4. For power(x, n) above, why does strong induction buy more than ordinary induction?
  5. Give an example of a function whose correctness proof goes through but whose termination proof does not. What does that tell you?
  6. In mergesort the induction is on len(A). What measure do you induct on when the recursion is on a tree instead of a list (e.g., a mirror(t) function on a binary tree)?
  7. Why is the inductive step of power(x, n) a good pattern to mimic in "repeated squaring" algorithms elsewhere (matrix exponentiation, modular power)?

Mini Drill or Application​

Prove correctness of each. State pre/post, base case, and inductive step explicitly.

  1. A recursive sum: sum(A) returns the sum of the list.
  2. Binary search on a sorted list: returns the index of $x$ or $-1$.
  3. Euclid's GCD: gcd(a, b) = gcd(b, a % b), base gcd(a, 0) = a.
  4. reverse(A) via recursion: reverse([]) = [], reverse(x :: xs) = reverse(xs) ++ [x].
  5. Tower of Hanoi: hanoi(n, src, dst, tmp) prints a valid sequence of $2^n - 1$ moves.
  6. Implementation drill. Implement fib_pair(n) that returns $(F_n, F_{n+1})$ using the recurrence on $(n/2)$ via the identities $F_{2k} = F_k (2 F_{k+1} - F_k)$, $F_{2k+1} = F_k^2 + F_{k+1}^2$. Prove correctness by strong induction. Complexity derivation: $T(n) = T(n/2) + \Theta(1) = \Theta(\log n)$.

Read This Only If Stuck​