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
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;
Conference_Titel :
Foundations of Computer Science, 2001. Proceedings. 42nd IEEE Symposium on
Print_ISBN :
0-7695-1116-3
DOI :
10.1109/SFCS.2001.959904