Journal of Automated Reasoning

, Volume 51, Issue 3, pp 281–324 | Cite as

Non-Linear Rewrite Closure and Weak Normalization

  • Carles Creus
  • Guillem Godoy
  • Francesc Massanes
  • Ashish Tiwari


A rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. Rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. This property has been useful for proving decidability results in term rewriting. Unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). The left-hand side term is unrestricted, and in particular, it may be non-linear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that right-shallow right-linear term rewrite systems are regularity preserving. Moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. A preliminary version of this work was presented at LICS 2009 (Creus 2009).


Rewrite closure Term rewriting Weak normalization Tree automata 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  2. 2.
    Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. Available on: (2007). Accessed 12 Oct 2007
  3. 3.
    Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Inf. Comput. 187(1), 123–153 (2003)MathSciNetCrossRefMATHGoogle Scholar
  4. 4.
    Creus, C., Godoy, G., Massanes, F., Tiwari, A.: Non-linear rewrite closure and weak normalization. In: LICS, pp. 365–374 (2009)Google Scholar
  5. 5.
    Dauchet, M., Caron, A.C., Coquidé, J.L.: Automata for reduction properties solving. J. Symb. Comput. 20(2), 215–233 (1995)CrossRefMATHGoogle Scholar
  6. 6.
    Godoy, G., Huntingford, E., Tiwari, A.: Termination of rewriting with right-flat rules. In: Rewriting Techniques and Applications (RTA), pp. 200–213. Springer, Paris (2007)Google Scholar
  7. 7.
    Godoy, G., Tison, S.: On the normalization and unique normalization properties of term rewrite systems. In: Conference on Automated Deduction (CADE), pp. 247–262. Springer, Bremen (2007)Google Scholar
  8. 8.
    Godoy, G., Tiwari, A.: Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure. In: International Joint Conference on Automated Reasoning (IJCAR), pp. 91–106. Springer, Cork (2004)Google Scholar
  9. 9.
    Godoy, G., Tiwari, A.: Confluence of shallow right-linear rewrite systems. In: Computer Science Logic (CSL), pp. 541–556. Springer, Oxford (2005)CrossRefGoogle Scholar
  10. 10.
    Godoy, G., Tiwari, A., Verma, R.: Characterizing confluence by rewrite closure and right ground term rewrite systems. Appl. Algebra Eng. Commun. Comput. 15(1), 13–36 (2004)MathSciNetCrossRefMATHGoogle Scholar
  11. 11.
    Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. Inf. Comput. 178(2), 499–514 (2002)MathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Rewriting Techniques and Applications (RTA), pp. 246–260. Springer, Norwich (2000)CrossRefGoogle Scholar
  13. 13.
    Uchiyama, K., Sakai, M., Sakabe, T.: Decidability of termination and innermost termination for term rewriting systems with right-shallow dependency pairs. IEICE Trans. 93-D(5), 953–962 (2010)Google Scholar
  14. 14.
    Wang, Y., Sakai, M.: Decidability of termination for semi-constructor TRSs, left-linear shallow TRSs and related systems. In: Rewriting Techniques and Applications (RTA), pp. 343–356. Springer, Seattle (2006)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2012

Authors and Affiliations

  • Carles Creus
    • 1
  • Guillem Godoy
    • 1
  • Francesc Massanes
    • 1
  • Ashish Tiwari
    • 2
  1. 1.Universitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.SRI InternationalMenlo ParkUSA

Personalised recommendations