Node:CHR Introductory Examples, Next:, Previous:CHR Introduction, Up:CHR



Introductory Examples

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.