Skip to main content
SpringerLink
Log in
Book cover

International Conference on Rewriting Techniques and Applications

RTA 2001: Rewriting Techniques and Applications pp 108–121Cite as

Termination Proofs by Context-Dependent Interpretations

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2051))

Abstract

Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated.

Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

    Google Scholar 

  2. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9:137–159, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  3. A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In D. Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction CADE-11, volume 607 of Lecture Notes in Artificial Intelligence, pages 139–147. Springer-Verlag, 1992.

    Google Scholar 

  4. A. Cichon and J.-Y. Marion. Light LPO. Technical Report 99-R-138, LORIA, Nancy, France, 1999.

    Google Scholar 

  5. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1-2):69–115, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  6. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–320. Elsevier Science Publishers, 1990.

    Google Scholar 

  7. F. Drewes and C. Lautemann. Incremental termination proofs and the length of derivations. In R.V. Book, editor, Proc. 4th Int. Conf. on Rewriting Techniques and Applications RTA-91, volume 488 of Lecture Notes in Computer Science, pages 49–61. Springer-Verlag, 1991.

    Google Scholar 

  8. R. Fraïssé. Theory of Relations, volume 118 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1986.

    MATH  Google Scholar 

  9. O. Geupel. Terminationsbeweise bei Termersetzungssystemen. Diplomarbeit, Technische Universität Dresden, Sektion Mathematik, 1988.

    Google Scholar 

  10. J. Giesl. Generating polynomial orderings for termination proofs. In J. Hsiang, editor, Proc. 6th Int. Conf. on Rewriting Techniques and Applications RTA-95, volume 914 of Lecture Notes in Computer Science, pages 426–431. Springer-Verlag, 1995.

    Google Scholar 

  11. J. Giesl. POLO–a system for termination proofs using polynomial orderings. Technical Report 95/24, Technische Hochschule Darmstadt, 1995.

    Google Scholar 

  12. D. Hofbauer. Termination proofs and derivation lengths in term rewriting systems. Dissertation, Technische Universität Berlin, Germany, 1991. Available as Technical Report 92-46, TU Berlin, 1992.

    Google Scholar 

  13. D. Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science, 105(1):129–140, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  14. D. Hofbauer. Termination proofs for ground rewrite systems–interpretations and derivational complexity. Mathematische Schriften 24/00, Universität Gh Kassel, Germany, 2000. To appear in Applicable Algebra in Engineering, Communication and Computing.

    Google Scholar 

  15. D. Hofbauer. An upper bound on the derivational complexity of Knuth-Bendix orderings. Mathematische Schriften 28/00, Universität Gh Kassel, Germany, 2000. To appear in Information and Computation.

    Google Scholar 

  16. D. Hofbauer and C. Lautemann. Termination proofs and the length of derivations. In N. Dershowitz, editor, Proc. 3rd Int. Conf. on Rewriting Techniques and Applications RTA-89, volume 355 of Lecture Notes in Computer Science, pages 167–177. Springer-Verlag, 1989.

    Google Scholar 

  17. D. S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, May 1979.

    Google Scholar 

  18. C. Lautemann. A note on polynomial interpretation. Bulletin of the European Association for Theoretical Computer Science, 36:129–131, Oct. 1988.

    MATH  Google Scholar 

  19. I. Lepper. Derivation lengths and order types of Knuth-Bendix orders. Technical report, Westfälische Wilhelms-Universität Münster, Institut für Mathematische Logik und Grundlagenforschung, Germany, May 2000. Available as http://wwwmath.uni-muenster.de/logik/publ/pre/5.html, to appear in Theoretical Computer Science.

    Google Scholar 

  20. P. Lescanne. Termination of rewrite systems by elementary interpretations. Formal Aspects of Computing, 7(1):77–90, 1995.

    Article  MATH  Google Scholar 

  21. Z. Manna and S. Ness. On the termination of Markov algorithms. In Proc. 3rd Hawaii Int. Conf. on System Science, pages 789–792, Honolulu, 1970.

    Google Scholar 

  22. J.-Y. Marion. Analysing the implicit complexity of programs. Technical Report 99-R-106, LORIA, Nancy, France, 1999.

    Google Scholar 

  23. V. C. S. Meeussen and H. Zantema. Derivation lengths in term rewriting from interpretations in the naturals. Technical Report RUU-CS-92-43, Utrecht University, The Netherlands, 1992.

    Google Scholar 

  24. F. L. Morris and C. B. Jones. An early program proof by Alan Turing. Annals of the History of Computing, 6(2):139–143, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  25. J. Steinbach. Termination proofs of rewriting systems–Heuristics for generating polynomial orderings. Technical Report SR-91-14, Fachbereich Informatik, Universität Kaiserslautern, Germany, 1991.

    Google Scholar 

  26. J. Steinbach. Proving polynomials positive. In R. Shyamasundar, editor, Proc. Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 191–202. Springer-Verlag, 1992.

    Google Scholar 

  27. J. Steinbach. Generating polynomial orderings. Information Processing Letters, 49(2):85–93, 1994.

    Article  MATH  Google Scholar 

  28. J. Steinbach and M. Zehnter. Vademecum of polynomial orderings. Technical Report SR-90-03, Fachbereich Informatik, Universität Kaiserslautern, Germany, 1990.

    Google Scholar 

  29. H. Touzet. Propriétées combinatoires pour la terminaison de systèmes de réé ecriture. PhD thesis, Université Henri Poincaré–Nancy 1, France, 1997.

    Google Scholar 

  30. A. M. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, pages 67–69. University Mathematics Lab, Cambridge University, 1949.

    Google Scholar 

  31. W. Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1992.

    MATH  Google Scholar 

  32. A. Weiermann. Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theoretical Computer Science, 139(1-2):355–362, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  33. H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17(1):23–50, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  34. H. Zantema. Termination of term rewriting. Technical Report RUU-CS-2000-04, Utrecht University, The Netherlands, 2000.

    Google Scholar 

  35. H. Zantema. The termination hierarchy for term rewriting. To appear in Applicable Algebra in Engineering, Communication and Computing.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel, Germany

    Dieter Hofbauer

Authors
  1. Dieter Hofbauer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Information Sciences and Electronics, University of Tsukuba, Tsukuba, 305-8573, Japan

    Aart Middeldorp

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hofbauer, D. (2001). Termination Proofs by Context-Dependent Interpretations. In: Middeldorp, A. (eds) Rewriting Techniques and Applications. RTA 2001. Lecture Notes in Computer Science, vol 2051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45127-7_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-45127-7_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42117-7

  • Online ISBN: 978-3-540-45127-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation