New Directions for Syntactic Termination Orderings

Abstract

There is a wide diversity of orderings on data structures such as strings, multisets, vectors, permutations and terms. Orderings on strings which are preserved under concatenation and make words bigger than subwords,are a widely used technique for proving termination of string rewriting systems, or, more generally, of other processes over strings. Until recently the theory of division orderings on strings seemed diverse and incomprehensible: many different orderings were known but there was no common framework in which to understand or classify them. Recent work has shown that total division orderings on strings can be classified in terms of certain numeric and ordinal invariants. This paper surveys this work, and discusses some new research directions arising from attempts to extend it to other data structures.