Abstract

Faced with an ad-hoc collection of computational or mathematical objects an obvious impulse is to try and classify them: if we can do so in terms of existing mathematical structures we can, with luck, get new understanding of our original problem and find new phenomena that were not originally apparent.

Proving that a computation or process terminates generally requires showing that something is reduced in a well-founded ordering, and a wide variety of orderings on common data structures have been devised for the purpose.

We investigate monotonic well-founded orderings on multisets, strings and terms and show that despite the apparent diversity they can be studied in a unifying framework that provides a classifying space related to projective geometry, and hence logical and numeric invariants for the different orderings.

An initial understanding is provided by the order type. We outline a finer classification, showing that in each case the relevant orders are essentially extensions of an order by weight. This allows us to associate numerical invariants to orders, to show that several previously studied orderings were equivalent and to reduce some termination proofs to constraint solving.

We describe applications and extensions in fields as diverse as computer algebra, group theory and computational biology.