Sequentiality, Second Order Monadic Logic and Tree Automata

Abstract

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 form, 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. Lévy defined in their 1978 paper the sequentiality of a predicate P on partially evaluated terms. We show here 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 and new consequences of this remark: 1-- strong sequentiality, as defined by Huet and Lévy, of a left linear (possibly overlapping) rewrite system is decidable, 2-- NV-sequentiality , as defined by Oyamaguchi, is decidable, even in the case of overlapping rewrite systems 3-- Sequentiality of any linear shallow rewrite system is decidable. Then we describe a direct construction of a tree automaton recognizing the set of terms that do have needed redexes, which, again, yields immediate consequences: 1-- Strong sequentiality of possibly overlapping linear rewrite systems is decidable in EXPTIME, 2-- For strongly sequential rewrite systems, needed redexes can be read directly on the automaton.

paper (.ps version)