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)