Program termination and well partial orderings
The following known observation is useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U(1),..., U(n) then R is well-founded. A question arises how to bound the ordinal height vertical bar R vertical bar of the relation R in terms of the ordinals alpha(i) = vertical bar U(i) vertical bar. We introduce the notion of the stature parallel to P parallel to of a well partial ordering P and show that vertical bar R vertical bar <= parallel to alpha(1) x ... x alpha(n) parallel to and that this bound is tight. The notion of stature is of considerable independent interest. We define parallel to P parallel to as the ordinal height of the forest of nonempty bad sequences of P, but it has many other natural and equivalent definitions. In particular, parallel to P parallel to is the supremum, and in fact the maximum, of the lengths of linearizations of P. And parallel to alpha(1) x ... x alpha(n) parallel to is equal to the natural product alpha(1) circle times ... circle times alpha(n).
program termination well partial orderings algorithms theory covering observation game criterion