Skip to main content
SpringerLink
Log in

A complete characterization of termination of 0p 1q→1r 0s

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1995)

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

Included in the following conference series:

Abstract

We characterize termination of one-rule string rewriting systems of the form 0p 1q → 1r 0s for every choice of positive integers p, q, r, and s. For the simply terminating cases, we give the precise complexity of derivation lengths.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Leo Bachmair and Nachum Dershowitz. Commutation, transformation, and termination. In 8th Int. Conf. Automated Deduction, pages 5–20. Springer LNCS 230, 1985.

    Google Scholar 

  2. Françoise Bellegarde and Pierre Lescanne. Transformation ordering. In 2nd TAP-SOFT, pages 69–80. Springer LNCS 249, 1987.

    Google Scholar 

  3. Françoise Bellegarde and Pierre Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication, and Computing, 1:79–96, 1990.

    Google Scholar 

  4. Ronald Book and Friedrich Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer, New York, 1993.

    Google Scholar 

  5. Max Dauchet. Simulation of turing machines by a left-linear rewrite rule. In Proc. 3rd Int. Conf. Rewriting Techniques and Applications, pages 109–120. LNCS 355, 1989.

    Google Scholar 

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

    Article  Google Scholar 

  7. Nachum Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69–115, Feb./April 1987. Corrigendum: 4, 3, Dec. 1987, 409–410.

    Google Scholar 

  8. Nachum Dershowitz and Charles Hoot. Topics in termination. In Claude Kirchner, editor, 5th Int. Conf. Rewriting Techniques and Applications, pages 198–212. Springer LNCS 690, 1993.

    Google Scholar 

  9. Maria C. F. Ferreira and Hans Zantema. Dummy elimination: Making termination easier. Technical Report UU-CS-1994-47, Utrecht University, October 1994. Available via ftp.cs.ruu.nl/pub/RUU/CS/techreps/CS-1994.

    Google Scholar 

  10. Alfons Geser. Relative termination. Dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany, 1990. Also available as: Report 91-03, Ulmer Informatik-Berichte, Universität Ulm, 1991.

    Google Scholar 

  11. Alfons Geser. A solution to Zantema's problem. In Rudolf Berghammer and Gunther Schmidt, editors, Proc. coll. “Programmiersprachen und Grundlagen der Programmierung”, pages 88–96, Bericht Nr. 9309, Univ. der Bundeswehr, Neubiberg, Germany, December 1993. Also appeared as report MIP-9314, Universität Passau, Germany, December 1993.

    Google Scholar 

  12. Gérard Huet and Dallas Lankford. On the uniform halting problem for term rewriting systems. Technical Report 283, INRIA, 1978.

    Google Scholar 

  13. Matthias Jantzen. Confluent string rewriting, volume 14 of EATCS Monographs on Theoretical Computer Science. Springer, Berlin, 1988.

    Google Scholar 

  14. Dallas S. Lankford. On proving term rewriting systems are noetherian. Technical Report MTP-3, Louisiana Technical University, Math. Dept., Ruston, LA, 1979.

    Google Scholar 

  15. Robert McNaughton. The uniform halting problem for one-rule Semi-Thue Systems. Technical Report 94-18, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY, August 1994.

    Google Scholar 

  16. Vincent Meeussen and Hans Zantema. Derivation lengths in term rewriting from interpretations in the naturals. In H. A. Wijshoff, editor, Computing Science in the Netherlands, pages 249–260, November 1993. Also appeared as report RUU-CS-92-43, Utrecht University.

    Google Scholar 

  17. Elias Tahhan-Bittar. Non-erasing, right-linear orthogonal term rewrite systems, application to Zantema's problem. Technical Report RR2202, INRIA, France, 1994.

    Google Scholar 

  18. Hans Zantema. Termination of rewriting by semantic labelling. Technical Report RUU-CS-92-38, Utrecht University, December 1992. Extended and revised version appeared as RUU-CS-93-24, July 1993, accepted for special issue on term rewriting of Fundamenta Informaticae.

    Google Scholar 

  19. Hans Zantema. Termination of term rewriting: interpretation and type elimination. J. Symbolic Computation, 17:23–50, 1994.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universiteit Utrecht, P.O. Box 80089, NL-3508, Utrecht, The Netherlands

    Hans Zantema

  2. Lehrstuhl für Programmiersysteme, Universität Passau, D-94030, Passau, Germany

    Alfons Geser

Authors
  1. Hans Zantema
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alfons Geser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jieh Hsiang

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zantema, H., Geser, A. (1995). A complete characterization of termination of 0p 1q→1r 0s . In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_46

Download citation

  • DOI: https://doi.org/10.1007/3-540-59200-8_46

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59200-6

  • Online ISBN: 978-3-540-49223-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation