## CHR by example

We define a user-defined constraint for less-than-or-equal, =<, that can handle variable arguments. The implementation will rely on syntactical equality, =, which is assumed to be a predefined (built-in) constraint.

reflexivity @ X=<Y <=> X=Y | true.
antisymmetry @ X=<Y,Y=<X <=> X=Y.
transitivity @ X=<Y,Y=<Z ==> X=<Z.

The CHR specify how =< simplifies and propagates as a constraint. They implement reflexivity, antisymmetry and transitivity in a straightforward way. CHR reflexivity states that X=<Y is logically true, provided it is the case that X=Y. This test forms the (optional) guard of a rule, a precondition on the applicability of the rule. Hence, whenever we see the constraint X=<X we can simplify it to true. CHR antisymmetry means that if we find X=<Y as well as Y=<X in the current constraint, we can replace it by the logically equivalent X=Y. Note the different use of X=Y in the two rules: In the reflexivity rule the equality is a precondition (test) on the rule, while in the antisymmetry rule it is enforced when the rule fires.

The rules reflexivity and antisymmetry are simplification CHR. The rule transitivity propagates constraints. It states that the conjunction X=<Y, Y=<Z implies X=<Z. Operationally, we add logical consequences as a redundant constraint. This kind of CHR is called propagation CHR.

Redundancy from propagation CHR is useful, as the query A=<B,C=<A,B=<C shows: The first two constraints cause CHR transitivity to fire and add C=<B to the query. This new constraint together with B=<C matches the head of CHR antisymmetry, X=<Y,Y=<X. So the two constraints are replaced by B=C. In general, matching takes into account the syntactical equalities that are implied by built-in constraints. Therefore, since the built-in constraint B=C was added, CHR antisymmetry applies to the constraints A=<B,C=<A, resulting in A=B. The query contains no more inequalities, the simplification stops. The constraint solver we built has solved A=<B,C=<A,B=<C and produced the answer A=B,B=C:

A=<B,C=<A,B=<C.
% C=<A,A=<B propagates C=<B by transitivity.
% C=<B,B=<C simplifies to B=C by antisymmetry.
% A=<B,C=<A simplifies to A=B by antisymmetry since B=C.
A=B,B=C.

Note that multiple heads of rules are essential in solving these constraints. Also note that this solver implements a (partial) order constraint over any constraint domain, this generality is only possible with CHR.

For the solver to work, we require conjunctions of constraints to be idempotent, so that multiple occurrences of the same constraint are absorbed. This ensures termination of the solver, since given a finite number of variables, there can only be a finite number of different =< constraints between them. Then, the solver is confluent, this means that from a given query, the answer will always be the same, regardless of which order we apply the rules. E.g. in the above query we could have started with applying transitivity to C=<A,B=<C.

Click on the link above and when there, choose the solver Inequalities between variables (less-than-or-equal).