Characterizing confluence by rewrite closure and right ground term rewrite systems

Guillem Godoy, Ashish Tiwari, and Rakesh Verma

Applicable Algebra in Engineering, Communication and Computing, AAECC, Publisher: Springer-Verlag, Issue: Volume 15, Number 1, June 2004, pp 13-36. © Springer-Verlag. The final version will appear at the Springer AAECC journal website .

Abstract

Abstract. Just as saturation under an appropriate superposition calculus leads to a convergent presentation of a given equational theory, saturation under a suitable chaining calculus gives, what we call, a rewrite closure. We present a theorem that characterizes confluence of (possibly nonterminating) term rewrite systems that admit a rewrite closure presentation, in terms of local confluence of a related terminating term rewrite system and joinability inclusion between these two rewrite systems. Using constraints to avoid variable chaining, we obtain a finite and computable rewrite closure presentation for right ground systems. This gives an alternate method to decide the reachability and joinability properties for right ground systems. The characterization of confluence, combined with the rewrite closure presentation, is used to obtain a decision procedure for confluence of right ground systems (this problem has been open for quite some time [8]), and a simple decision procedure for the unification problem of confluent right ground systems (result recently obtained in [17). An EXPTIME-hardness result is also proved for reachability and confluence of right ground systems.

Keywords Terms, Rewriting, Confluence

Article presently not online. Send me an email.

BibTeX Entry


@article{GodoyTiwariVerma:AAECC,
	TITLE = {Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems},
	AUTHOR = {Godoy, G. and Tiwari, A. and Verma, R.},
	journal = {Applicable Algebra in Engineering, Communication and Computing},
	volume = 15,
	number = 1,
	year = 2004,
	pages = "13--36",
	month = jun,
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page