## Quick Reference

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*

*〉 belongs to*

_{i+1}*R*. As an example, if

*S*consists of the natural numbers, then the “greater than” elation, 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.

*R* ⊆ *S* × *S*

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.

*Subjects:*
Computing.