On Confluence of Constraint Handling Rules
by Slim Abdennadher, Thom Frühwirth and Holger Meuss
Computer Science Department, University of Munich
Oettingenstr. 67, 80538 Munich, Germany
Abstract
We introduce the notion of confluence for Constraint Handling Rules
(chr), a powerful language for writing constraint solvers. With chr
one simplifies and solves constraints by applying rules. Confluence
guarantees that a chr program will always compute the same result for
a given set of constraints independent of which rules are applied. We
give a decidable, sufficient and necessary syntactic condition for
confluence.
Confluence turns out to be an essential syntactical property of
chr programs for two reasons. First, confluence implies correctness
(as will be shown in this paper). In a correct chr program,
application of chr rules preserves logical equivalence of
the simplified constraints.
Secondly, even when the program is already correct, confluence is
highly desirable. Otherwise, given some constraints, one
computation may detect their inconsistency while another one may
just simplify them into a still complex constraint.
As a side-effect, the paper also gives soundness and completeness
results for chr programs. Due to their special nature, and in
particular correctness, these theorems are stronger than what holds
for the related families of (concurrent) constraint programming
languages.