Confluence and Semantics of Constraint Simplification Rules

by Slim Abdennadher, Thom Frühwirth and Holger Meuss

Institut für Informatik, Ludwig-Maximilians-Universität München, Germany


Constraint Simplification Rules (CSR) is a subset of the Constraint
Handling Rules (CHR) language. CHR is a powerful special-purpose
declarative programming language for writing constraint solvers.  The
CSR subset of CHR forms essentially a committed-choice language
consisting of guarded rules with multiple heads that replace
constraints by simpler ones until they are solved.  This paper gives
declarative and operational semantics as well as soundness and
completeness results for CSR programs.

In this paper, we introduce a notion of confluence for CSR programs.
Confluence is an essential syntactical property of any constraint
solver.  It ensures that the solver will always compute the same
result for a given set of constraints independent of which rules are
applied. It also means that it does not matter for the result in which
order the constraints arrive at the constraint solver.

We give a decidable, sufficient and necessary syntactic condition for
confluence of terminating CSR programs.  Moreover, as  shown
in this paper, confluence of a program implies consistency of its logical
meaning (under a mild restriction).