We define a CHR constraint for less-than-or-equal, `leq`

, that can
handle variable arguments. This handler can be found in the
library as the file `leq.pl`

. (The code works regardless of
options switched on or off.)

:- use_module(library(chr)). handler leq. constraints leq/2. :- op(500, xfx, leq). reflexivity @ X leq Y <=> X=Y | true. antisymmetry @ X leq Y , Y leq X <=> X=Y. idempotence @ X leq Y \ X leq Y <=> true. transitivity @ X leq Y , Y leq Z ==> X leq Z.

The CHR specify how `leq`

simplifies and propagates as a
constraint. They implement reflexivity, idempotence, antisymmetry and
transitivity in a straightforward way. CHR `reflexivity`

states
that `X leq Y`

simplifies to `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 a
constraint of the form `A leq A`

we can simplify it to `true`

.

The rule `antisymmetry`

means that if we find `X leq Y`

as well as
`Y leq X`

in the constraint store, 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 reflexivity rule could also have
been written as `reflexivity X leq X <=> true`

.)

The rules `reflexivity`

and `antisymmetry`

are
simplification CHR. In such rules, the constraints found are
removed when the rule applies and fires. The rule `idempotence`

is
a simpagation CHR, only the constraints right of `'\'`

will
be removed. The rule says that if we find `X leq Y`

and another ```
X
leq Y
```

in the constraint store, we can remove one.

Finally, the rule `transitivity`

states that the conjunction
`X leq Y, Y leq Z`

implies `X leq Z`

. Operationally, we add
`X leq Z`

as (redundant) constraint, without removing the
constraints `X leq Y, Y leq Z`

. This kind of CHR is called
propagation CHR.

Propagation CHR are useful, as the query ```
A leq B,C leq A,B
leq C
```

illustrates: The first two constraints cause CHR
`transitivity`

to fire and add `C leq B`

to the
query. This new constraint together with `B leq C`

matches
the head of CHR `antisymmetry`

, `X leq Y, Y leq X`

. So
the two constraints are replaced by `B=C`

. Since `B=C`

makes
`B`

and `C`

equivalent, CHR `antisymmetry`

applies to the
constraints `A leq B, C leq A`

, resulting in `A=B`

. The
query contains no more CHR constraints, the simplification stops.
The constraint handler we built has solved ```
A leq B, C leq A, B leq
C
```

and produced the answer `A=B, B=C`

:

A leq B,C leq A,B leq C. % C leq A, A leq B propagates C leq B by transitivity. % C leq B, B leq C simplifies to B=C by antisymmetry. % A leq B, C leq 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 handler implements a (partial) order constraint over any constraint domain, this generality is only possible with CHR.

As another example, we can implement the sieve of Eratosthenes to
compute primes simply as (for variations see the handler
`primes.pl`

):

:- use_module(library(chr)). handler eratosthenes. constraints primes/1,prime/1. primes(1) <=> true. primes(N) <=> N>1 | M is N-1,prime(N),primes(M). % generate candidates absorb(J) @ prime(I) \ prime(J) <=> J mod I =:= 0 | true.

The constraint `primes(N)`

generates candidates for prime numbers,
`prime(M)`

, where `M`

is between `1`

and `N`

.
The candidates react with each other such that each
number absorbs multiples of itself. In the end, only prime numbers remain.

Looking at the two rules defining `primes/1`

, note that head
matching is used in CHR, so the first rule will only apply to
`primes(1)`

. The test `N>1`

is a guard (precondition) on the
second rule. A call with a free variable, like `primes(X)`

,
will delay (suspend). The third, multi-headed rule `absorb(J)`

reads as follows: If there is a constraint `prime(I)`

and some
other constraint `prime(J)`

such that `J mod I =:= 0`

holds,
i.e. `J`

is a multiple of `I`

, then keep `prime(I)`

but
remove `prime(J)`

and execute the body of the rule,
`true`

.