## 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`.

*Run this example now.
Test-Drive CHR. Run CHR online. Do a demo. Try it out now!*

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