In computer science, a loop variant is a mathematical function defined on the state space of a computer program whose value is monotonically decreased with respect to a (strict) well-founded relation by the iteration of a while loop under some invariant conditions, thereby ensuring its termination.
However, a loop variant may be transfinite, and thus is not necessarily restricted to integer values.
A well-founded relation is characterized by the existence of a minimal element of every non-empty subset of its domain.
The existence of a variant proves the termination of a while loop in a computer program by well-founded descent.
To express total correctness, we write instead: where, in addition, V is the variant, and by convention the unbound symbol z is taken to be universally quantified.
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.
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.
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 ω1, 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 ω1 is the enumeration of all well-order types on countable sets.
In practice, loop variants are often taken to be non-negative integers, or even required to be so,[2] but the requirement that every loop have an integer variant removes the expressive power of unbounded iteration from a programming language.
Unless such a (formally verified) language allows a transfinite proof of termination for some other equally powerful construct such as a recursive function call, it is no longer capable of full μ-recursion, but only primitive recursion.
In terms of their computational complexity, however, functions that are not primitive recursive lie far beyond the realm of what is usually considered tractable.
So it is difficult to imagine a practical use for full μ-recursion where primitive recursion will not do, especially since the former can be simulated by the latter up to exceedingly long running times.
And in any case, Kurt Gödel's first incompleteness theorem and the halting problem imply that there are while loops that always terminate but cannot be proven to do so; thus it is unavoidable that any requirement for a formal proof of termination must reduce the expressive power of a programming language.
Here is an example, in C-like pseudocode, of an integer variant computed from some upper bound on the number of iterations remaining in a while loop.
However, C allows side effects in the evaluation of expressions, which is unacceptable from the point of view of formally verifying a computer program.