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.
Preview
Unable to display preview. Download preview PDF.
References
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.
N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, to appear in: Handbook of Theoretical Computer Science (ed. J. van Leeuwen), North-Holland, 1989.
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.
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.
N. Dershowitz and D.A. Plaisted, Logic Programming cum Applicative Programming, Proceedings of the IEEE Symposium on Logic Programming, Boston, pp. 54–66, 1985.
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.
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.
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.
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.
S. Kaplan, Conditional Rewrite Rules, Theoretical Computer Science 33(2), pp. 175–193, 1984.
S. Kaplan, Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence, Journal of Symbolic Computation 4(3), pp. 295–334, 1987.
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.
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.)
M. Kurihara and A. Ohuchi, Modularity of Simple Termination of Term Rewriting Systems, Journal of IPS Japan 31(5), pp. 633–642. 1990.
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.
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.
A. Middeldorp, Confluence of the Disjoint Union of Conditional Term Rewriting Systems, Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam, 1989.
A. Middeldorp, Termination of Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R8959, Centre for Mathematics and Computer Science, Amsterdam, 1989.
A. Middeldorp, Unique Normal Forms for Disjoint Unions of Conditional Term Rewriting Systems, Report CS-R9003, Centre for Mathematics and Computer Science, Amsterdam, 1990.
A. Middeldorp, Modular Properties of Term Rewriting Systems, Ph.D. thesis, Vrije Universiteit, Amsterdam, 1990.
M. Rusinowitch, On Termination of the Direct Sum of Term Rewriting Systems, Information Processing Letters 26, pp. 65–70, 1987.
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.
Y. Toyama, Counterexamples to Termination for the Direct Sum of Term Rewriting Systems, Information Processing Letters 25, pp. 141–143, 1987.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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