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?

score 3 · Accepted Answer · answered Sep 11 '16 at 17:23

3

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:

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]).

answered Sep 11 '16 at 17:23

mat

40,498
3
51
78

I added this simpagation rule, but the example still does not work as expected in SWI-Prolog. – Anderson Green Sep 11 '16 at 19:33
Please produce a simple, self contained test case that is clearly formatted and shows: (1) the **program**, (2) the **query**, (3) the **actual** result and (4) the **expected** result. – mat Sep 11 '16 at 19:35
I updated this question, showing the modified version of this program that produces an `out of local stack` error. – Anderson Green Sep 11 '16 at 19:37
1

You must put the simpagation rule first or at least earlier. Please read more of the existing CHR literature to see how they work, and next time please more clearly separate your programs from your query. Combining them makes it unnecessarily hard to even compile the program successfully. – mat Sep 11 '16 at 19:42

Avoiding infinite recursion with Constraint Handling Rules

1 Answers1