Loop Variant - Practical Considerations

Practical Considerations

In practice, loop variants are often taken to be non-negative integers, or even required to be so, 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 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 a variant, this does not mean that the well-foundedness of the loop iteration can be proven.