# 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 *x*_{1}, *x*_{2}, *x*_{3},… of members of *S* for which each pair 〈*x _{i}*,

*x*

_{i}_{+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**