Abstract
A very powerful method for proving the Church-Rosser property for abstract rewriting systems has been developed by van Oostrom. In this paper, his technique is extended in two ways to abstract rewriting modulo an equivalence relation. It is shown that known Church-Rosser theorems can be viewed as special cases of the new criteria. Moreover, applications of the new criteria yield several new results.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus. Reduktionssysteme. Springer Verlag, 1995 (in German).
A. Geser. Relative Termination. PhD thesis, Universität Passau, 1990.
R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964.
G. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. of the ACM 27 (4), pages 797–821, 1980.
J.-P. Jouannaud and H. Kirchner. Completion of a Set of Rules Modulo a Set of Equations. SIAM J. on Computing 15 (4), pages 1155–1194, 1986.
J.-P. Jouannaud and M. Munoz. Termination of a Set of Rules Modulo a Set of Equations. In Proceedings of the 7th International Conference on Automated Deduction, pages 175–193. LNCS 170, 1984.
J.W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, 1992.
E. Ohlebusch. Conditional Graph Rewriting. In Proceedings of the 6th International Conference on Algebraic and Logic Programming, pages 144–158. LNCS 1298, 1997.
V. van Oostrom. Confluence by Decreasing Diagrams. Theoretical Computer Science 126 (2), pages 259–280, 1994.
V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit te Amsterdam, 1994.
R. Pino Pérez and Ch. Even. An Abstract Property of Confluence Applied to the Study of the Lazy Partial Lambda Calculus. In Proceedings of the 3rd International Symposium on Logical Foundations of Computer Science, pages 278–290. LNCS 813, 1994.
B.K. Rosen. Tree-Manipulating Systems and Church-Rosser Theorems. J. of the ACM 20(1), pages 160–187, 1973.
R. Sethi. Testing for the Church-Rosser Property. J. of the ACM 21, pages 671–679, 1974.
J. Staples. Church-Rosser Theorems for Replacement Systems. In J. Crosley, editor, Algebra and Logic, pages 291–307. Lecture Notes in Mathematics 450, 1975.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Ohlebusch, E. (1998). Church-Rosser theorems for abstract reduction modulo an equivalence relation. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052358
Download citation
DOI: https://doi.org/10.1007/BFb0052358
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive