Constraint Handling Rules: Propagation Instead of Search

I have been looking at relational programming, where a query searches for substitutions that satisfy a relation. Constraint Handling Rules takes a different approach. It keeps a multiset of constraints and repeatedly applies guarded rewrite rules to that store. By default it does not search over alternatives; it commits to a rule and continues. That changes both the programming model and the failure modes.

The name sounds narrower than the language is. CHR began as a way to add user-defined constraint solvers to a host language. It became a general-purpose rule language, used for type systems, testing and verification, scheduling, and classic algorithms ^[2]. It is usually embedded in Prolog, Haskell, Java, or C, but it is not a small add-on. It is a full computational model.

This post is a first pass at that model, and at what it means for relational computation.

The language, by example

Suppose you know three things:

• A is less than or equal to B.
• B is less than or equal to C.
• C is less than or equal to A.

What follows? All three must be equal. A cycle of ≤ forces equality at every edge. That is the kind of conclusion CHR is designed to derive.

In CHR, each fact is a constraint: leq(A,B), leq(B,C), leq(C,A). The engine keeps the current constraints in a multiset called the store. The store starts with those three constraints.

A CHR rule is a pattern that says how to change the store. It has a head, an optional guard, and a body. The head matches one or more constraints in the store. The guard is a condition written in the host language. If the head matches and the guard succeeds, the rule fires and its body updates the store.

The leq program uses four rules:

reflexivity  @ leq(X,X) <=> true.
antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
idempotence  @ leq(X,Y) \ leq(X,Y) <=> true.
transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).

Read transitivity first. Its head matches two constraints: leq(X,Y) and leq(Y,Z). If both are in the store, the rule adds leq(X,Z). The original two constraints stay. That is a propagation rule: it adds a consequence.

reflexivity is a simplification rule. If the store contains leq(X,X), the rule replaces it with true, which removes it. The constraint says nothing useful.

antisymmetry is also a simplification rule, but it matches two constraints. If the store contains both leq(X,Y) and leq(Y,X), the rule removes both and adds X = Y. The host language handles the equality.

idempotence is a simpagation rule. It matches two copies of the same constraint. The copy before the backslash is kept; the copy after it is removed. This is why the store is a multiset, not a set: duplicate constraints can exist, and the rule can remove one while keeping the other.

Now run the example. Start with:

leq(A,B), leq(B,C), leq(C,A)

One derivation goes like this. transitivity fires on leq(B,C) and leq(C,A), adding leq(B,A). The store is now:

leq(A,B), leq(B,C), leq(C,A), leq(B,A)

antisymmetry matches leq(A,B) and leq(B,A). It removes both and adds A = B. The equality rewrites the remaining leq(B,C) to leq(A,C). The store is now:

leq(A,C), leq(C,A), A = B

antisymmetry matches leq(A,C) and leq(C,A). It removes both and adds A = C. The final store is:

A = B, A = C

The cycle of inequalities has been reduced to equalities. No rule applies to the equalities, so the derivation stops.

That is the basic shape of CHR. The program is a set of local rules. The engine keeps applying rules until no rule applies—or continues indefinitely if the program does not terminate. The rules are declarative, but the derivation is operational.

Once a rule fires, the engine commits. It does not backtrack over the choice of rule. If the guard fails, it tries the next rule. If no rule applies, the constraint is suspended ^[3].

That commitment is the first big difference from a search-based relational engine. A search-based engine explores alternatives and may expose multiple answers. CHR instead commits to a rewrite and continues.

What the rules mean

The rules have a logical reading ^[1][2]. For the leq program, it is easy to state:

• reflexivity says leq(X,X) is equivalent to true.
• antisymmetry says leq(X,Y) and leq(Y,X) together are equivalent to X = Y.
• transitivity says leq(X,Y) and leq(Y,Z) imply leq(X,Z).

That is the declarative meaning. It is what the rules say, independent of the order in which the engine applies them.

idempotence shows where the logical reading and the operational reading start to separate. Logically, a duplicate leq(X,Y) adds nothing; the truth is already there. Operationally, the store is a multiset, so the duplicate exists as a separate constraint. The rule removes one copy and keeps the other. The logic sees redundancy; the engine sees a multiset.

That gap matters. The logical reading tells you what the rules mean. The operational semantics tells you how the store changes. They are related, but they are not the same. A rule can be logically true and still produce a bad derivation if it loops or if the rule set is not confluent. Confluence means the final store does not depend on the order in which rules are applied; without it, two rule orders can end in different stores.

How it runs

The previous section described the rules. This section describes what the engine does with them.

Start again with the store leq(A,B), leq(B,C), leq(C,A). The engine does not apply all rules at once. It picks a constraint, makes it active, and tries the rules in order. The other constraints in the store are passive: they can be partners if a rule needs more than one constraint in its head.

Suppose leq(B,C) is active. reflexivity fails because the two arguments differ. antisymmetry looks for leq(C,B); it is not there. idempotence looks for a duplicate leq(B,C); there is none. transitivity looks for a constraint of the form leq(C,Z) or leq(X,B). It finds leq(C,A), so the rule fires and adds leq(B,A). The original leq(B,C) and leq(C,A) stay in the store.

That is one step. The new leq(B,A) becomes active, and the engine repeats the process. It tries the rules in order, finds a partner if needed, checks the guard, and either fires a rule or suspends the constraint. When a rule fires, its body is executed immediately. The engine commits to the rule application: it does not undo that choice through backtracking. If the active constraint remains in the store, it may later resume and try subsequent rule occurrences.

If no rule applies, the constraint is suspended. It stays in the store and can be used as a passive partner for another active constraint. If a variable inside it becomes bound later, the constraint is reactivated and the rules are tried again. That is how a constraint can become relevant after it was suspended.

The engine's state is more than the constraint store. It also has a goal, which is the constraints that have not been introduced yet; a built-in store, which holds host constraints such as A = B; and a propagation history. The propagation history records which rule has already fired on which constraints. Without it, a propagation rule like transitivity could fire on the same constraints repeatedly and add the same consequence forever. The history prevents that specific loop. It does not guarantee termination in general.

The theoretical semantics lets any applicable rule fire. The refined semantics used by most implementations fixes an order: a new constraint becomes active, rules are tried in program order, and matching partners are taken from the suspended store ^[2][3]. That makes behavior predictable, but it also means rule order is part of the program's operational behavior. The declarative reading is order-independent: it is a set of logical formulas with no notion of which rule fires first ^[1][2]. The implementation is not, and CHR programs can rely on that order for correctness or complexity ^[2].

The costs

The first cost is confluence. If the final store can depend on rule order, the program is not confluent, and different valid derivations may produce different results. That is the central correctness question, and it is not automatic.

The second is termination. Simplification rules remove constraints, so a ranking function can sometimes prove termination. Propagation rules add constraints without removing them, which makes termination harder. The propagation history prevents trivial loops, but it does not guarantee termination ^[2].

The third is complexity. Multi-headed rules have to match several constraints at once. Guards have to be checked. The store has to be updated. The number of rule applications is the first-order cost, but the matching cost can dominate. CHR has a body of work on complexity analysis, but there is no free lunch.

The fourth is composition. Composition just means putting two independently written rule sets in the same store and letting them interact. The rules are local, but confluence and termination are properties of the whole program. Two rule sets can each be confluent and terminating on their own and still misbehave when combined. A minimal example:

% rule set A
p(X) ==> q(X).

% rule set B
q(X) ==> p(X).

On its own, rule set A terminates: it adds q from p and stops. On its own, rule set B terminates: it adds p from q and stops. Put them in the same store and they loop. p adds q, q adds p, and each new constraint has a new identity, so the propagation history does not recognize it as the same constraint and the cycle continues.

