On the Confluence of Linear Shallow Term Rewrite Systems
Guillem Godoy, Ashish Tiwari, and Rakesh Verma
To be presented at
STACS 2003, Berlin, Germany, Feb 27--Mar 01 2003,
© Springer-Verlag.
Short Description
This paper shows that the confluence of shallow linear term rewrite
systems is decidable. This class of rewrite systems properly
includes ground rewrite systems and shallow, linear, and non-sharing
rewrite systems for which confluence was shown to admit polynomial
time decision procedure previously. For example, the commutativity
axiom falls under this class. The decision procedure presented in
this paper is a nontrivial generalization of the polynomial time algorithms
for deciding confluence of ground and restricted non-ground term rewrite
systems presented in~\cite{Tiwari2002LICS,ComonGodoyNieuwenhuis2001FOCS}.
This algorithm has a polynomial time complexity if the maximum arity of
a function symbol in the signature is considered a constant. This paper
also gives {\small EXPTIME}-hardness proofs for reachability and confluence
of shallow term rewrite systems. This shows that the shallow linear
assumptions made in this paper are fairly tight.
Abstract
We show that the confluence of shallow linear term rewrite
systems is decidable. The decision procedure is a
nontrivial generalization of the polynomial time algorithms
for deciding confluence of ground
and restricted non-ground term rewrite systems presented
in~\cite{Tiwari2002LICS,ComonGodoyNieuwenhuis2001FOCS}.
Our algorithm has a polynomial time complexity if the
maximum arity of a function symbol in the
signature is considered a constant.
We also give {\small EXPTIME}-hardness proofs for reachability and
confluence of shallow term rewrite systems.
postscript
pdf (from LNCS website)
BibTeX Entry
@inproceedings{GodoyTiwariVerma03:STACS,
TITLE = "On the Confluence of Linear Shallow Term Rewrite Systems",
AUTHOR = "Godoy, G. and Tiwari, A. and Verma, R.",
BOOKTITLE = {20th Intl. Symposium on Theoretical Aspects of Computer Science STACS 2003},
EDITOR = "Alt, H. and Habib, M.",
YEAR = "2003",
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
PAGES = {85--96},
VOLUME = "2607",
MONTH = feb,
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page