Skip to main content
SpringerLink
Log in

Confluent term rewriting systems with membership conditions

  • Part 1 Research Articles
  • Conference paper
  • First Online:
Conditional Term Rewriting Systems (CTRS 1987)

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

Included in the following conference series:

Abstract

We propose a new type of conditional term rewriting system: the membership-conditional term rewriting system, in which, each rewriting rule can have membership conditions which restrict the substitution values for the variables occurring in the rule. For example, the rule f(x, x, y) ▹ g(x, y) if x ∈ T' yields the reduction f(M, M, N) → g(M, N) only when M is in the term set T'. Thus, by using membership-conditional rewriting, we can easily provide a strategy for term reduction. We study the confluence of membership-conditional term rewriting systems that are nonterminating and nonlinear. It is shown that a restricted nonlinear term rewriting system in which membership conditions satisfy the closure and termination properties is confluent if the system is nonoverlapping.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H.P. Barendregt, The lambda calculus, its syntax and semantics, (North-Holland, 1981).

    Google Scholar 

  2. J.A. Bergstra and J.W. Klop, Conditional rewrite rules: confluence and termination, J. Comput. and Syst. Sci. 32 (1986) 323–362.

    Google Scholar 

  3. G. Huet, Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM 27 (1980) 797–821.

    Article  Google Scholar 

  4. G. Huet and D.C. Oppen, Equations and rewrite rules: a survey, in: R.V. Book, ed., Formal languages: perspectives and open problems, (Academic Press, 1980) 349–405.

    Google Scholar 

  5. J.-P. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. COMPUT. 15 (1986) 1155–1194.

    Article  Google Scholar 

  6. S. Kaplan, Conditional rewrite rules, Theoretical Comput. Sci. 33 (1984) 175–193.

    Google Scholar 

  7. J.W. Klop, Combinatory reduction systems, Dissertation, Univ. of Utrecht, 1980.

    Google Scholar 

  8. D.E. Knuth and P.G. Bendix, Simple word problems in universal algebras, in: J. Leech, ed., Computational problems in abstract algebra (Pergamon Press, 1970) 263–297.

    Google Scholar 

  9. B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, J. ACM 20 (1973) 160–187.

    Article  Google Scholar 

  10. Y. Toyama, On the Church-Rosser property for the direct sum of term rewriting systems, J. ACM 34 (1987) 128–143.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NTT Basic Research Laboratories, 3-9-11 Midori-cho, Musashino-shi, 180, Tokyo, Japan

    Yoshihito Toyama

Authors
  1. Yoshihito Toyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Kaplan J. -P. Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Toyama, Y. (1988). Confluent term rewriting systems with membership conditions. In: Kaplan, S., Jouannaud, J.P. (eds) Conditional Term Rewriting Systems. CTRS 1987. Lecture Notes in Computer Science, vol 308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19242-5_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-19242-5_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19242-8

  • Online ISBN: 978-3-540-39166-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation