Confluence of Shallow Right-Linear Rewrite Systems

  • Guillem Godoy
  • Ashish Tiwari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We show that confluence of shallow and right-linear term rewriting systems is decidable. This class of rewriting system is expressive enough to include nontrivial nonground rules such as commutativity, identity, and idempotence. Our proof uses the fact that this class of rewrite systems is known to be regularity-preserving, which implies that its reachability and joinability problems are decidable. The new decidability result is obtained by building upon our prior work for the class of ground term rewriting systems and shallow linear term rewriting systems. The proof relies on the concept of extracting more general rewrite derivations from a given rewrite derivation.


Induction Hypothesis Congruence Relation Ground Term Tree Automaton Joinability Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Computation 4, 217–247 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Bouajjani, A.: Languages, rewriting systems, and verification of infinite-state systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 24–39. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on
  4. 4.
    Comon, H., Haberstrau, M., Jouannaud, J.-P.: Syntacticness, cyclesyntacticness, and shallow theories. Information and Computation 111(1), 154–191 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Amsterdam. Formal Models and Semantics, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)Google Scholar
  6. 6.
    Giesl, J., Zantema, H.: Liveness in rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 321–336. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Godoy, G., Tiwari, A.: Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 91–106. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 85–96. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Godoy, G., Tiwari, A., Verma, R.: Deciding confluence of certain term rewriting systems in polynomial time. Annals of Pure and Applied Logic 130(1-3), 33–59 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Jacquemard, F.: Reachability and confluence are undecidable for flat term rewriting systems. Inf. Process. Lett. 87(5), 265–270 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Proc. 11th IEEE Symp. on Logic In Comp. Sc. LICS, pp. 473–483. IEEE Computer Society, Los Alamitos (1996)CrossRefGoogle Scholar
  13. 13.
    Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 246–260. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Guillem Godoy
    • 1
  • Ashish Tiwari
    • 2
  1. 1.Technical University of CataloniaBarcelonaSpain
  2. 2.SRI InternationalMenlo ParkUSA

Personalised recommendations