• DocumentCode
    1710975
  • Title

    The confluence of ground term rewrite systems is decidable in polynomial time

  • Author

    Comon, Hubert ; Godoy, Guillem ; Nieuwenhuis, Robert

  • Author_Institution
    Stanford Univ., Cachan, France
  • fYear
    2001
  • Firstpage
    298
  • Lastpage
    307
  • Abstract
    The confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently by M. Dauchet et al. (1987; 1990) and by M. Oyamaguchi (1987) using tree automata techniques and ground tree transducer techniques (originated from this problem), yielding EXPTIME decision procedures (PSPACE for strings). Since then, it has been a well-known longstanding open question whether this bound is optimal. The authors give a polynomial-time algorithm for deciding the confluence of GTRS, and hence alsofor the particular case of suffix- and prefix string rewrite systems or Thue systems. We show that this bound is optimal for all these problems by proving PTIME-hardness for the string case. This result may have some impact on other areas of formal language theory, and in particular on the theory of tree automata.
  • Keywords
    automata theory; computational complexity; decidability; optimisation; rewriting systems; theorem proving; trees (mathematics); EXPTIME decision procedures; GTRS; PSPACE; PTIME-hardness; Thue systems; confluence property; decidability; formal language theory; ground term rewrite systems; ground tree transducer techniques; polynomial time; prefix string rewrite systems; suffix-string rewrite systems; tree automata techniques; Algebra; Automata; Computer languages; Computer science; Formal languages; Polynomials; Transducers;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Foundations of Computer Science, 2001. Proceedings. 42nd IEEE Symposium on
  • Print_ISBN
    0-7695-1116-3
  • Type

    conf

  • DOI
    10.1109/SFCS.2001.959904
  • Filename
    959904