Abstract:
|
The confluence property of ground (i.e., variable-free) term rewrite
systems (GTRS) is well-known to be decidable.
This was proved independently in [DTHL87,DHLT90]
and in [Oya87] 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 (see, e.g., [RTA01]).
In [CGN01] we gave the first polynomial-time algorithm for
deciding the confluence of GTRS. Later in [Tiw02] this result was
extended, using abstract congruent closure techniques, to linear-shallow TRS.
Here, we give a new and much simpler proof of the latter result. |