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.
Read more about this topic: Loop Variant
Other articles related to "practical considerations, practical":
... or transfinite variant? This question has been raised because in all practical instances where we want to prove that a program terminates, we also want to prove that it terminates in a ...
Famous quotes containing the word practical:
“Missionaries, whether of philosophy or religion, rarely make rapid way, unless their preachings fall in with the prepossessions of the multitude of shallow thinkers, or can be made to serve as a stalking-horse for the promotion of the practical aims of the still larger multitude, who do not profess to think much, but are quite certain they want a great deal.”
—Thomas Henry Huxley (182595)