Abstract
We introduce simultaneous critical pairs, which account for simultaneous overlapping of several rewrite rules. Based on this, we introduce a new CR-criterion widely applicable to arbitrary left-linear term rewriting systems. Our result extends the well-known criterion given by Huet (1980), Toyama (1988), and Oostrom (1997) and incomparable with other well-known criteria for left-linear systems.
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
G. Boudol: Computational Semantics of Term Rewriting Systems, In M. Nivat and J.C. Reynolds, eds., Algebraic Method in Semantics, pp.169–236, Cambridge University Press (1985).
N. Dershowitz and J.-P. Jouannaud: Rewrite Systems, In J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol.B, pp.243–320, The MIT Press (1990).
N. Dershowitz, J.-P. Jouannaud, and J. W. Klop: Open Problems in Rewriting, In Proceedings of RTA-91 (LNCS 488), pp.445-456, Springer (1991).
B. Gramlich: Confluence without termination via parallel critical pairs, In Proceedings of CAAP-96 (LNCS 1059), pp.211–225, Springer (1996).
G. Huet: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, JACM, 27, pp.797–821, 1980.
G. Huet and J.J. Lévy: Computations in Orthogonal Rewrite Systems, I and II, In J.-L. Lassez and G. Plotkin, eds., Computational Logic, Essays in Honor of Alan Robinson, pp.396–443, MIT Press, 1991.
J. W. Klop: Term Rewriting Systems, In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds., Handbook of Logic in Computer Science, Vol.2, pp.2–116, Oxford University Press (1992).
J. W. Klop: Combinatory Reduction Systems, Ph.D. Thesis, Rijksuniversiteit Utrecht (1980).
J. W. Klop, V. van Oostrom and F. van Raamsdonk: Combinatory Reduction Systems, Introduction and Survey, TCS 121, pp.279–308 (1993)
A. Martelli and U. Montanari: An Efficient Unification Algorithm, ACM Trans. on Programming languages and Systems, 4, pp.258–282 (1982).
R. Mayr and T. Nipkow: Higher-Order Rewrite Systems and Their Confluence, http://www4. informatik.tu-muenchen.de/nipkow/pubs/hrs.html, To appear in TCS.
A. Middeldorp: Personal Communication (1997).
T. Nipkow: Higher-Order Critical Pairs, In Proceedings of LICS-91, pp.342–349 (1991).
T. Nipkow: Orthogonal Higher-Order Rewrite Systems are Confluent, In Proceedings of TLCA-93 (LNCS 664), pp.306–317 (1993)
V. van Oostrom: Development Closed Critical Pairs, In HOA-95 Selected Papers (LNCS 1074), pp. 185–200 (1995).
V. van Oostrom: Developing Developments, TCS, 175.1, pp.159–181 (1997).
M. Oyamaguchi and Y. Ohta: A New Parallel Closed Condition for Church-Rosser of Left-Linear Term Rewriting Systems, In Proceedings of RTA-91 (LNCS 1232), pp.187–201 (1997).
B. K. Rosen: Tree Manipulating Systems and Church-Rosser Theorems, JACM, 20, pp.160–187 (1973).
Y. Toyama: On the Church-Rosser Property of Term Rewriting Systems (Japanese), Technical Report, 17672, NTT ECL (1981).
Y. Toyama: Commutativity of Term Rewriting Systems, In Fuchi and L. Kott eds., Programming of Future Generation Computer, Vol.11, pp.393–407, North-Holland (1988).
Y. Toyama: Personal Communication (1997).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Okui, S. (1998). Simultaneous critical pairs and Church-Rosser property. 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/BFb0052357
Download citation
DOI: https://doi.org/10.1007/BFb0052357
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