Как избежать бесконечной рекурсии с помощью правил обработки ограничений

Question

Я написал простой набор ограничений в 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]).

Я добавил правило упрощения в эту программу, но оно все еще приводит к 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.

Например, Советы по программированию CHR содержатся в Подсказках попрограммированию:

9. Установить семантику

Система CHR допускает наличие идентичных ограничений, то есть нескольких ограничений с одним и тем же функтором, арностью и аргументами. Для большинства решателей ограничений это нежелательно: это влияет на эффективность и, возможно, завершение. Следовательно, соответствующие правила упрощения должны быть добавлены в виде:constraint \ constraint <=> true

Таким образом, ваш пример работает должным образом, если вы добавите правило упрощения CHR:

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

Пример запроса и результат:

? - означает ([3, равно,4,],[3 и 4 равно]). означает ([3, и,4, равны],[3, равно, равно, 4]), означает ([3, равно, равно,4],[3, и,4, являются, равно]).