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