Program Termination, and Well Partial Orderings

  • Andreas Blass ,
  • Yuri Gurevich

MSR-TR-2006-27 |

The following known observation may be 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| less than or equal to the stature of the direct product of ordinals α 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 the stature of the direct product of ordinals α 1 ,…,α n is equal to the natural product of these ordinals.