Composition can also break confluence. If two rule sets simplify the same constraint differently, the final store depends on which rule fires first. Sneyers et al. discuss this as a separate problem: rule sets that are confluent and terminating alone can lose those properties when combined, and preserving termination is especially hard ^[2]. That is the composition cost.

The hard part is not writing a rule. It is predicting what happens when rules interact.

What CHR gets right

CHR treats constraints as partial information. A constraint in the store is not a function call waiting for arguments. It is a condition that may be simplified, combined, or propagated. That is close to the relational picture: the store is a shared body of partial knowledge, and the rules are local ways of drawing consequences.

The rules are compositional in form. Each rule is a small pattern; if execution terminates, the engine reaches a fixed point where no rule applies. That is a clean picture of computation as local rewriting.

CHR also shows that a rule-based constraint language can be practical without a search tree. The cost moves to confluence, termination, matching, and rule order. That is a different engineering problem from search in relational computation more generally, and it is worth studying on its own terms.

Finally, CHR shows the value of a host language. It borrows data types, arithmetic, and equality from the host. That is why the core can stay small. CHR pushes the idea further: the host provides the built-in constraint solver, and CHR provides the user-defined rules.

CHR is also unexpectedly general. It is Turing-complete, but that is the weaker claim. Turing completeness says a language can compute anything computable; it says nothing about cost. Sneyers et al. report a stronger result: complexity-wise completeness. For every RAM algorithm that uses at least as much time as space, there is a CHR program that, in the K.U.Leuven CHR system, runs within a constant factor of the original time and space complexity ^[2][4]. Roughly: for ordinary algorithms whose running time is at least as large as their memory use, CHR can match their asymptotic cost.

That is a stronger claim than it sounds. It means CHR is not just expressive; it can simulate ordinary algorithms without an asymptotic penalty. The multiset-rewriting style does not inherently cost an extra factor of time or space. The constants may be large, and the CHR program may be elaborate, but the model itself is not asymptotically handicapped. That is a remarkable result for a language built on local rewrite rules. It also changes the question: the hard part is not whether a rule-based constraint language can be efficient in principle, but whether a particular program and implementation can realize that efficiency in practice.

What it leaves open

The first open question is search. CHR is committed-choice. It does not explore alternatives by default. If a problem needs search, the host language or an extension has to provide it. Can propagation and search coexist without giving up the declarative reading?

The second is composition. Local rules do not guarantee global properties. Can confluence and termination be checked incrementally as rule sets are composed? Or is composition always a global analysis problem?

The third is the relationship between the logical and operational readings. CHR has both, and they are not the same. Which one is the specification? The answer depends on what you are building: a solver, a type checker, or a general-purpose system.

These are the questions I want to pursue. CHR is a mature model of rule-based constraint computation: rules propagate and simplify a shared store instead of searching a space of substitutions. The price is confluence, termination, and committed choice.

This is exploratory, not a claim that CHR is the right model. The value is in the contrast. CHR shows a different way to organize computation and cost, and that contrast is useful even if the final design looks like neither CHR nor a search-based relational language.

The interesting thing is not that one model is better. It is that they put control in different places: a search-based relational engine explores alternatives; CHR commits to a rule and rewrites the store. A compositional system has to decide which kind of control it wants.

References

1. Frühwirth, T. (1998). Theory and Practice of Constraint Handling Rules. Journal of Logic Programming, 37(1–3), 95–138.
2. Sneyers, J., Van Weert, P., Schrijvers, T., and De Koninck, L. (2010). As Time Goes By: Constraint Handling Rules. Theory and Practice of Logic Programming, 10(1), 1–47.
3. SWI-Prolog. CHR Syntax and Semantics.
4. Sneyers, J., Schrijvers, T., and Demoen, B. (2009). The Computational Power and Complexity of Constraint Handling Rules. ACM Transactions on Programming Languages and Systems, 31(2).