Classes of Term Rewrite Systems with Polynomial Confluence Problems

摘要

The confluence property of ground (i.e., variable-free) term rewrite systems (TRS) is well known to be decidable. This was proved independently in Dauchet et al. [1987, 1990] and in Oyamaguchi [1987] using tree automata techniques and ground tree transducer techniques (originated from this problem), yielding EXPTIME decision procedures (PSPACE for strings). Since then, and until last year, the optimality of this bound had been a well-known longstanding open question (see, e.g., RTA-LOOP [2001]). In Comon et al. [2001], we gave the first polynomial-time algorithm for deciding the confluence of ground TRS. Later in Tiwari [2002] this result was extended, using abstract congruent closure techniques, to linear shallow TRS, that is, TRS where no variable occurs twice in the same rule nor at depth greater than one. Here, we give a new and much simpler proof of the latter result.