Skip to main content

Confluence of the disjoint union of conditional term rewriting systems

  • Chapter 4 Combined Systems, Combined Languages And Modularity
  • Conference paper
  • First Online:
Conditional and Typed Rewriting Systems (CTRS 1990)

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

Included in the following conference series:

Abstract

Toyama proved that confluence is a modular property of term rewriting systems. This means that the disjoint union of two confluent term rewriting systems is again confluent. In this paper we extend his result to the class of conditional term rewriting systems. In view of the important role of conditional rewriting in equational logic programming, this result may be of relevance in integrating functional programming and logic programming.

Note: Research partially supported by ESPRIT BRA project nr. 3020, Integration.

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. J.A. Bergstra and J.W. Klop, Conditional Rewrite Rules: Confluence and Termination, Journal of Computer and System Sciences 32(3), pp. 323–362, 1986.

    Google Scholar 

  2. N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, to appear in: Handbook of Theoretical Computer Science (ed. J. van Leeuwen), North-Holland, 1989.

    Google Scholar 

  3. N. Dershowitz, M. Okada and G. Sivakumar, Confluence of Conditional Rewrite Systems, Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, Orsay, Lecture Notes in Computer Science 308, pp. 31–44, 1987.

    Google Scholar 

  4. N. Dershowitz, M. Okada and G. Sivakumar, Canonical Conditional Rewrite Systems, Proceedings of the 9th Conference on Automated Deduction, Argonne, Lecture Notes in Computer Science 310, pp. 538–549, 1988.

    Google Scholar 

  5. N. Dershowitz and D.A. Plaisted, Logic Programming cum Applicative Programming, Proceedings of the IEEE Symposium on Logic Programming, Boston, pp. 54–66, 1985.

    Google Scholar 

  6. N. Dershowitz and D.A. Plaisted, Equational Programming, in: Machine Intelligence 11 (eds. J.E. Hayes, D. Michie and J. Richards), Oxford University Press, pp. 21–56, 1987.

    Google Scholar 

  7. L. Fribourg, SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting, Proceedings of the IEEE Symposium on Logic Programming, Boston, pp. 172–184, 1985.

    Google Scholar 

  8. J.A. Goguen and J. Meseguer, EQLOG: Equality, Types and Generic Modules for Logic Programming, in: Logic Programming: Functions, Relations and Equations (eds. D. DeGroot and G. Lindstrom), Prentice-Hall, pp. 295–363, 1986.

    Google Scholar 

  9. J.-P. Jouannaud and B. Waldmann, Reductive Conditional Term Rewriting Systems, Proceedings of the 3rd IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, pp. 223–244, 1986.

    Google Scholar 

  10. S. Kaplan, Conditional Rewrite Rules, Theoretical Computer Science 33(2), pp. 175–193, 1984.

    Google Scholar 

  11. S. Kaplan, Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence, Journal of Symbolic Computation 4(3), pp. 295–334, 1987.

    Google Scholar 

  12. J.W. Klop, Term Rewriting Systems, to appear in: Handbook of Logic in Computer Science, Vol. I (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, 1989.

    Google Scholar 

  13. M. Kurihara and I. Kaji, Modular Term Rewriting Systems: Termination, Confluence and Strategies, Report, Hokkaido University, Sapporo, 1988. (Abridged version: Modular Term Rewriting Systems and the Termination, Information Processing Letters 34, pp. 1–4, 1990.)

    Google Scholar 

  14. M. Kurihara and A. Ohuchi, Modularity of Simple Termination of Term Rewriting Systems, Journal of IPS Japan 31(5), pp. 633–642. 1990.

    Google Scholar 

  15. A. Middeldorp, Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, Lecture Notes in Computer Science 355, pp. 263–277, 1989.

    Google Scholar 

  16. A. Middeldorp, A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems, Proceedings of the 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, pp. 396–401, 1989.

    Google Scholar 

  17. A. Middeldorp, Confluence of the Disjoint Union of Conditional Term Rewriting Systems, Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam, 1989.

    Google Scholar 

  18. A. Middeldorp, Termination of Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R8959, Centre for Mathematics and Computer Science, Amsterdam, 1989.

    Google Scholar 

  19. A. Middeldorp, Unique Normal Forms for Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R9003, Centre for Mathematics and Computer Science, Amsterdam, 1990.

    Google Scholar 

  20. A. Middeldorp, Modular Properties of Term Rewriting Systems, Ph.D. thesis, Vrije Universiteit, Amsterdam, 1990.

    Google Scholar 

  21. M. Rusinowitch, On Termination of the Direct Sum of Term Rewriting Systems, Information Processing Letters 26, pp. 65–70, 1987.

    Google Scholar 

  22. Y. Toyama, On the Church-Rosser Property for the Direct Sum of Term Rewriting Systems, Journal of the ACM 34(1), pp. 128–143, 1987.

    Google Scholar 

  23. Y. Toyama, Counterexamples to Termination for the Direct Sum of Term Rewriting Systems, Information Processing Letters 25, pp. 141–143, 1987.

    Google Scholar 

  24. Y. Toyama, J.W. Klop and H.P. Barendregt, Termination for the Direct Sum of Left-Linear Term Rewriting Systems (preliminary draft), Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill, Lecture Notes in Computer Science 355, pp. 477–491, 1989.

    Google Scholar 

  25. H. Zhang and J.L. Rémy, Contextual Rewriting, Proceedings of the 1st International Conference on Rewriting Techniques and Applications, Dijon, Lecture Notes in Computer Science 202, pp. 46–62, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

S. Kaplan M. Okada

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Middeldorp, A. (1991). Confluence of the disjoint union of conditional term rewriting systems. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_99

Download citation

  • DOI: https://doi.org/10.1007/3-540-54317-1_99

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics