使用约束处理规则避免无限递归

Question

我使用 Constraint Handling Rules 在 SWI-Prolog 中编写了一组简单的约束。它使用了两个相对简单的推理规则：

%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([3,is,equal,to,4],[3,equals,4]) 是 true，但它似乎导致无限递归：

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

我在这个程序中添加了一个 simpagation 规则，但它仍然导致 Out of local stack 错误：

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

是否可以重写推理规则，使其不产生无限递归？

Answer 1

请阅读可用的 CHR 文献，了解有关 CHR 这些方面的更多详细信息。

例如，Tips for CHR programming 包含在 编程提示 中：

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

因此，如果您添加 CHR 简化规则，您的示例将按预期工作：

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

示例查询和结果：

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

使用约束处理规则避免无限递归

Avoiding infinite recursion with Constraint Handling Rules

prolog

constraint-programming

constraint-handling-rules