Proving Termination

A loop invariant proves your loop is right — but only if it stops. That "if" is not a technicality: the program \texttt{while } x \ne 0 \texttt{ do skip} preserves every invariant you could wish for and delivers no answer at all, because it spins forever. Partial correctness and termination are two different claims, and invariants speak only to the first.

So how do you prove a loop stops? You cannot run it and wait — that never proves anything, and in general the question is undecidable. The classical technique is beautifully simple: exhibit a quantity that must go down every iteration but cannot go below a floor. Squeezed between a strict descent and a hard floor, the loop has nowhere to run.

The variant (ranking function)

A variant (or ranking function) for a loop \texttt{while } b \texttt{ do } C is an integer-valued expression V over the program variables such that, whenever the guard b holds:

Then the loop terminates.

The argument is pure arithmetic. Each iteration strictly decreases an integer that never drops below 0. A strictly decreasing sequence of non-negative integers cannot be infinite — after at most V_0 + 1 steps (its starting value) there is no room left. No guard can still be true, so the loop is over. Notice this also hands you a running-time bound for free: the initial variant value is an upper bound on the iteration count.

The picture is the whole idea: the variant is a staircase that only ever steps down, and the floor at 0 stops the staircase after finitely many steps. Contrast the invariant, which is a property that stays the same; the variant is a quantity that reliably shrinks.

Worked variants

Finding a variant is usually easy: ask "what is getting smaller?" Here are three staples.

// (1) Countdown. Variant V = n. while (n > 0) { n = n - 1; // V drops by exactly 1; guard n>0 keeps V >= 1 > 0 } // V = n: bounded below by 0, strictly decreasing. Halts in n steps. // (2) Integer division of a by d (a >= 0, d > 0). Variant V = r. let q = 0, r = a; while (r >= d) { r = r - d; // r decreases by d >= 1 each pass q = q + 1; } // V = r: while the guard r >= d holds, r >= 0; each pass lowers r by d. Halts. // (3) Euclid's gcd by subtraction (a, b >= 1). Variant V = a + b. while (a !== b) { if (a > b) { a = a - b; } else { b = b - a; } // one of a,b strictly drops } // V = a + b: always >= 2 while looping, and every pass makes it strictly smaller. Halts.

In each case the variant is the smallest honest measure of "how much work is left." For the countdown it is n itself; for division it is the remainder r; for gcd it is the sum a + b (neither a nor b alone decreases every step, but their sum does).

Nested loops need lexicographic variants

Sometimes a single integer will not fall every step. Consider an outer loop that occasionally resets an inner counter — no one number monotonically shrinks. The fix is to rank states by a tuple compared lexicographically (like dictionary order): (x, y) < (x', y') iff x < x', or x = x' and y < y'.

// Variant V = (n - i, n - j) compared lexicographically. let i = 0, j = 0; while (i < n) { if (j < n) { j = j + 1; } // second component drops; first unchanged else { i = i + 1; j = 0; } // first component drops (j reset is fine!) }

When the inner branch runs, the first component n - i is unchanged but the second n - j falls. When the outer branch runs, the first component falls — and we do not care that j resets, because a drop in a more-significant digit beats any change below it. The tuples live in a well-founded order: one with no infinite strictly-decreasing chain. Non-negative integers are the simplest such order; lexicographic tuples of them are the next.

The wall: termination is undecidable

Could we skip the cleverness and write a tool that, given any program, simply tells us whether it halts? Turing proved in 1936 that we cannot: the halting problem is undecidable. No algorithm decides termination for all programs. That is why a variant is not a mechanical afterthought but a genuine proof obligation the human must discharge — the undecidability is dodged precisely because you supply the ranking function; the tool only has to check your candidate decreases, which is easy.

So termination proving is a partnership: undecidability says no tool can always find the variant, but for any particular loop a well-chosen variant makes the proof short and certain. The art is in the choosing.

A variant is more than a termination certificate — it is a step counter in disguise. Since V starts at V_0, drops by at least 1 each iteration, and stops at 0, the loop runs at most V_0 times. For the countdown that is n steps; for integer division it is \lceil a/d \rceil (the remainder falls by d each pass); for a variant that halves each step, like binary search's interval width, it is \log_2 V_0. The same expression that proves the loop stops often hands you its asymptotic cost in the bargain — which is why a good variant is the first thing to look for when you analyse a loop, whether your goal is correctness or complexity.

Two classic slips. First, do not confuse the roles: the invariant stays true (unchanging), while the variant strictly decreases. They answer different questions — "is it right?" versus "does it stop?" — and you generally need both. Second, "decreasing" alone never proves termination: the values 10, 9, 8, \ldots could sail past 0 into -1, -2, \ldots forever if there is no floor, and a real-valued quantity can shrink infinitely while never reaching its bound (1, \tfrac12, \tfrac14, \ldots never hits 0). You need both the strict decrease and the well-founded floor — an integer bounded below by 0, or values in some well-founded order. Drop either half and the proof collapses.