Confluence of Shallow Right-Linear TRSs

Guillem Godoy and Ashish Tiwari

Presented at CSL 2005, Oxford, UK, Aug 22-25, 2005. Springer-Verlag. The final version will appear at the the Springer LNCS site.


We show that confluence of shallow and right-linear term rewriting systems is decidable. This class of rewriting system is expressive enough to include nontrivial nonground rules such as commutativity, identity, and idempotence. Our proof uses the fact that this class of rewrite systems is known to be regularity-preserving, which implies that its reachability and joinability problems are decidable. The new decidability result is obtained by building upon our prior work for the class of ground term rewriting systems and shallow linear term rewriting systems. The proof relies on the concept of extracting more general rewrite derivations from a given rewrite derivation.

pdf. Springer link .


Slides of the presentation at CSL'05 : postscript pdf.

BibTeX Entry

	author = "G. Godoy and A. Tiwari",
	title = "Confluence of Shallow Right-Linear Rewrite Systems",
	booktitle = "Computer Science Logic, 14th Annual Conf., CSL 2005",
	EDITOR = "Ong, L.",
	pages = "541--556",
	series = {LNCS},
	volume = 3634,
	PUBLISHER = {Springer},
	MONTH = aug,
	YEAR = 2005

Return to the Ashish's home page
Return to the Computer Science Laboratory home page