Abstract
In a seminal paper, Huet introduced abstract properties of term rewriting systems, and the confluence analysis of terminating term rewriting systems by critical pairs computation. In this paper, we provide an abstract notion of critical pair for arbitrary binary relations and context operators. We show how this notion applies to the confluence analysis of various transition systems, ranging from classical term rewriting systems to production rules with constraints and partial control strategies, such as the Constraint Handling Rules language CHR. Interestingly, we show in all these cases that some classical critical pairs can be disregarded. The crux of these analyses is the ability to compute critical pairs between states built with general context operators, on which a bounded, not necessarily well-founded, ordering is assumed.

URL:
http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2007-111

BibTeX:

@inproceedings{REWERSE-RP-2007-111,
	author = {R\'{e}my Haemmerl\'{e} and Fran\c{c}ois Fages},
	title = {Abstract Critical Pairs and Confluence of Arbitrary Binary Relations},
	booktitle = {Proceedings of 18th International Conference on Rewriting Techniques and Applications, Paris, France (26th--28th June 2007)},
	year = {2007},
	volume = {4533},
	series = {LNCS},
	pages = {214--228},
	url = {http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2007-111}
}