Skip to main content

33 Examples of termination

  • Conference paper
  • First Online:
Term Rewriting (TCS School 1993)

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

Included in the following conference series:

Abstract

A graded sequence of examples—presented in a uniform framework—spotlights stages in the development of methods for proving termination of rewrite systems.

Research supported in part by the U. S. National Science Foundation under Grants CCR-90-07195 and CCR-90-24271.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, to appear.

    Google Scholar 

  2. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.

    Google Scholar 

  3. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.

    Google Scholar 

  4. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.

    Google Scholar 

  5. Nachum Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69–115, February/April 1987. Corrigendum: 4, 3 (December 1987), 409–410; reprinted in Rewriting Techniques and Applications, J.-P. Jouannaud, ed., pp. 69–115, Academic Press, 1987.

    Google Scholar 

  6. Trevor Evans. On multiplicative systems defined by generators and relations, I. Proceedings of the Cambridge Philosophical Society, 47:637–649, 1951.

    Google Scholar 

  7. Saul Gorn. On the conclusive validation of symbol manipulation processes (how do you know it has to work?). J. of the Franklin Institute, 296(6):499–518, December 1973.

    Google Scholar 

  8. R. Iturriaga. Contributions to mechanical mathematics. Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, 1967.

    Google Scholar 

  9. Sam Kamin and Jean-Jacques LĂ©vy. Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980.

    Google Scholar 

  10. Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.

    Google Scholar 

  11. Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer-Verlag, Berlin, pp. 342–376 (1983).

    Google Scholar 

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

    Google Scholar 

  13. R. Lipton and L. Snyder. On the halting of tree replacement systems. In Proceedings of the Conference on Theoretical Computer Science, pages 43–46, Waterloo, Canada, August 1977.

    Google Scholar 

  14. Zohar Manna and Steven Ness. On the termination of Markov algorithms. In Proceedings of the Third Hawaii International Conference on System Science, pages 789–792, Honolulu, HI, January 1970.

    Google Scholar 

  15. David A. Plaisted. Well-founded orderings for proving termination of systems of rewrite rules. Report R-78-932, Department of Computer Science, University of Illinois, Urbana, IL, July 1978.

    Google Scholar 

  16. David A. Plaisted. A recursively defined ordering for proving termination of term rewriting systems. Report R-78-943, Department of Computer Science, University of Illinois, Urbana, IL, September 1978.

    Google Scholar 

  17. David A. Plaisted. Term rewriting systems. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 4, chapter 2. Oxford University Press, Oxford, 1993. To appear.

    Google Scholar 

  18. Hans Zantema. Classifying termination of term rewriting. Technical Report RUU-CS-91-42, Utrecht University, The Netherlands, November 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Hubert Comon Jean-Pierre Jounnaud

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dershowitz, N. (1995). 33 Examples of termination. In: Comon, H., Jounnaud, JP. (eds) Term Rewriting. TCS School 1993. Lecture Notes in Computer Science, vol 909. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59340-3_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-59340-3_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59340-9

  • Online ISBN: 978-3-540-49237-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics