Skip to main content

Termination of rewriting is undecidable in the one-rvle case

  • Communications
  • Conference paper
  • First Online:
Book cover Mathematical Foundations of Computer Science 1988 (MFCS 1988)

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

Abstract

It is well known that it is undecidable whether a term rewriting system is terminating. We prove in this paper that the property remains undecidable if the system has only one rule.

The preparation of this paper was supported in part by the "GRECO de Programmation" and the PRC "Kathématiques et Informatique".

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. R.V. Book, Thue Systems as Rewriting Systems, in: J.P. Jouannaud, ed., Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France. Springer Lec. Notes Comp. Sci.202 (1985) 63–94. Revised version: J. Symbolic Computation, 3 (1987) 39–68.

    Google Scholar 

  2. N. Dershowitz, Termination, in: J.P. Jouannaud, ed., Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France. Springer Lec. Notes Comp. Sci.202 (1985) 180–224. Revised version: Termination of rewiting. J. Symbolic Computation, 3 (1987) 69–116.

    Google Scholar 

  3. J.V. Guttag, D. Kapur and D.R. Musser, On proving uniform termination and restricted termination of rewriting systems. SIAM J. Comput.12 (1983) 187–214.

    Google Scholar 

  4. G. Huet, D.S. Lankfork, On the uniform halting problem for term rewriting systems, Rapport Laboria 283 (1978), INRIA, Le Chesnay, France.

    Google Scholar 

  5. G. Huet and D.C. Oppen, Equations and rewrite rules: A survey, in: R.V. Book, ed., Formal Language Theory: Perspectives and Open Problems, 1980, pp. 349–405. New York: Academic Press.

    Google Scholar 

  6. J.P. Jouannaud, Editorial of J. Symbolic Computation, 3, 1–2, 1987, 1–2.

    Google Scholar 

  7. R. Lipton and L. Snyder, On the halting of tree replacement systems. Proceedings of the Conference on Theoretical Computer Science, University of Waterloo, Waterloo, Canada, (1977), 43–46.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Michal P. Chytil Václav Koubek Ladislav Janiga

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dauchet, M. (1988). Termination of rewriting is undecidable in the one-rvle case. In: Chytil, M.P., Koubek, V., Janiga, L. (eds) Mathematical Foundations of Computer Science 1988. MFCS 1988. Lecture Notes in Computer Science, vol 324. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017149

Download citation

  • DOI: https://doi.org/10.1007/BFb0017149

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45926-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics