Case Study: Proving Horner's Method Correct with a Loop Invariant

"Testing shows the presence, not the absence, of bugs." — Edsger W. Dijkstra

Executive Summary

You'll take a small, fast, slightly mysterious loop — Horner's method for evaluating a polynomial — and prove that it is correct for every polynomial and every input, using a single loop invariant. This is the technique from §6.5 applied to code you'll actually meet again: Horner's method is the standard way to evaluate polynomials, and the same loop shape powers polynomial hashing (Chapter 26) and modular exponentiation (Chapter 23). The point is not that Horner's method is hard — it's that "I ran it on a few polynomials and it worked" is not the same as "it is correct," and a loop invariant closes that gap.

Skills applied

  • Translating an informal claim ("this loop evaluates the polynomial") into a precise statement.
  • Stating a loop invariant at a fixed program point.
  • Proving the invariant by induction (initialization, maintenance) and adding a termination argument.
  • Connecting the proof to the structure of the code.

Background

The scenario

A teammate submits this function in a code review:

def horner(coeffs, x):
    """Evaluate a polynomial at x. coeffs[i] is the coefficient of x**i,
    so coeffs = [a0, a1, ..., an] represents a0 + a1*x + ... + an*x**n."""
    result = 0
    for a in reversed(coeffs):
        result = result * x + a
    return result

print(horner([1, 2, 3], 2))   # 1 + 2*2 + 3*4 = 17
# Expected output:
# 17

It's three lines and it passes the one test in the PR. But it's doing something non-obvious: it walks the coefficients from the top down and repeatedly multiplies by x and adds the next coefficient. Why does that compute $a_0 + a_1 x + a_2 x^2 + \dots + a_n x^n$? Your job in review is to be sure — not "it looks right," but "here's why it's right for every input."

💡 Intuition: Horner's method factors the polynomial as a nest: $a_0 + a_1 x + a_2 x^2 + a_3 x^3 = a_0 + x\big(a_1 + x(a_2 + x \cdot a_3)\big).$ Evaluating the nest from the inside out is exactly what the loop does — but "it looks like the nest" is intuition, not proof. Let's prove it.

Why this matters

Polynomial evaluation is everywhere: in graphics (Bézier curves), in cryptography and hashing (treat a string as the coefficients of a polynomial and evaluate it modulo a prime — Chapter 26), and in the fast modular exponentiation that makes RSA practical (Chapter 23). The loop you're verifying here is a pattern you'll trust thousands of times. Verifying it once, properly, is worth the hour.

Phase 1: State the claim precisely

Let the input be $\text{coeffs} = [a_0, a_1, \dots, a_n]$, representing the polynomial $$p(x) = \sum_{i=0}^{n} a_i x^i.$$ We want to prove:

Claim. horner(coeffs, x) returns $p(x) = \sum_{i=0}^{n} a_i x^i$.

The loop iterates over reversed(coeffs), i.e. it processes $a_n, a_{n-1}, \dots, a_1, a_0$ in that order. To reason about "how far we've gotten," index the iterations: after the loop has processed $a_n, a_{n-1}, \dots, a_{n-j+1}$ — that is, after $j$ iterations — call the value held in result $r_j$. So $r_0 = 0$ (before any iteration), and each iteration does $r_{j+1} = r_j \cdot x + a_{n-j}$.

🔄 Check Your Understanding After processing just $a_n$ (one iteration), what is result? After processing $a_n$ then $a_{n-1}$ (two iterations)?

Answer

After one iteration: $r_1 = 0 \cdot x + a_n = a_n$. After two: $r_2 = a_n x + a_{n-1}$. Notice $r_2 = a_{n-1} + a_n x$ — the top two terms of the polynomial, in "nested" form.

Phase 2: Find the invariant

The hard part of a loop proof is guessing the invariant; the rest is mechanical. From the hand-computations above, after $j$ iterations result holds the top $j$ coefficients assembled in Horner form: $$r_1 = a_n, \quad r_2 = a_n x + a_{n-1}, \quad r_3 = a_n x^2 + a_{n-1} x + a_{n-2}, \ \dots$$ Reading the pattern, after $j$ iterations: $$r_j = \sum_{i=0}^{j-1} a_{n-i}\, x^{\,j-1-i} = a_n x^{j-1} + a_{n-1} x^{j-2} + \dots + a_{n-j+1}.$$

That sum is awkward; a cleaner equivalent form (re-indexing $t = n - i$) is the invariant we'll use:

Invariant $I(j)$. After $j$ iterations of the loop ($0 \le j \le n+1$), $$\text{result} = \sum_{t=n-j+1}^{n} a_t\, x^{\,t-(n-j+1)}.$$ Equivalently: result holds the polynomial formed by the top $j$ coefficients, evaluated as if they were the bottom $j$ coefficients.

⚠️ Common Pitfall: It is tempting to write an invariant that's "almost right" and patch it later. Resist. Hand-compute $r_1, r_2, r_3$ first (Phase 1), and only then write the invariant that fits them. An invariant guessed before checking small cases is usually wrong in its index bounds.

Phase 3: Prove the invariant by induction

We prove $I(j)$ for $j = 0, 1, \dots, n+1$ by induction on $j$ — initialization is the base case, maintenance is the inductive step.

Initialization (base case, $j = 0$). Before any iteration, result $= 0$. The invariant's sum for $j = 0$ is empty (the index range $t = n+1$ down to $n$ is empty), which is $0$. So $I(0)$ holds.

Maintenance (inductive step). Assume $I(j)$ holds for some $j$ with $0 \le j \le n$, so $$r_j = \sum_{t=n-j+1}^{n} a_t\, x^{\,t-(n-j+1)}.$$ The next iteration processes coefficient $a_{n-j}$ and computes $r_{j+1} = r_j \cdot x + a_{n-j}$. Multiplying the hypothesis by $x$ raises every exponent by 1: $$r_j \cdot x = \sum_{t=n-j+1}^{n} a_t\, x^{\,t-(n-j+1)+1} = \sum_{t=n-j+1}^{n} a_t\, x^{\,t-(n-j)}.$$ Now add $a_{n-j}$. Note $a_{n-j} = a_{n-j} x^{0} = a_{n-j} x^{(n-j)-(n-j)}$, which is exactly the $t = n-j$ term of the same sum. So adding it extends the lower limit from $n-j+1$ down to $n-j$: $$r_{j+1} = \sum_{t=n-j}^{n} a_t\, x^{\,t-(n-j)} = \sum_{t = n-(j+1)+1}^{n} a_t\, x^{\,t-(n-(j+1)+1)},$$ which is precisely $I(j+1)$. So the invariant is maintained.

By induction, $I(j)$ holds after every iteration $j = 0, 1, \dots, n+1$. $\blacksquare$ (invariant)

🔗 Connection: The maintenance step used the same algebra as a summation induction — "multiply through, then absorb the new term by extending the index." If §6.3's summation proofs felt abstract, here they are paying rent inside a real correctness argument.

Phase 4: Termination and conclusion

The loop runs once per element of coeffs, so it performs exactly $n+1$ iterations (for coefficients $a_0, \dots, a_n$) and then stops. Applying the invariant at $j = n+1$: $$\text{result} = \sum_{t = n-(n+1)+1}^{n} a_t\, x^{\,t-(n-(n+1)+1)} = \sum_{t=0}^{n} a_t\, x^{\,t} = p(x).$$ That is the value returned. Therefore horner(coeffs, x) returns $p(x)$ for every coefficient list and every $x$. $\blacksquare$

We have proved correctness for infinitely many inputs — every polynomial, every argument — with one finite argument. No amount of testing could have done that.

🐛 Find the Error: A reviewer claims the invariant should be "after $j$ iterations, result $= \sum_{t=0}^{j-1} a_t x^t$" (the bottom $j$ coefficients). Hand-compute $r_1$ for coeffs = [1, 2, 3], $x = 2$ and show this proposed invariant is wrong.

Answer

The loop processes the top coefficient first: $r_1 = 0 \cdot 2 + 3 = 3 = a_2$. The proposed invariant predicts $r_1 = \sum_{t=0}^{0} a_t x^t = a_0 = 1$. Since $3 \ne 1$, the proposed invariant fails initialization-plus-one. The bug is direction: Horner builds from the high-degree end down.

Discussion Questions

  1. The proof never assumed the coefficients were integers, or even real. For what kinds of coeffs and x does the argument still go through? (Hint: what operations did we use?)
  2. How does the loop behave on the empty coefficient list []? Does the claim, as stated, cover that case? Adjust the claim if needed.
  3. Horner's method uses $n$ multiplications and $n$ additions. The "naive" method ($\sum a_i \cdot x^i$, recomputing each power) uses far more. Estimate the naive count and explain why Horner is preferred — connecting to Chapter 14's cost analysis.
  4. Where, exactly, would the proof break if the line were result = result + x * a instead of result = result * x + a? Which step of the induction fails?

Your Turn: Extensions

  • Option A (modular Horner). Modify horner to compute $p(x) \bmod m$ by reducing after each step. State the new invariant (it includes "$\bmod m$") and argue correctness. This is exactly polynomial hashing (Chapter 26).
  • Option B (derivative). Extend the loop to also compute $p'(x)$ in the same pass. State the second invariant and prove it. (This is "Horner for derivatives," used in root-finding.)
  • Option C (formal check). Use the Toolkit's check_identity to compare horner(coeffs, x) against a naive evaluator for 50 random-looking polynomials and inputs you write out by hand. Explain what a None result does and does not establish.

Key Takeaways

  1. Guess the invariant from small cases, then prove it. Hand-computing $r_1, r_2, r_3$ is what makes the right invariant visible; writing the invariant first usually gets the index bounds wrong.
  2. A loop proof is an induction proof. Initialization is the base case; maintenance is the inductive step; termination connects the final invariant to the returned value.
  3. Correctness is universal; testing is not. One invariant argument covered every polynomial and every input — something no finite test suite can do.
  4. The same loop recurs across CS. Horner's shape reappears in hashing and modular exponentiation; verifying it here pays off in Parts III and IV.