Reputation: 31800
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?
Upvotes: 1
Views: 246
Reputation: 40768
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]).
Upvotes: 3