Avoiding infinite recursion with Constraint Handling Rules

Question

I have written a simple set of constraints in SWI-Prolog using Constraint Handling Rules. It uses two relatively simple rules of inference:

%If A means B, then B means A.
means(A,B) ==> means(B,A).    
%If A means B and A means C, then B means C.
means(A,B),means(A,C) ==> means(B,C).

I expected means([3,is,equal,to,4],[3,equals,4]) to be true, but it seems to cause infinite recursion instead:

:- use_module(library(chr)).
:- chr_constraint means/2.
:- initialization(main).


means([A,equals,B],[A,'=',B]).
means([A,is,equal,to,B],[A,'=',B]).
means([A,equals,B],[A,and,B,are,equal]).


%These are the rules of inference for this program.
    %If A means B, then B means A.
    means(A,B) ==> means(B,A).    
    %If A means B and A means C, then B means C.
    means(A,B),means(A,C) ==> means(B,C).

main :-
    %This part works as expected. X = [3,'=',4].
    means([3,is,equal,to,4],X),writeln(X),

    %This statement should be true, so why does it produce an infinite recursion?
    means([3,is,equal,to,4],[3,and,4,are,equal]).

I added a simpagation rule to this program, but it still leads to an Out of local stack error:

:- use_module(library(chr)).
:- chr_constraint means/2.
:- initialization(main).


%These are the rules of inference for this program.
    %If A means B, then B means A.
    means(A,B) ==> means(B,A).    
    %If A means B and A means C, then B means C.
    means(A,B),means(A,C) ==> means(B,C).
    means(A,B) \ means(A,B) <=> true.
    means(A,A) <=> true.

means([A,equals,B],[A,'=',B]).
means([A,is,equal,to,B],[A,'=',B]).
means([A,equals,B],[A,and,B,are,equal]).

main :-
    %This part works as expected. X = [3,'=',4].
    means([3,is,equal,to,4],X),writeln(X),

    %This statement should be true, so why does it produce an infinite recursion?
    means([3,is,equal,to,4],[3,and,4,are,equal]).

Is it possible to re-write the rules of inference so that they do not produce infinite recursion?

Answer 1

Please read the available CHR literature for more detailed information about such aspects of CHR.

For example,Tips for CHR programming contains in Programming Hints:

9. Set Semantics

The CHR system allows the presence of identical constraints, i.e. multiple constraints with the same functor, arity and arguments. For most constraint solvers, this is not desirable: it affects efficiency and possibly termination. Hence appropriate simpagation rules should be added of the form: constraint \ constraint <=> true

Thus, your example works as expected if you add the CHR simpagation rule:

means(A,B) \ means(A,B) <=> true.

Sample query and result:

?- means([3,is,equal,to,4],[3,and,4,are,equal]).
means([3, and, 4, are, equal], [3, is, equal, to, 4]),
means([3, is, equal, to, 4], [3, and, 4, are, equal]).