Logic in Computer Science (LICS 1995)

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

Authors: H. Comon

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{Comon-SequentialitySecond,
    author = 	 {H. Comon},
    title = 	 {Sequentiality, Second-order Monadic Logic and Tree Automata},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {508-517},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }