Invariants, Patterns and Weights for Ordering Terms

Ursula Martin, Duncan Shand

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We prove that any simplification order over arbitrary terms is an extension of an order by weight, by considering a related monadic term algebra called the spine. We show that any total ground-stable simplification order on the spine lifts to an order on the full term algebra. Conversely, under certain restrictions, a simplification ordering on the term algebra defines a weight function on the spine, which in turn can be lifted to a weight order on the original ground terms which contains the original order. We investigate the Knuth–Bendix and polynomial orders in this light. We provide a general framework for ordering terms by counting embedded patterns, which gives rise to many new orderings. We examine the recursive path order in this context.
Original languageEnglish
Pages (from-to)921-957
Number of pages37
JournalJournal of Symbolic Computation
Issue number6
Publication statusPublished - 2000


Dive into the research topics of 'Invariants, Patterns and Weights for Ordering Terms'. Together they form a unique fingerprint.

Cite this