Classes of term rewrite systems with polynomial confluence problems
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/97487
Tipus de documentReport de recerca
Data publicació2002-06-06
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
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.
CitacióGodoy, G., Nieuwenhuis, R. "Classes of term rewrite systems with polynomial confluence problems". 2002.
Forma partLSI-02-45-R
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
R02-45.ps | 127,9Kb | Postscript | Visualitza/Obre |