Skip to main content
SpringerLink
Log in

Simultaneous critical pairs and Church-Rosser property

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1998)

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

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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).

    Google Scholar 

  2. 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).

    Google Scholar 

  3. 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).

    Google Scholar 

  4. B. Gramlich: Confluence without termination via parallel critical pairs, In Proceedings of CAAP-96 (LNCS 1059), pp.211–225, Springer (1996).

    Google Scholar 

  5. G. Huet: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, JACM, 27, pp.797–821, 1980.

    Article  MathSciNet  MATH  Google Scholar 

  6. 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.

    Google Scholar 

  7. 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).

    Google Scholar 

  8. J. W. Klop: Combinatory Reduction Systems, Ph.D. Thesis, Rijksuniversiteit Utrecht (1980).

    Google Scholar 

  9. J. W. Klop, V. van Oostrom and F. van Raamsdonk: Combinatory Reduction Systems, Introduction and Survey, TCS 121, pp.279–308 (1993)

    Article  MATH  Google Scholar 

  10. A. Martelli and U. Montanari: An Efficient Unification Algorithm, ACM Trans. on Programming languages and Systems, 4, pp.258–282 (1982).

    Article  MATH  Google Scholar 

  11. 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.

    Google Scholar 

  12. A. Middeldorp: Personal Communication (1997).

    Google Scholar 

  13. T. Nipkow: Higher-Order Critical Pairs, In Proceedings of LICS-91, pp.342–349 (1991).

    Google Scholar 

  14. T. Nipkow: Orthogonal Higher-Order Rewrite Systems are Confluent, In Proceedings of TLCA-93 (LNCS 664), pp.306–317 (1993)

    MathSciNet  Google Scholar 

  15. V. van Oostrom: Development Closed Critical Pairs, In HOA-95 Selected Papers (LNCS 1074), pp. 185–200 (1995).

    Google Scholar 

  16. V. van Oostrom: Developing Developments, TCS, 175.1, pp.159–181 (1997).

    Article  MATH  Google Scholar 

  17. 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).

    MathSciNet  Google Scholar 

  18. B. K. Rosen: Tree Manipulating Systems and Church-Rosser Theorems, JACM, 20, pp.160–187 (1973).

    Article  MATH  Google Scholar 

  19. Y. Toyama: On the Church-Rosser Property of Term Rewriting Systems (Japanese), Technical Report, 17672, NTT ECL (1981).

    Google Scholar 

  20. 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).

    Google Scholar 

  21. Y. Toyama: Personal Communication (1997).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Engineering Faculty of Engineering, Mie University, 514, Tsu, Japan

    Satoshi Okui

Authors
  1. Satoshi Okui
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Tobias Nipkow

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation