Loop Variant - Every Loop That Terminates Has A Variant

Every Loop That Terminates Has A Variant

The existence of a variant implies that a while loop terminates. It may seem surprising, but the converse is true, as well, as long as we assume the axiom of choice: every while loop that terminates (given its invariant) has a variant. To prove this, assume that the loop

terminates given the invariant I where we have the total correctness assertion

Consider the "successor" relation on the state space induced by the execution of the statement S from a state satisfying both the invariant I and the condition C. That is, we say that a state is a "successor" of if and only if

• I and C are both true in the state and
• is the state that results from the execution of the statement S in the state

We note that for otherwise the loop would fail to terminate.

Next consider the reflexive, transitive closure of the "successor" relation. Call this iteration: we say that a state is an iterate of if either or there is a finite chain such that and is a "successor" of for all i,

We note that if and are two distinct states, and is an iterate of, then cannot be an iterate of for again, otherwise the loop would fail to terminate. In other words, iteration is antisymmetric, and thus, a partial order.

Now, since the while loop terminates after a finite number of steps given the invariant I, and no state has a successor unless I is true in that state, we conclude that every state has only finitely many iterates, every descending chain with respect to iteration has only finitely many distinct values, and thus there is no infinite descending chain, i.e. loop iteration satisfies the descending chain condition.

Therefore—assuming the axiom of choice—the "successor" relation we originally defined for the loop is well-founded on the state space since it is strict (irreflexive) and contained in the "iterate" relation. Thus the identity function on this state space is a variant for the while loop, as we have shown that the state must strictly decrease—as a "successor" and an "iterate"—each time the body S is executed given the invariant I and the condition C.

Moreover, we can show by a counting argument that the existence of any variant implies the existence of a variant in ω₁, the first uncountable ordinal, i.e.,

This is because the collection of all states reachable by a finite computer program in a finite number of steps from a finite input is countably infinite, and ω₁ is the enumeration of all well-order types on countable sets.