Title :
Non-linear Rewrite Closure and Weak Normalization
Author :
Creus, Carles ; Godoy, Guillem ; Massanes, Francesc ; Tiwari, Ashish
Author_Institution :
Llenguatges i Sistemes Inf. (LSI), Univ. Politec. de Catalunya (UPC), Barcelona, Spain
Abstract :
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 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.
Keywords :
automata theory; decidability; rewriting systems; trees (mathematics); decidability; nonlinear rewrite closure; rewrite closure construction; right-linear right-shallow term rewrite system; tree automata theory; weak normalization; Automata; Computational modeling; Computer science; Equations; Informatics; Large scale integration; Linearity; Logic; rewrite closure; term rewriting; tree automata; weak normalization;
Conference_Titel :
Logic In Computer Science, 2009. LICS '09. 24th Annual IEEE Symposium on
Conference_Location :
Los Angeles, CA
Print_ISBN :
978-0-7695-3746-7
DOI :
10.1109/LICS.2009.9