Orderings for term-rewriting systems
Open Access
- 1 October 1979
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 59 (02725428), 123-131
- https://doi.org/10.1109/sfcs.1979.32
Abstract
Methods of proving that a term-rewriting system terminates are presented. They are based on the notion of "simplification orderings", orderings in which any term that is homeomorphically embeddable in another is smaller than the other. A particularly useful class of simplification orderings, the "recursive path orderings", is defined. Several examples of the use of such orderings in termination proofs are given.Keywords
This publication has 6 references indexed in Scilit:
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Automatic Proofs of Theorems in Analysis Using Nonstandard TechniquesJournal of the ACM, 1977
- REDUCE 2Published by Association for Computing Machinery (ACM) ,1971
- SCRATCHPAD/1Published by Association for Computing Machinery (ACM) ,1971
- On well-quasi-ordering finite treesMathematical Proceedings of the Cambridge Philosophical Society, 1963
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's ConjectureTransactions of the American Mathematical Society, 1960