On the Church-Rosser property for the direct sum of term rewriting systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

On the Church-Rosser property for the direct sum of term rewriting systems

Full text

Pdf (906 KB)

Source

Journal of the ACM (JACM) archive
Volume 34 , Issue 1 (January 1987) table of contents

Pages: 128 - 143

Year of Publication: 1987

ISSN:0004-5411

Author

Yoshihito Toyama

NTT Electrical Communication Labs, Tokyo, Japan

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 32, Citation Count: 6

Additional Information:

abstract references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/7531.7534 What is a DOI?

ABSTRACT

The direct sum of two term rewriting systems is the union of systems having disjoint sets of function symbols. It is shown that if two term rewriting systems both have the Chruch-Rosser property, then the direct sum of these systems also has this property.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	BARENDREGT, H. P. The Lambda Calculus, Its Syntax and Semantics. North-Holland, Amsterdam, 1981.
	2	Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
	3	KLOP, J.W. Combinatory reduction systems, Dissertation, Univ. of Utrecht, The Netherlands, 1980.
	4	Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
	5	Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]
	6	STAPLES, J. Church-Rosser Theorem for Replacement Systems. Lecture Notes in Mathematics 450, Springer-Verlag, New York, 1975, pp. 291-307.
	7	TOVAMA, Y. On commutativity of term rewriting systems. Trans. IECE Japan J66-D, 12 (1983), 1370-1375 (in Japanese).

CITED BY 6

	M. Okada, Strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.357-363, July 17-19, 1989, Portland, Oregon, United States
	Bernhard Gramlich , Salvador Lucas, Modular termination of context-sensitive rewriting, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.50-61, October 06-08, 2002, Pittsburgh, PA, USA
	Y. Toyama , J. W. Klop , H. P. Barendregt, Termination for direct sums of left-linear complete term rewriting systems, Journal of the ACM (JACM), v.42 n.6, p.1275-1304, Nov. 1995
	Jakob Grue Simonsen, On modularity in infinitary term rewriting, Information and Computation, v.204 n.6, p.957-988, June 2006
	Anderson Santana de Oliveira, Rewriting-Based Access Control Policies, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.4, p.59-72, July, 2007
	Rakesh M. Verma, Unique normal forms and confluence of rewrite systems: persistence, Proceedings of the 14th international joint conference on Artificial intelligence, p.362-368, August 20-25, 1995, Montreal, Quebec, Canada