Non-Linear Rewrite Closure and Weak Normalization
- 141 Downloads
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).
KeywordsRewrite closure Term rewriting Weak normalization Tree automata
Unable to display preview. Download preview PDF.
- 1.Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
- 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: www.grappa.univ-lille3.fr/tata (2007). Accessed 12 Oct 2007
- 4.Creus, C., Godoy, G., Massanes, F., Tiwari, A.: Non-linear rewrite closure and weak normalization. In: LICS, pp. 365–374 (2009)Google Scholar
- 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.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.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
- 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.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