Program termination and well partial orderings
Andreas R. Blass, Yuri G. Gurevich · ACM Transactions on Computational Logic · 2008
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 | R | of the relation R in terms of the ordinals α i = | U i |. We introduce the notion of the stature ∥ P ∥ of a well partial ordering P and show that | R | ≤ ∥α 1 × … × α n ∥ and that this bound is tight. The notion of stature is of considerable independent interest. We define ∥ P ∥ as the ordinal height of the forest of nonempty bad sequences of P , but it has many other natural and equivalent definitions. In particular, ∥ P ∥ is the supremum, and in fact the maximum, of the lengths of linearizations of P . And ∥α 1 × … × α n ∥ is equal to the natural product α 1 ⊗ … ⊗ α n .