well-founded relation
well-founded relation A particular kind of partial ordering, used in termination proofs (see program correctness proof). A well-founded relation on a set S consists of a partial ordering R ⊆ S × S
such that there does not exist any infinite sequence x1, x2, x3,… of members of S for which each pair 〈xi,xi+1〉 belongs to R. As an example, if S consists of the natural numbers, then the “greater than” relation, containing all pairs 〈m,n〉 such that m>n, is well-founded, since there are no infinite descending sequences of natural numbers. On the other hand “greater than or equal to”, and “less than” are not well-founded. On the set of integers, none of these relations are well-founded. As another example, if S is the set of all finite sets of natural numbers, then “proper superset of” is well-founded.
In the application to terminate proofs it is shown that, whenever a certain point in the program is visited during execution, the current value of some quantity lies within S and also that, if x is the value of that quantity at one such visit, and x′ its value at a later visit, the pair 〈x,x′〉 belongs to R. It then follows that that point in the program cannot be visited infinitely often. By considering enough such points it can be concluded that any execution must have finite length.
such that there does not exist any infinite sequence x1, x2, x3,… of members of S for which each pair 〈xi,xi+1〉 belongs to R. As an example, if S consists of the natural numbers, then the “greater than” relation, containing all pairs 〈m,n〉 such that m>n, is well-founded, since there are no infinite descending sequences of natural numbers. On the other hand “greater than or equal to”, and “less than” are not well-founded. On the set of integers, none of these relations are well-founded. As another example, if S is the set of all finite sets of natural numbers, then “proper superset of” is well-founded.
In the application to terminate proofs it is shown that, whenever a certain point in the program is visited during execution, the current value of some quantity lies within S and also that, if x is the value of that quantity at one such visit, and x′ its value at a later visit, the pair 〈x,x′〉 belongs to R. It then follows that that point in the program cannot be visited infinitely often. By considering enough such points it can be concluded that any execution must have finite length.
More From encyclopedia.com
Domain , Domain
The domain of a relation is the set that contains all the first elements, x, from the ordered pairs (x,y) that make up the relation. In mathem… Lysithea , Lysithea (Jupiter X) One of the lesser satellites of Jupiter, with a diameter of 24km. Diophantus Of Alexandria , Diophantus of Alexandria
Diophantus of Alexandria
(fl. ad. 250)
mathematics.
We know virtually nothing about the life of Diophantus. The dating of hi… Inverse Matrix , Inverse Matrix
BIBLIOGRAPHY
The concept of inverse matrix is somewhat analogous to that of the reciprocal of a number. If a is a nonzero number, then… Exponent , Skip to main content
exponent
exponent •abeyant, mayn't •ambient, circumambient •gradient, irradiant, radiant •expedient, ingredient, mediant, obedie… George Boole , Boole, George
Boole, George
(b. Lioncoln, England, 1815; d. Cork, Ireland, 1864)
mathematics.
George Boole was the son of John Boole, a cobbler whose…
You Might Also Like
NEARBY TERMS
well-founded relation