Skip to main content
SpringerLink
Log in

Sufficient conditions for modular termination of conditional term rewriting systems

  • Modularity and Termination
  • Conference paper
  • First Online:
Conditional Term Rewriting Systems (CTRS 1992)

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

Included in the following conference series:

Abstract

Recently we have shown the following abstract result for unconditional term rewriting systems (TRSs). Whenever the disjoint union R 1 ⊕ R 2 of two (finite) terminating TRSs R 1, R 2 is non-terminating, then one of the systems, say R 1, enjoys an interesting property, namely it is not termination preserving under non-deterministic collapses, i.e. R 1 ⊕ {G(x,y) → x,G(x,y)→y is non-terminating, and the other system R 2 is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting. Here we extend this result and derived sufficient criteria for modularity of termination to the case of conditional term rewriting systems (CTRSs). Moreover we relate various definitions of notions related to termination of CTRSs to each other and discuss some subtleties and problems concerning extra variables in the rules.

This research was supported by the ‘Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)’.

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. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, pages 279–301, 1982.

    Google Scholar 

  2. N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

    MathSciNet  Google Scholar 

  3. N. Dershowitz, M. Okada, and G. Sivakumar. Canonical conditional rewrite systems. In E. Lusk and R. Overbeek, editors, Proc. of the 9th Int. Conf. on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 538–549. Springer, 1988.

    Google Scholar 

  4. B. Gramlich. A structural analysis of modular termination of term rewriting systems. SEKI Report SR-91-15, Dept. of Comp. Science, Univ. of Kaiserslautern, 1991.

    Google Scholar 

  5. B. Gramlich. Generalized sufficient conditions for modular termination of rewriting. In Proc. of 3rd Int. Conf. on Algebraic and Logic Programming, Pisa, Italy, Lecture Notes in Computer Science. Springer-Verlag, 1992. to appear.

    Google Scholar 

  6. B. Gramlich. Relating innermost, weak, uniform and modular termination of term rewriting systems. In A. Voronkov, editor, Conference on Logic Programming and Automated Reasoning, St. Petersburg, volume 624 of Lecture Notes in Artificial Intelligence, pages 285–296. Springer-Verlag, 1992.

    Google Scholar 

  7. J.-P. Jouannaud and B. Waldmann. Reductive conditional term rewriting systems. In Proceedings of the 3rd IFIP Working Conference on Formal Description of Programming Concepts, pages 223–244. North-Holland, 1986.

    Google Scholar 

  8. S. Kaplan. Simplifying conditional term rewriting systems: Unification, termination and confluence. Journal of Symbolic Computation, 4:295–334, 1987.

    Google Scholar 

  9. J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I. Oxford University Press, 1990.

    Google Scholar 

  10. M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems. Journal of IPS, Japan, 34:632–642, 1990.

    Google Scholar 

  11. A. Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the 4 th IEEE Symposium on Logic in Computer Science, pages 396–401, Pacific Grove, 1989.

    Google Scholar 

  12. A. Middeldorp. Termination of disjoint unions of conditional term rewriting systems. Technical Report CS-R8959, Centre for Mathematics and Computer Science, Amsterdam, 1989.

    Google Scholar 

  13. A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Centre for Mathematics and Computer Science, Amsterdam, 1990.

    Google Scholar 

  14. A. Middeldorp. Completeness of combinations of conditional constructor systems. Advanced Research Laboratory, Hitachi Ltd., Hatoyama, Japan, draft version, see also this volume, February 1992.

    Google Scholar 

  15. A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In R.V. Book, editor, Proc. of the 4th Int. Conf. on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, pages 174–187. Springer, 1991.

    Google Scholar 

  16. M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26:65–70, 1987.

    Article  Google Scholar 

  17. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, 1987.

    Article  Google Scholar 

  18. Y. Toyama, J.W. Klop, and H.P. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In N. Dershowitz, editor, Proc. of the 3rd Int. Conf. on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 477–491. Springer, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Kaiserslautern, Erwin Schrödinger Straße, W-6750, Kaiserslautern, Germany

    Bernhard Gramlich

Authors
  1. Bernhard Gramlich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michaël Rusinowitch Jean-Luc Rémy

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gramlich, B. (1993). Sufficient conditions for modular termination of conditional term rewriting systems. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-56393-8_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56393-8

  • Online ISBN: 978-3-540-47549-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation