Sequentiality, second order monadic logic and tree automata

Given a term rewriting system R and a normalizable term t, a redex is needed if in any reduction sequence of t to a normal for m, this redex will be contracted. Roughly, R is sequential if there is an optimal reduction strategy in which only needed redexes are contracted. More generally, G. Huet and J.-J. Levy (1991) define the sequentiality of a predicate P on partially evaluated terms. We show that the sequentiality of P is definable in SkS, the second order monadic logic with k: successors, provided P is definable in SkS. We derive several known an new consequences of this remark: strong sequentiality, as defined by Huet and Levy, of a left linear (possibly overlapping) rewrite system is decidable; NV sequentiality, as defined by M. Oyamaguchi (1993), is decidable, even in the case of overlapping rewrite systems; sequentiality of any linear shallow rewrite system is decidable. Then we describe a direct construction of an automaton recognizing the set of terms that have needed redexes, which again, yields immediate consequences: strong sequentiality of possibly overlapping linear rewrite systems is decidable in EXPTIME; for strongly sequential rewrite systems, needed redexes can be read directly on the automaton