Skip to main content
SpringerLink
Log in

On modularity of termination and confluence properties of conditional rewrite systems

  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1994)

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

Included in the following conference series:

Abstract

We investigate the modularity behaviour of termination and confluence properties of conditional term rewriting systems. In particular, we show how to obtain sufficient conditions for the modularity of weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, confluence and completeness of conditional rewrite systems.

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. J. A. Bergstra and J. W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

    Google Scholar 

  2. N. Dershowitz. Hierarchical termination, Department of Computer Science, Hebrew University, Jerusalem, Israel. November 1993.

    Google Scholar 

  3. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, ed., Formal models and semantics, Handbook of Theoretical Computer Science, vol. B, chapter 6, pp. 243–320. Elsevier — The MIT Press, 1990.

    Google Scholar 

  4. N. Dershowitz, M. Okada, and G. Sivakumar. Canonical conditional rewrite systems. In E. Lusk and R. Overbeek, eds., Proc. 9th CADE, LNCS 310, pp. 538–549. Springer, 1988.

    Google Scholar 

  5. N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan and J.-P. Jouannaud, eds., Proc. 1st CTRS, LNCS 308, pp. 31–44. Springer, 1988.

    Google Scholar 

  6. M. Fernandez and J.-P. Jouannaud. Modularity properties of term rewriting systems revisited. Rapport de Recherche 875, LRI, Orsay, France, 1993.

    Google Scholar 

  7. B. Gramlich. Generalized sufficient conditions for modular termination of rewriting. In H. Kirchner and G. Levi, eds., Proc. 3rd ALP, LNCS 632, pp. 53–68. Springer, 1992. Ext. version in AAECC 5:131–158, 1994.

    Google Scholar 

  8. B. Gramlich. Relating innermost, weak, uniform and modular termination of term rewriting systems. In A. Voronkov, editor, 3rd LPAR, St. Petersburg, LNAI 624, pp. 285–296. Springer, 1992.

    Google Scholar 

  9. B. Gramlich. New abstract criteria for termination and confluence of conditional rewrite systems. SEKI-Report SR-93-17, FB Informatik, Universität Kaiserslautern, 1993, ext. abstract to appear in Proc. 4th CTRS, 1994.

    Google Scholar 

  10. B. Gramlich. Relating innermost, weak, uniform and modular termination of term rewriting systems. SEKI-Report SR-93-09, FB Informatik, Universität Kaiserslautern, 1993.

    Google Scholar 

  11. B. Gramlich. Sufficient conditions for modular termination of conditional term rewriting systems. In M. Rusinowitch and J.L. Remy, eds., Proc. 3rd CTRS, Pont-à-Mousson, 1992, LNCS 656, pages 128–142. Springer, 1993.

    Google Scholar 

  12. S. Kaplan. Conditional rewrite rules. TCS, 33:175–193, 1984.

    Google Scholar 

  13. J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, vol. 2, chapter 1, pp. 2–117. Clarendon Press, Oxford, 1992.

    Google Scholar 

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

    Google Scholar 

  15. M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. TCS, 103:273–282, 1992.

    Google Scholar 

  16. M.R.K. Krishna Rao. Completeness of hierarchical combinations of term rewriting systems. In R.K. Shyamasundar, editor, Proc. 13th FSTTCS, LNCS 761, pp. 125–138. Springer, 1993.

    Google Scholar 

  17. M.R.K. Krishna Rao. Simple termination of hierarchical combinations of term rewriting systems. In Proc. TACS, LNCS 789, pp. 203–223, 1994.

    Google Scholar 

  18. A. Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proc. 4th LICS, pp. 396–401, 1989.

    Google Scholar 

  19. A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University, Amsterdam, 1990.

    Google Scholar 

  20. A. Middeldorp. Completeness of combinations of conditional constructor systems. In M. Rusinowitch and J.L. Remy, editors, Proc. 3rd CTRS, July 1992, Pont-à-Mousson, LNCS 656, pp. 82–96. Springer, 1993.

    Google Scholar 

  21. A. Middeldorp. Modular properties of conditional term rewriting systems. Information and Computation, 104(1):110–158, May 1993.

    Google Scholar 

  22. A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In R.V. Book, editor, Proc. 4th RTA, LNCS 488, pp. 174–187. Springer, 1991.

    Google Scholar 

  23. M.J. O'Donnell. Computing in Systems Described by Equations, LNCS 58. Springer, 1977.

    Google Scholar 

  24. E. Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. Technical Report 13, Universität Bielefeld, 1993.

    Google Scholar 

  25. E. Ohlebusch. On the modularity of termination of term rewriting systems. Technical Report 11, Universität Bielefeld, March 1993.

    Google Scholar 

  26. B.K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20:160–187, 1973.

    Google Scholar 

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

    Google Scholar 

  28. 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. 3rd RTA, LNCS 355, pp. 477–491. Springer, 1989.

    Google Scholar 

  29. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, D-67653, Kaiserslautern, Germany

    Bernhard Gramlich

Authors
  1. Bernhard Gramlich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Giorgio Levi Mario Rodríguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag

About this paper

Cite this paper

Gramlich, B. (1994). On modularity of termination and confluence properties of conditional rewrite systems. In: Levi, G., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1994. Lecture Notes in Computer Science, vol 850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58431-5_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-58431-5_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58431-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation