Constraint Handling Rules

The concrete syntax of CHR programs depends on the host language, and in fact programs embed statements in the host language that are executed to handle some rules. The host language supplies a data structure for representing terms, including logical variables. Terms represent constraints, which can be thought of as "facts" about the program's problem domain. Traditionally, Prolog is used as the host language, so its data structures and variables are used. The rest of this section uses a neutral, mathematical notation that is common in the CHR literature.

A CHR program, then, consists of rules that manipulate a multi-set of these terms, called the constraint store. Rules come in three types:[5]

• Simplification rules have the form ${\displaystyle h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$. When they match the heads ${\displaystyle h_{1},\dots ,h_{n}}$ and the guards ${\displaystyle g_{1},\dots ,g_{m}}$ hold, simplification rules may rewrite the heads into the body ${\displaystyle b_{1},\dots ,b_{o}}$.
• Propagation rules have the form ${\displaystyle h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$. These rules add the constraints in the body to the store, without removing the heads.
• Simpagation rules combine simplification and propagation. They are written ${\displaystyle h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$. For a simpagation rule to fire, the constraint store must match all the rules in the head and the guards must hold true. The ${\displaystyle \ell }$ constraints before the ${\displaystyle \backslash }$ are kept, as a in a propagation rule; the remaining ${\displaystyle n-\ell }$ constraints are removed.

Since simpagation rules subsume simplification and propagation, all CHR rules follow the format

${\displaystyle H_{k}\,\backslash \,H_{r}\Longleftrightarrow G\,|\,B}$

where each of ${\displaystyle H_{k},H_{r},G,B}$ is a conjunction of constraints: ${\displaystyle H_{k},H_{r}}$ and ${\displaystyle B}$ contain CHR constraints, while the guards ${\displaystyle G}$ are built-in. Only one of ${\displaystyle H_{k},H_{r}}$ needs to be non-empty.

The host language must also define built-in constraints over terms. The guards in rules are built-in constraints, so they effectively execute host language code. The built-in constraint theory must include at least true (the constraint that always holds), fail (the constraint that never holds, and is used to signal failure) and equality of terms, i.e., unification.[7] When the host language does not support these features, they must be implemented along with CHR.[9]

Execution of a CHR program starts with an initial constraint store. The program then proceeds by matching rules against the store and applying them, until either no more rules match (success) or the fail constraint is derived. In the former case, the constraint store can be read off by a host language program to look for facts of interest. Matching is defined as "one-way unification": it binds variables only on one side of the equation. Pattern matching can be easily implemented when as unification when the host language supports it.[9]

 % X leq Y means variable X is less-or-equal to variable Y 
 reflexivity  @ X leq X <=> true.
 antisymmetry @ X leq Y, Y leq X <=> X = Y.
 transitivity @ X leq Y, Y leq Z ==> X leq Z.
 idempotence  @ X leq Y \ X leq Y <=> true.

A leq B, B leq C, C leq A

To decide which rule should "fire" on a given constraint store, a CHR implementation must use some pattern matching algorithm. Candidate algorithms include RETE and TREAT,[12] but most implementation use a lazy algorithm called LEAPS.[13]

The original specification of CHR's semantics was entirely non-deterministic, but the so-called "refined operation semantics" of Duck et al. removed much of the non-determinism so that application writers can rely on the order of execution for performance and correctness of their programs.[5][14]

Most applications of CHRs require that the rewriting process be confluent; otherwise the results of searching for a satisfying assignment will be nondeterministic and unpredictable. Establishing confluence is usually done by way of the following three properties:[2]

• A CHR program is locally confluent if all its critical pairs are joinable.
• A CHR program is called terminating if there are no infinite computations.
• A terminating CHR program is confluent if all its critical pairs are joinable.

• Constraint programming
• Constraint logic programming
• Logic programming
• Production system (computer science)
• Business rules engines
• Rewriting

• Christiansen, Henning. "CHR grammars." Theory and Practice of Logic Programming 5.4-5 (2005): 467-501.

• Official website
• CHR Bibliography
• The CHR mailing list
• The K.U.Leuven CHR System
• WebCHR: a CHR web interface