Linear interpretations by counting patterns
We introduce a new family of well-founded monotonic orderings on terms, constructed bu counting certain patterns in terms called zig-zags. These extend the familiar Knuth Bendix orderings, providing in general continuum many distinct new orderings with a given choice of Knuth-Bendix weight.
KeywordsFunction Symbol Coordinate Vector Springer Lecture Note Standard Basis Vector Recursive Decomposition
Unable to display preview. Download preview PDF.
- 7.J-P. Jouannaud, P. Lescanne and F. Reinig, Recursive decomposition ordering, in Formal description of programming concepts 2, Elsevier 1982, ed D Bjorner, pp 331–348Google Scholar
- 8.D. Knuth and P. Bendix, Simple Word Problems in Universal Algebras, in Computational Problems in Abstract Algebra, Pergamon Press 1970, ed J. Leech.Google Scholar
- 9.D. S. Lankford, On proving term rewriting systems are Noetherian, Tech report MTP-3, Louisiana Technical University, Ruston 1979Google Scholar
- 10.P. Lescanne, Termination of rewrite systems by elementary interpretations, in H Kirchner and G Levi, editors, Proc 3rd International Conference on Algebraic and Logic Programming, Springer Lecture Notes in Computer Science 463 (1992) 21–36Google Scholar
- 12.U. Martin, On the diversity of orderings on strings, RHBNC Technical Report 1991Google Scholar
- 13.P. Narendran and M. Rusinowitch, Any ground associative-commutative theory has a finite canonical system, Proc 4th International Conference on Term Rewriting Systems, Springer Lecture Notes in Computer Science 488, 423–434Google Scholar
- 15.H. Zantema, Termination of term rewriting by interpretation, Utrecht University technical report RUU-CS-92-14, April 1992Google Scholar