Invariants, Patterns and Weights for Ordering Terms

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)

Abstract

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. (C) 2000 Academic Press.

Original languageEnglish
Pages (from-to)921-957
Number of pages37
JournalJournal of Symbolic Computation
Volume29
Issue number6
DOIs
Publication statusPublished - Jun 2000

Keywords

  • DIVISION ORDERINGS
  • REWRITING-SYSTEMS
  • TERMINATION
  • STRINGS
  • THEOREM

Fingerprint

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

Cite this