## Paper: Sequentiality, Second-order Monadic Logic and Tree Automata (at LICS 1995)

**Hubert Comon-Lundh**

### 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. Levy define 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 an new consequences of this remark: 1-- strong sequentiality, as defined by Huet and Levy, 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.

### BibTeX

@InProceedings{ComonLundh-SequentialitySecond, author = {Hubert Comon-Lundh}, title = {Sequentiality, Second-order Monadic Logic and Tree Automata}, booktitle = {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)}, year = {1995}, month = {June}, pages = {508--517}, location = {San Diego, CA, USA}, publisher = {IEEE Computer Society Press} }