Conditions for confluence of innermost terminating term rewriting systems

  • Sayaka Ishizuki
  • Michio Oyamaguchi
  • Masahiko SakaiEmail author
Original Paper


This paper presents a counterexample for the open conjecture whether innermost joinability of all critical pairs ensures confluence of innermost terminating term rewriting systems. We then show that innermost joinability of all normalized instances of the critical pairs is a necessary and sufficient condition. Using this condition, we give a decidable sufficient condition for confluence of innermost terminating systems. Finally, we enrich the condition by introducing the notion of left-stable rules. As a corollary, confluence of innermost terminating left-weakly-shallow TRSs is shown to be decidable.


Confluence Innermost termination Term rewriting systems Decidability 

Mathematics Subject Classification




The authors are grateful to Yoshihito Toyama, Aart Middeldorp, Nao Hirokawa, and Takahito Aoto for their useful comments.


  1. 1.
    Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Proceedings of RTA 2009. LNCS, vol. 5595, pp. 93–102 (2009)Google Scholar
  2. 2.
    Aoto, T., Toyama, Y., Uchida, K.: Proving confluence of term rewriting systems via persistency and decreasing diagrams. In: Proceedings of RTA-TLCA 2014, LNCS, vol. 8560, pp. 46–60 (2014)Google Scholar
  3. 3.
    Baeten, J.C.M., Bergstra, J.A., Klop, J.W., Weijland, W.P.: Term-rewriting systems with rule priorities. Theor. Comput. Sci. 67, 283–301 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 243–320. MIT Press, Cambridge (1990)Google Scholar
  5. 5.
    Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58, 3–31 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae 24, 3–23 (1995)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Hirokawa, N., Klein, D.: Saigawa: A confluence tool. In: Proceedings of 1st IWC, p. 49 (2012)Google Scholar
  8. 8.
    Hullot, J.-M.: Canonical forms and unification. In: Proceedings of 5th CADE. LNCS, vol. 87, pp. 318–334 (1980)Google Scholar
  9. 9.
    Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)Google Scholar
  10. 10.
    Mitsuhashi, I., Oyamaguchi, M., Jacquemard, F.: The confluence problem for flat TRSs. In: Proceedings of AISC 2006. LNCS, vol. 4120, pp. 68–81 (2006)Google Scholar
  11. 11.
    Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002)CrossRefzbMATHGoogle Scholar
  12. 12.
    Sakai, M., Okamoto, K., Sakabe, T.: Innermost reductions find all normal forms on right-linear terminating overlay TRSs. In: Proceedings of 3rd WRS. Technical report DSIC-II/14/03, pp. 79–88 (2003)Google Scholar
  13. 13.
    Sakai, M., Oyamaguchi, M., Ogawa, M.: Non-E-Overlapping, weakly shallow, and non-collapsing TRSs are confluent. In: Proceedings of CADE 2015. LNCS, vol. 9195, pp. 111–126 (2015)Google Scholar
  14. 14.
    Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI: a confluence tool. In: Proceedings of CADE 2011. LNCS, vol. 6803, pp. 499–505 (2011)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Sayaka Ishizuki
    • 1
    • 2
  • Michio Oyamaguchi
    • 3
  • Masahiko Sakai
    • 3
    Email author
  1. 1.Graduate School of Information ScienceNagoya UniversityNagoyaJapan
  2. 2.KDDI CorporationTokyoJapan
  3. 3.Graduate School of InformaticsNagoya UniversityNagoyaJapan

Personalised recommendations