Linear interpretations by counting patterns

  • Ursula Martin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 690)


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.


Function Symbol Coordinate Vector Springer Lecture Note Standard Basis Vector Recursive Decomposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Ben Cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming 9 (1987) 137–160CrossRefMATHMathSciNetGoogle Scholar
  2. 2.
    M. Dauchet, Simulation of Turing machines by a left linear rewrite rule, in Proc 3rd International Conference on Term Rewriting Systems, Springer Lecture Notes in Computer Science 355 (1989) 109–120CrossRefMathSciNetGoogle Scholar
  3. 3.
    N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science 17 (1982) 279–301CrossRefMATHMathSciNetGoogle Scholar
  4. 4.
    N. Dershowitz, Termination of Rewriting, Journal of Symbolic Computation, 3 (1987) 69–116CrossRefMATHMathSciNetGoogle Scholar
  5. 5.
    A. J. J. Dick, J. R. Kalmus and U. Martin, Automating the Knuth Bendix ordering, Acta Informatica 28 (1990) 95–119CrossRefMATHMathSciNetGoogle Scholar
  6. 6.
    G. Higman, Ordering by divisibility in abstract algebras, Proceedings of the London Mathematical Society 2 (1952) 326–336CrossRefMATHMathSciNetGoogle Scholar
  7. 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. 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. 9.
    D. S. Lankford, On proving term rewriting systems are Noetherian, Tech report MTP-3, Louisiana Technical University, Ruston 1979Google Scholar
  10. 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
  11. 11.
    U. Martin, A geometrical approach to multiset orderings, Theoretical computer Science 67 (1989) 37–54CrossRefMATHMathSciNetGoogle Scholar
  12. 12.
    U. Martin, On the diversity of orderings on strings, RHBNC Technical Report 1991Google Scholar
  13. 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
  14. 14.
    J. Steinbach, Extensions and comparison of simplification ordering, in Proc 3rd International Conference on Term Rewriting Systems, Springer Lecture Notes in Computer Science 355 (1989) 434–448CrossRefMathSciNetGoogle Scholar
  15. 15.
    H. Zantema, Termination of term rewriting by interpretation, Utrecht University technical report RUU-CS-92-14, April 1992Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Ursula Martin
    • 1
  1. 1.Department of Mathematical and Computational SciencesUniversity of St AndrewsSt AndrewsScotland

Personalised recommendations