Skip to main content
SpringerLink
Log in

Confluence of terminating membership conditional TRS

  • Contextual Rewriting and Constrained Rewriting
  • Conference paper
  • First Online:
Conditional Term Rewriting Systems (CTRS 1992)

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

Included in the following conference series:

Abstract

Membership conditional term rewriting systems (MCTRSs) axe term rewriting systems in which applications of rewriting rules are restricted by membership conditions. In this paper, a sufficient condition (the critical pair lemma) for terminating MCTRSs is proposed. To show the condition, the notion of contextual rewriting discussed by Zhang-Rémy is extended and a new technique to divide membership conditions into simpler subconditions is introduced. Furthermore, when membership conditions of MCTRSs are divided into infinite subconditions with some well-founded structures, their confluence are shown by induction on the structures. Finally, a completion algorithm for MCTRSs is proposed on the basis of this sufficient condition and a completion of McCarthy's 91-function is demonstrated.

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. Bergstra, J. and Klop, J.: “Conditional Rewrite Rules”, J. of Comp. and Sys. Sci. 32, pp.323–362 (1986).

    Google Scholar 

  2. Comon, H.: “Equational Formulas in Order Sorted Formulas”, Springer LNCS 443, pp.674–688 (1990).

    Google Scholar 

  3. Comon, H.: “Completion of Rewrite Systems with Membership Conditions”, Springer LNCS 623, pp.392–404 (1992).Draft for full version, May 1992.

    Google Scholar 

  4. Dershowitz, N. and Jouannaud, J.-P.: “Rewrite Systems”, in Handbook of Theoretical Computer Science, Vol.B, N.-Holland (1990).

    Google Scholar 

  5. Gnaedig, I., Kirchner, C. and Kirchner, H.: “Equational Completion in Order Sorted Algebras”, TCS 72, pp. 169–202 (1990).

    Google Scholar 

  6. Huet, G.: “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems”, J. of ACM 27, pp.797–821 (1980).

    Article  Google Scholar 

  7. Huet, G. and Hullot, J.-M.: “Induction in Equational Theories with Constructors”, J. of Comp. and Sys. Sci. 25, pp.239–266 (1982).

    Google Scholar 

  8. Kaplan, S.: “Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence”, J. of Symbolic Computation 4, pp.295–334 (1987).

    Google Scholar 

  9. Kapur, D., Narendran, P. and Zhang, H.: “Proof by Induction Using Test Sets”, Springer LNCS 230, pp.99–117 (1985).

    Google Scholar 

  10. Kirchner, H.: “Schematization of Infinite Sets of Rewrite Rules Generated by Divergent Completion Processes”, TCS 67, pp.303–332 (1989).

    Google Scholar 

  11. Kirchner H. and Hermann, M.: “Meta-rule Synthesis from Crossed Rewrite Systems”, Springer LNCS 516, pp.143–154 (1991).

    Google Scholar 

  12. Knuth, E. and Bendix, B.: “Simple Word Problems in Universal Algebras”, in Computational Problems in Abstract Algebra, ed. J. Leech, pp.263–297, Pergamon Press (1970).

    Google Scholar 

  13. Nutt, W., Smolka, G., Goguen, J., and Meseguer, J.: “Order Sorted Computation”, Proc. the Colloq. on Resolution of Equations in Algebraic Structures (1987).

    Google Scholar 

  14. Thiel, J.-J.: “Stop Losing Sleep over Incomplete Data Type Specification”, Proc. 11th ACM POPL, pp.76–82 (1984).

    Google Scholar 

  15. Toyama, Y.: “Term Rewriting Systems with Membership Conditions”, Springer LNCS 308, pp.228–244 (1988).

    Google Scholar 

  16. Toyama, Y.: “Membership Conditional Term Rewriting Systems”, Trans. IEICEJ, E72, pp.1224–1229 (1989).

    Google Scholar 

  17. Toyama, Y.: “How to Prove Equivalence of Term Rewriting Systems without Induction”, TCS 90(1991), pp. 369–390.

    Google Scholar 

  18. Yamada, J.: “Membership Conditional TRS with Infinite Sets in Conditions”, IPSJ SIG Notes 90-SF-35-6/IEICEJ Tech. Rep. COMP90-6 (1990).

    Google Scholar 

  19. Yamada, J.: “On the Confluence of Terminating Membership Conditional TRS”, IEICEJ Trans. IEICEJ J-74-D-I (1991), pp.666–674, in Japanese.

    Google Scholar 

  20. Yamada, J.: “Membership Conditional TRS with Regular Tree Automata”, ICOT PAR-WG, Feb. 1992.

    Google Scholar 

  21. Yamada, J. and Toyama, Y.: “Confluence of Membership Conditional TRS”, IEICEJ Tech. Rep. COMP89-8/IPSJ SIG Notes 89-SF-28-8 (1989).

    Google Scholar 

  22. Zhang, H. and Rémy, J.-L.: “Contextual Rewriting”, Springer LNCS 202, pp.46–62 (1985).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NTT Research Laboratories, Seika-cho Soraku-gun, 619-02, Kyoto, Japan

    Junnosuke Yamada

Authors
  1. Junnosuke Yamada
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michaël Rusinowitch Jean-Luc Rémy

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yamada, J. (1993). Confluence of terminating membership conditional TRS. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_29

Download citation

  • DOI: https://doi.org/10.1007/3-540-56393-8_29

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation