Constraint Handling Rules
Paradigms  Constraint logic, declarative 

Designed by  Thom Frühwirth 
First appeared  1991 
Website  constrainthandlingrules 
Influenced by  
Prolog 
Constraint Handling Rules (CHR) is a declarative, rulebased programming language, introduced in 1991 by Thom Frühwirth at the time with European ComputerIndustry Research Centre (ECRC) in Munich, Germany. Originally intended for constraint programming, CHR finds applications in grammar induction, type systems, abductive reasoning, multiagent systems, natural language processing, compilation, scheduling, spatialtemporal reasoning, testing, and verification.
A CHR program, sometimes called a constraint handler, is a set of rules that maintain a constraint store, a multiset of logical formulas. Execution of rules may add or remove formulas from the store, thus changing the state of the program. The order in which rules "fire" on a given constraint store is nondeterministic, according to its abstract semantics and deterministic (topdown rule application), according to its refined semantics.
Although CHR is Turing complete, it is not commonly used as a programming language in its own right. Rather, it is used to extend a host language with constraints. Prolog is by far the most popular host language and CHR is included in several Prolog implementations, including SICStus and SWIProlog, although CHR implementations also exist for Haskell, Java, C, SQL, and JavaScript. In contrast to Prolog, CHR rules are multiheaded and are executed in a committedchoice manner using a forward chaining algorithm.
Language overview
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 multiset of these terms, called the constraint store. Rules come in three types:
 Simplification rules have the form . When they match the heads and the guards hold, simplification rules may rewrite the heads into the body .
 Propagation rules have the form . These rules add the constraints in the body to the store, without removing the heads.
 Simpagation rules combine simplification and propagation. They are written . For a simpagation rule to fire, the constraint store must match all the rules in the head and the guards must hold true. The constraints before the are kept, as a in a propagation rule; the remaining constraints are removed.
Since simpagation rules subsume simplification and propagation, all CHR rules follow the format
where each of is a conjunction of constraints: and contain CHR constraints, while the guards are builtin. Only one of needs to be nonempty.
The host language must also define builtin constraints over terms. The guards in rules are builtin constraints, so they effectively execute host language code. The builtin 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. When the host language does not support these features, they must be implemented along with CHR.
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 "oneway 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.
Example program
The following CHR program, in Prolog syntax, contains four rules that implement a solver for a lessorequal constraint. The rules are labeled for convenience (labels are optional in CHR).
% X leq Y means variable X is lessorequal 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.
The rules can be read in two ways. In the declarative reading, three of the rules specify the axioms of a partial ordering:
 Reflexivity: X ≤ X
 Antisymmetry: if X ≤ Y and Y ≤ X, then X = Y
 Transitivity: if X ≤ Y and Y ≤ Z, then X ≤ Z
All three rules are implicitly universally quantified (uppercased identifiers are variables in Prolog syntax). The idempotence rule is a tautology from the logical viewpoint, but has a purpose in the second reading of the program.
The second way to read the above is as a computer program for maintaining a constraint store, a collection of facts (constraints) about objects. The constraint store is not part of this program, but must be supplied separately. The rules express the following rules of computation:
 Reflexivity is a simplification rule: it expresses that, if a fact of the form X ≤ X is found in the store, it may be removed.
 Antisymmetry is also a simplification rule, but with two heads. If two facts of the form X ≤ Y and Y ≤ X can be found in the store (with matching X and Y), then they can be replaced with the single fact X = Y. Such an equality constraint is considered built in, and implemented as a unification that is typically handled by the underlying Prolog system.
 Transitivity is a propagation rule. Unlike simplification, it does not remove anything from the constraint store; instead, when facts of the form X ≤ Y and Y ≤ Z (with the same value for Y) are in the store, a third fact X ≤ Z may be added.
 Idempotence, finally, is a simpagation rule, a combined simplification and propagation. When it finds duplicate facts, it removes them from the store. Duplicates may occur because constraint stores are multisets of facts.
Given the query
A leq B, B leq C, C leq A
the following transformations may occur:
Current constraints  Rule applicable to constraints  Conclusion from rule application 

A leq B, B leq C, C leq A 
transitivity  A leq C

A leq B, B leq C, C leq A, A leq C 
antisymmetry  A = C

A leq B, B leq A, A = C 
antisymmetry  A = B

A = B, A = C 
none 
The transitivity rule adds A leq C
. Then, by applying the antisymmetry rule, A leq C
and C leq A
are removed and replaced by A = C
. Now the antisymmetry rule becomes applicable on the first two constraints of the original query. Now all CHR constraints are eliminated, so no further rules can be applied, and the answer A = B, A = C
is returned: CHR has correctly inferred that all three variables must refer to the same object.
Execution of CHR programs
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, but most implementation use a lazy algorithm called LEAPS.
The original specification of CHR's semantics was entirely nondeterministic, but the socalled "refined operation semantics" of Duck et al. removed much of the nondeterminism so that application writers can rely on the order of execution for performance and correctness of their programs.
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:
 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.