Constraint Handling Rules in SWI Prolog: Does the "constraint store" exists only for the duration of the toplevel goal processing?

Question

I am taking a closer look at Constraint Handling Rules (CHR) to see if I can understand them (in the sense what's being computed here and how does classical logic and even linear logic fit into this) and possibly apply them.

Thom Frühwirth's book from 2009 discusses principles of CHR, but implementations may of course differ.

In this case, I'm using the SWI Prolog implementation of CHR.

If I understand well:

1. An implementation of CHR would provide at least one "constraint store" to express "the state of the computation". The constraint store contains only ground atoms (i.e. positive literals).
2. In a typical CHR session, one first set up the constraint store with an initial state. One writes the CHR program, containing CHR rules. One then runs the CHR program with the constraint store as parameter. Repeated application of the forward-chaining CHR rules until no rules are applicable any longer will iteratively (and destructively) transform the constraint store from its initial state to some final state. The constraint store can then be examined to find the desired answer.
3. In this scenario, only don't care non-determinism ("committed choice non-determinism") is considered: when several rules apply at any intermediate state, any is taken.
4. The "don't know" non-determinism with backtracking to the choice point in case of later failure is not considered - it is left to the implementation to provide this in one manner or the other, if so desired.

Just as an exercise, a most simple program to compute the GCD using Euclid's Algorithm and retain a log of the operations:

% Constraint `logg(Ti,Msg)` retains the log message `Msg` at step `Ti`
% (which increases monotonically)
% Constraint `gcdpool(X)` denotes a "GCD pool member". At each step, we want
% to compute the GCD of all the X for which there is a `gcdpool(X)` constraint
% in the constraint store. A CHR transformation of the store always reduces the
% sum of the X (variant) while keeping the GCD of the GCD pool members constant
% (invariant). We will thus find a solution eventually.

:- module(my_gcd, [  gcdpool/1, logg/2 ]).
:- use_module(library(chr)).

:- chr_constraint gcdpool/1, logg/2.

% pool contains duplicate: drop one! 

gcdpool(N) \ gcdpool(N),logg(Ti,Msg) <=> To is Ti+1, logg(To,[[drop,[N,N],[N]]|Msg]).

% pool contains 1 and anything not 1: keep only 1

gcdpool(1) \ gcdpool(N),logg(Ti,Msg) <=> 1<N | To is Ti+1, logg(To,[[drop,[1,N],[N]]|Msg]).

% otherwise

gcdpool(N) \ gcdpool(M),logg(Ti,Msg) <=> 0<N, N<M | To is Ti+1, 
                                                    V is M-N, 
                                                    gcdpool(V), 
                                                    logg(To,[[diff,[N,M],[N,V]]|Msg]).

This is all very straightforward. A test run in SWI Prolog

?- use_module(library(chr)).
?- [gcd].
?- chr_trace.
% now we enter a goal:
?- gcdpool(6),gcdpool(3),logg(0,[]).
CHR:   (0) Insert: gcdpool(6) # <907>
CHR:   (1) Call: gcdpool(6) # <907> ? [creep]
CHR:   (1) Exit: gcdpool(6) # <907> ? [creep]
CHR:   (0) Insert: gcdpool(3) # <908>
CHR:   (1) Call: gcdpool(3) # <908> ? [creep]
CHR:   (1) Exit: gcdpool(3) # <908> ? [creep]
CHR:   (0) Insert: logg(0,[]) # <909>
CHR:   (1) Call: logg(0,[]) # <909> ? [creep]
CHR:   (1) Try: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]).
CHR:   (1) Apply: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]). ? [creep]
CHR:   (1) Remove: gcdpool(6) # <907>
CHR:   (1) Remove: logg(0,[]) # <909>
CHR:   (1) Insert: gcdpool(3) # <910>
CHR:   (2) Call: gcdpool(3) # <910> ? [creep]
CHR:   (2) Exit: gcdpool(3) # <910> ? [creep]
CHR:   (1) Insert: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Call: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (2) Try: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]).
CHR:   (2) Apply: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]). ? [creep]
CHR:   (2) Remove: gcdpool(3) # <910>
CHR:   (2) Remove: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Insert: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912>
CHR:   (3) Call: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (3) Exit: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (2) Exit: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (1) Exit: logg(0,[]) # <909> ? [creep]

gcdpool(3),
logg(2, [[drop, [3, 3], [3]], [diff, [3, 6], [3, 3]]]) .

The answer is given by the last two lines: The only constraint left in the constraint store is gcdpool(3), so 3 is the answer.

Implementation-wise the following the following seems to hold:

There is no dedicated "constraint store". The CHR program is (somehow) compiled into Prolog, and a "CHR constraint" becomes a "Prolog predicate". The "constraint store" as such is the stack of the called Prolog toplevel goal (it is not reified).

Thus the "constraint store" is initialized with the constraints listed in the "CHR goal", and disappears on final exit. You also cannot set up the constraint store in a stepwise or interactive manner, but must do in one line:

gcdpool(6),gcdpool(3),logg(0,[]).

After which the CHR program immediately starts its work.

Indeed, the predicate find_chr_constraint/1, which is supposed to get data out of a constraint store, returns nothing once the CHR program has run. Because there is no constraint store anymore.

Moreover, trying to set up a constraint store in the "CHR program" itself makes no sense. Thus putting logg(0,[]) into the GCD code has no effect. You have to put logg(0,[]) into the CHR goal.

Question

• Is that understanding correct?
• How do I get results of CHR computation back into Prolog?
• What's the deal with the possibility of backtracking provided by the Prolog implementation? How do I put it to use for CHR?

Answer 1

In regards to "How do I get results of CHR computation back into Prolog?".

You can do something like:

:- chr_constraint item/1, get_item/1.

item(In) \ get_item(Out) <=> In = Out.

Query:

?- item(foo),get_item(X).
X = foo.

Have a look at this tutorial for some more info: http://www.pathwayslms.com/swipltuts/chr/index.html

Answer 2

I'm following Anne Ogborn's great CHR tutorial. Some notes:

Where is the CHR constraint store?

In the above tutorial, under 5 Which Rule fires? we read:

When CHR is just sitting there no constraint is active. When we call a chr_constraint from Prolog, it is added and made the active constraint. If the rule causes other rules to be added, in turn they will be the active constraint. Only rules that contain the active constraint are checked.

This makes the store more stable. You needn’t worry about some unrelated action firing a rule.

And under 6.1 Threads

A CHR store is local to one thread.

This is particularly painful when implementing a server that uses CHR.

One solution is to do all the CHR work on a special thread.

Falco Nogatz’s CHR-Constraint-Server is a useful tool.

The 3 Little Pigs game is a useful starter for a server that uses CHR for its logic.

A Pengine will have its own thread. This can be useful for CHR.

The SWI Prolog documentation says under global variables

Global variables are associations between names (atoms) and terms. They differ in various ways from storing information using assert/1 or recorda/3.

The value lives on the Prolog (global) stack. This implies that lookup time is independent of the size of the term. This is particularly interesting for large data structures such as parsed XML documents or the CHR global constraint store.

What is the deal with backtracking?

CHR rules don't backtrack, as that concept makes no sense in the CHR approach. However, under Making CHR interact with Prolog, we read:

If Prolog in the body of any rule fails, all changes to the store since the original attempt to add a constraint (by calling it from Prolog) are rolled back. The Prolog itself then fails to that point.