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.

Abstract

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

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

BibTeX Entry


@inproceedings{GodoyTiwari05:CSL,
	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