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
You Might Also Like
NEARBY TERMS
well-founded relation