Loop variant

In computer science, a loop variant is a mathematical function defined on the state space of a computer program having the property that each iteration of a loop (given its invariant) strictly decreases its value with respect to a well-founded relation.

A loop variant is used to prove the termination of a while loop in a computer program by well-founded descent. (See also [Glynn Winskel. "The Formal Semantics of Programming Languages: An Introduction." Massachusetts Institute of Technology, 1993.] , pp. 32–33, 174–176.) A basic property of a well-founded relation is that it has no infinite strictly descending chains. Therefore a loop possessing a variant will terminate after a finite number of iterations, as long as its body terminates each time.

A while loop, or, more generally, a computer program that may contain while loops, is said to be totally correct if it is partially correct and it terminates.

Rule of inference for total correctness

In order to formally state the rule of inference for the termination of a while loop we have demonstrated above, recall that in Floyd-Hoare logic, the rule for expressing the partial correctness of a while loop is::$$frac{{I land C};S;{I {{I};mathbf{while};C; mathbf{do}; S ;{lnot Cland I,where "I" is the "invariant", "C" is the "condition", and "S" is the "body" of the loop. To express total correctness, we write instead::$$frac{(Z,le) extrm{ is well-founded},; forall zin Z; [I land C land V=z ] ;S; [I land V le z land V eq z] } { [I] ;mathbf{while};C; mathbf{do}; S ; [lnot Cland I] },where, in addition, $$V:Sigma ightarrow Z is the "variant".

Every loop that terminates has a variant

Heretofore we have argued that the existence of a variant implies that a while loop terminates. It may seem surprising, but the converse is true, as well: every while loop that terminates has a variant. To prove this, assume that the loop:$$mathbf{while};C; mathbf{do} ; Sterminates given the invariant "I" where we have the total correctness assertion:$$ [I land C ] ;S; [I] .Consider the "successor" relation on the state space $$Sigma 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 $$sigma' is a "successor" of $$sigma if and only if
* "I" and "C" are both true in the state $$sigma, and
* $$sigma' is the state that results from the execution of the statement "S" in the state $$sigma.We note that $$sigma' eq sigma, 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 $$sigma' is an "iterate" of $$sigma if either $$sigma' = sigma, or there is a finite chain $$sigma_0, sigma_1,,dots,,sigma_n such that $$sigma_0 = sigma, $$sigma_n = sigma' and $$sigma_{i+1} is a "successor" of $$sigma_i for all "i", $$0 le i < n.

We note that if $$sigma and $$sigma' are two distinct states, and $$sigma' is an iterate of $$sigma, then $$sigma cannot be an iterate of $$sigma', 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 every "infinite" descending chain is eventually constant, so loop iteration satisfies the descending chain condition.

Therefore iteration of the loop is well-founded on the state space $$Sigma, and 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 an iterate—each time the body "S" is executed given the invariant "I" and the condition "C".

Practical considerations

In practice, loop variants are often taken to be non-negative integers, or even required to be so, e.g. [ [http://archive.eiffel.com/doc/faq/variant.html Eiffel: Why loop variants are integers] ] , 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. Ackermann's function is the canonical example of a recursive function that cannot be computed in a loop with an integer variant.

In terms of their computational complexity, however, functions that are not primitive recursive lie far beyond the realm of what is usually considered tractable. Considering even the simple case of exponentiation as a primitive recursive function, and that the composition of primitive recursive functions is primitive recursive, one can begin to see how quickly a primitive recursive function can grow. And any function that can be computed by a Turing machine in a running time bounded by a primitive recursive function is itself primitive recursive. So it is difficult to imagine a practical use for 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. While we have shown that every loop that terminates has an invariant, this does not mean that the well-foundedness of the loop iteration can be proven.

References

ee also

* While loop
* Loop invariant
* Transfinite induction
* Descending chain condition
* Total correctness