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.