Skip to main content
Springer Nature Link
Log in

Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems

  • Published:
Applicable Algebra in Engineering, Communication and Computing Aims and scope

Abstract.

Just as saturation under an appropriate superposition calculus leads to a convergent presentation of a given equational theory, saturation under a suitable chaining calculus gives, what we call, a rewrite closure. We present a theorem that characterizes confluence of (possibly nonterminating) term rewrite systems that admit a rewrite closure presentation, in terms of local confluence of a related terminating term rewrite system and joinability inclusion between these two rewrite systems. Using constraints to avoid variable chaining, we obtain a finite and computable rewrite closure presentation for right ground systems. This gives an alternate method to decide the reachability and joinability properties for right ground systems. The characterization of confluence, combined with the rewrite closure presentation, is used to obtain a decision procedure for confluence of right ground systems (this problem has been open for quite some time [8]), and a simple decision procedure for the unification problem of confluent right ground systems (result recently obtained in [17). An EXPTIME-hardness result is also proved for reachability and confluence of right ground systems.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (France)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bachmair, L.: Canonical Equational Proofs. Birkhäuser, Boston, 1991

  2. Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: 9th Annual IEEE Symposium on Logic in Computer Science, 1994, pp. 384–393

  3. Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: Conference on Automated Deduction CADE ‘2000, David McAllester, (ed.), Springer-Verlag, Pittsburgh, PA, Jun 2000, pp. 64–78 LNAI 1831

  4. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. Available at urlhttp://www.grappa.univ-lille3.fr/tata, 1997

  5. Comon, H., Godoy, G., Nieuwenhuis, R.: The confluence of ground term rewrite systems is decidable in polynomial time. In: 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS), Las Vegas Nevada, USA, 2001, pp. 298–307

  6. Dauchet, M., Tison, S., Heuillard, T., Lescanne, P.: Decidability of the confluence of ground term rewriting systems. In: Proceedings Symposium on Logic in Computer Science, Ithaca, New York, 22–25 Jun 1987, pp. 353–359. The computer society of the IEEE

  7. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science Volume B: Formal Models and Sematics (B), van Leeuwen, J., (ed.), MIT press/Elsevier, 1990, pp. 243–320

  8. Dershowitz, N., Treinen, R.: The RTA list of open problems: Open Problem Number 63. http://www.lsv.ens-cachan.fr/rtaloop/problems/63.html

  9. Ganzinger, H., Jacquemard, F., Veanes, M.: Rigid Reachability: The Non-Symmetric Form of Rigid E-Unification. Intl. J. Foundat. Comput. Sci. 11(1), 3–27 (2000)

    Google Scholar 

  10. Godoy, G., Nieuwenhuis, R., Tiwari, A.: Classes of term rewrite systems with polynomial confluence problems. ACM Transactions on Computational Logic (TOCL), 2004. To appear

  11. Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: 20th Intl. Symposium on Theoretical Aspects of Computer Science STACS 2003, Alt, H., (ed.), 2607, Springer, LNCS, Feb 2003, 85–96

  12. Hullot, J-M.: Canonical forms and unification. In: Fifth International Conference on Automated Deduction (CADE), R. Kowalski, (ed.), LNCS bf 87, Les Arcs France, Springer-Verlag, Jul 1980, pp. 318–334

  13. Levy, A., Agusti, J.: Bi-rewriting a term rewriting technique for monotoneorder relations. In: Rewriting Techniques and Applications RTA-93, Kirchner, C., (ed.), 1993, pp. 17–31 LNCS 690

  14. Mitra, S.: Semantic unification for convergent systems. PhD thesis,University of Illinois at Urbana-Champaign, 1994

  15. Mitsuhashi, I., Oyamaguchi, M., Ohta, Y., Yamada, T.: On the unification problem for confluent monadic term rewriting systems. IPSJ Trans. Program. 44(4), 54–66 (2003)

    Google Scholar 

  16. Oyamaguchi, M.: On the word problem for right-ground term-rewriting systems Trans. IEICE E73-5, 718–723 (1990)

    Google Scholar 

  17. Oyamaguchi, M., Ohta, Y.: The unification problem for confluent right-ground term rewriting systems. In: Rewriting Techniques and Applications 12th Intl Conf RTA 2001, Aart Middeldorp, (ed.), LNCS, 2051, Springer, 2001, pp. 246–260

  18. Oyamaguchi, M.: The reachability and joinability problems for right-ground term-rewriting systems. Inf. Proc. 347–354 (1990)

  19. Tiwari, A.: Rewrite closure for ground and cancellative AC theories. In: Conference on Foundations of Software Technology and Theoretical Computer Science FST & TCS ‘2001, Hariharan, R., Vinay, V., (eds.), Bangalore, India, Springer-Verlag, 2001, pp. 334–346 LNCS 2245

  20. Tiwari, A.: Deciding confluence of certain term rewriting systems in polynomial time. In: IEEE Symposium on Logic in Computer Science LICS 2002, Gordon Plotkin, (ed.), IEEE Society, Jul 2002, pp. 447–456

  21. Rakesh, M.: Verma algorithms and reductions for rewriting problems. II. Inf. Proc. Lett. 84(4), 227–233 (2002)

    Google Scholar 

  22. Verma, R.M., Rusinowitch, M., Lugiez, D.: Algorithms and reductions for rewriting problems. Fundamenta Informaticae 43(3), 257–276 (2001). Also in Proc. of Int’l Conf. on Rewriting Techniques and Applications 1998

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Catalonia, Jordi Girona 1, Barcelona, Spain

    Guillem Godoy

  2. SRI International, Menlo Park, CA 94025, USA

    Ashish Tiwari

  3. Computer Science Dept, Univ of Houston, TX 77204, USA

    Rakesh Verma

Authors
  1. Guillem Godoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rakesh Verma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Guillem Godoy.

Additional information

Research of the first author was supported in part by the Spanish CICYT project MAVERISH ref.TIC2001-2476-C03-01.Research of the second author was supported in part by NSF grant CCR-ITR-0326540. Research of the third author was supported in part by NSF grants CCR-0306475 and DUE-0313880.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Godoy, G., Tiwari, A. & Verma, R. Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems. AAECC 15, 13–36 (2004). https://doi.org/10.1007/s00200-004-0148-6

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00200-004-0148-6

Keywords

Search

Navigation