Vermeiden von unendlicher Rekursion mit Constraint Handling Regeln

Question

Ich habe einen einfachen Satz von Constraints in SWI-Prolog mit Constraint Handling Rules geschrieben. Es verwendet zwei relativ einfache Schlußregeln:

%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 means([3,is,equal,to,4],[3,equals,4]) erwartet true zu sein, aber es scheint stattdessen eine unendliche Rekursion zu verursachen:

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

ich eine simpagation Regel zu diesem Programm hinzugefügt, aber es noch führt zu einem Out of local stack Fehler:

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

Ist es möglich, die Schlußregeln neu zu schreiben, so dass sie erzeugt keine unendliche Rekursion?

Answer 1

Bitte lesen Sie die verfügbaren CHR Literatur für detailliertere Informationen über solche Aspekte von   CHR.

Zum Beispiel enthält Tips for CHR programming in Programmierung Hinweise:

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

So funktioniert Ihr Beispiel, wie erwartet, wenn Sie die CHR simpagation Regel hinzufügen:

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

Beispielabfrage und Ergebnis:

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