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. A loop variant whose range is restricted to the non-negative integers is also known as a bound function, because in this case it provides a trivial upper bound on the number of iterations of a loop before it terminates. 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 . [1] A basic property of a well-founded relation is that it has no infinite 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.
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:
where I is the invariant , C is the condition, and S is the body of the loop. 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.
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
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 ω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 . 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.
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.
/** condition-variable, which is changed in procedure S() **/boolC;/** function, which computes a loop iteration bound without side effects **/inlineunsignedintgetBound();/** body of loop must not alter V **/inlinevoidS();intmain(){unsignedintV=getBound();/* set variant equal to bound */assert(I);/* loop invariant */while(C){assert(V>0);/* this assertion is the variant's raison d'être (reason of existence) */S();/* call the body */V=min(getBound(),V-1);/* variant must decrease by at least one */};assert(I&&!C);/* invariant is still true and condition is false */return0;};Why even consider a non-integer 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 reasonable amount of time. There are at least two possibilities:
In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical.
In mathematics, a binary relation R is called well-founded on a class X if every non-empty subset S ⊆ X has a minimal element with respect to R, that is, an element m not related by sRm for any s ∈ S. In other words, a relation is well founded if
In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:
In computer science, a loop invariant is a property of a program loop that is true before each iteration. It is a logical assertion, sometimes checked within the code by an assertion call. Knowing its invariant(s) is essential in understanding the effect of a loop.
In mathematics, an invariant subspace of a linear mapping T : V → V from some vector space V to itself, is a subspace W of V that is preserved by T; that is, T(W) ⊆ W.
In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the five primitive recursive operators makes it possible to define all computable functions.
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. Computable functions are used to discuss computability without referring to any concrete model of computation such as Turing machines or register machines. Any definition, however, must make reference to some specific model of computation but all valid definitions yield the same class of functions. Particular models of computability that give rise to the set of computable functions are the Turing-computable functions and the μ-recursive functions.
In computer science, corecursion is a type of operation that is dual to recursion. Whereas recursion works analytically, starting on data further from a base case and breaking it down into smaller data and repeating until one reaches a base case, corecursion works synthetically, starting from a base case and building it up, iteratively producing data further removed from a base case. Put simply, corecursive algorithms use the data that they themselves produce, bit by bit, as they become available, and needed, to produce further bits of data. A similar but distinct concept is generative recursion which may lack a definite "direction" inherent in corecursion and recursion.
Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions.
The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
In computer science, recursion is a method of solving a problem where the solution depends on solutions to smaller instances of the same problem. Such problems can generally be solved by iteration, but this needs to identify and index the smaller instances at programming time. Recursion solves such recursive problems by using functions that call themselves from within their own code. The approach can be applied to many types of problems, and recursion is one of the central ideas of computer science.
The power of recursion evidently lies in the possibility of defining an infinite set of objects by a finite statement. In the same manner, an infinite number of computations can be described by a finite recursive program, even if this program contains no explicit repetitions.
In numerical linear algebra, the method of successive over-relaxation (SOR) is a variant of the Gauss–Seidel method for solving a linear system of equations, resulting in faster convergence. A similar method can be used for any slowly converging iterative process.
In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.
Forcing in recursion theory is a modification of Paul Cohen's original set-theoretic technique of forcing to deal with the effective concerns in recursion theory. Conceptually the two techniques are quite similar: in both one attempts to build generic objects by meeting dense sets. Both techniques are described as a relation between 'conditions' and sentences. However, where set-theoretic forcing is usually interested in creating objects that meet every dense set of conditions in the ground model, recursion-theoretic forcing only aims to meet dense sets that are arithmetically or hyperarithmetically definable. Therefore, some of the more difficult machinery used in set-theoretic forcing can be eliminated or substantially simplified when defining forcing in recursion theory. But while the machinery may be somewhat different, recursion-theoretic and set-theoretic forcing are properly regarded as an application of the same technique to different classes of formulas.
In the fields of computer vision and image analysis, the Harris affine region detector belongs to the category of feature detection. Feature detection is a preprocessing step of several algorithms that rely on identifying characteristic points or interest points so to make correspondences between images, recognize textures, categorize objects or build panoramas.
In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.
In mathematics, given a quiver Q with set of vertices Q0 and set of arrows Q1, a representation of Q assigns a vector space Vi to each vertex and a linear map V(α): V(s(α)) → V(t(α)) to each arrow α, where s(α), t(α) are, respectively, the starting and the ending vertices of α. Given an element d ∈ ℕQ0, the set of representations of Q with dim Vi = d(i) for each i has a vector space structure.
Attempts have been made to describe gauge theories in terms of extended objects such as Wilson loops and holonomies. The loop representation is a quantum hamiltonian representation of gauge theories in terms of loops. The aim of the loop representation in the context of Yang–Mills theories is to avoid the redundancy introduced by Gauss gauge symmetries allowing to work directly in the space of physical states. The idea is well known in the context of lattice Yang–Mills theory. Attempts to explore the continuous loop representation was made by Gambini and Trias for canonical Yang–Mills theory, however there were difficulties as they represented singular objects. As we shall see the loop formalism goes far beyond a simple gauge invariant description, in fact it is the natural geometrical framework to treat gauge theories and quantum gravity in terms of their fundamental physical excitations.