Termination proofs and the length of derivations

  • Dieter Hofbauer
  • Clemens Lautemann
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


The derivation height of a term t, relative to a set R of rewrite rules, dh R (t), is the length of a longest derivation from t. We investigate in which way certain termination proof methods impose bounds on dh R . In particular we show that, if termination of R can be proved by polynomial interpretation then dh R is bounded from above by a doubly exponential function, whereas termination proofs by Knuth-Bendix ordering are possible even for systems where dh R cannot be bounded by any primitive recursive functions. For both methods, conditions are given which guarantee a singly exponential upper bound on dh R . Moreover, all upper bounds are tight.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [CL87]
    Ahlem Ben Cherifa and Pierre Lescanne, Termination of Rewriting Systems by Polynomial Interpretations and its Implementation. Sci. of Comp. Prog. 9, pp. 137–159.Google Scholar
  2. [De87]
    Nachum Dershowitz, Termination of rewriting. J.Symbolic Computation 3, pp. 69–116.Google Scholar
  3. [DO88]
    Nachum Dershowitz and Mitsuhiro Okada, Proof-theoretic techniques for term rewriting theory. Proc. 3rd Ann. Symp. on Logic in Computer Science, pp. 104–111.Google Scholar
  4. [Ge88]
    Oliver Geupel, Terminationsbeweise bei Termersetzungssystemen. Diplomarbeit, Sektion Mathematik, TU Dresden.Google Scholar
  5. [He78]
    Hans Hermes Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit. 3rd ed., Springer.Google Scholar
  6. [HO80]
    Gérard Huet and Derek Oppen, Equations and rewrite rules: a survey. In Formal languages, perspectives and open problems, ed. Ronald Book, Academic Press.Google Scholar
  7. [KB70]
    Donald E. Knuth and Peter B. Bendix, Simple Word Problems in Universal Algebras. In: J. Leech, Ed., Computational Problems in Abstract Algebra, Oxford, Pergamon Press, pp. 263–297.Google Scholar
  8. [Ln75]
    Dallas Lankford, Canonical algebraic simplification in computational logic. Report ATP-25, University of Texas.Google Scholar
  9. [Ln79]
    Dallas Lankford, On proving term rewriting systems are Noetherian. Report MTP-3, Louisiana Tech University.Google Scholar
  10. [La88]
    Clemens Lautemann, A note on polynomial interpretation. EATCS Bulletin 36, to appear.Google Scholar
  11. [Le86]
    Pierre Lescanne, Divergence of the Knuth-Bendix completion procedure and termination orderings. EATCS Bulletin 30, pp. 80–83.Google Scholar
  12. [Ma87]
    Ursula Martin, How to choose the weights in the Knuth Bendix ordering. Proc. of the Second Int. Conf. on Rewriting Techniques and Applications, LNCS 256, pp. 42–53.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Dieter Hofbauer
    • 1
  • Clemens Lautemann
    • 2
  1. 1.Technische Universität BerlinGermany
  2. 2.Universität BremenGermany

Personalised recommendations