Правила обработки ограничений в SWI Prolog: ограничение neq не работает

Question

Я изучаю правила обработки ограничений (CHR) в swi-prolog.

Я начал с учебника Тома Шрайверса « Правила обработки ограничений. Учебник для (Пролог)-программистов » .

На стр. 286 автор привел пример реализации ограничения неравенства.

      :- use_module(library(chr)).

:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> X \= Y | true.

Но это не работает должным образом в swi-prolog.

Например, в swi-prolog

      ?- neq(A,B).
true.

?- neq(A,B), A = B.
A = $VAR(B).

но это должно быть

      ?- neq(A,B).
neq(A,B).

?- neq(A,B), A = B.
false.

Как я могу получить тот же результат, что и на слайде?

Моя версия swi-prolog (потоковая, 64-битная, версия 8.2.4) на windows.

Спасибо.

Answer 1

Вы можете использовать ?=/2 для второго предложения:

      :- use_module(library(chr)).
:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> ?=(X,Y) | true.

Примеры запусков:

      ?- neq(a,a).
false.

?- neq(a,b).
true.

?- neq(A,B).
neq(A, B).

?- neq(A,B), A = f(C), B = f(D).
A = f(C),
B = f(D),
neq(f(C), f(D)).

?- neq(A,B), A = [1,X], B=[].
A = [1, X],
B = [].

Answer 2

Вот временное решение для neq:

      :- use_module(library(chr)).

:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> ground(X), ground(Y) | true.

Он может пройти все тесты в слайде:

      ?- neq(a,a).
false.

?- neq(a,b).
true.

?- neq(A,B).
neq($VAR(A),$VAR(B)).

?- neq(A,B), A = B.
false.

?- neq(A,B), A = a, B = a.
false.

?- neq(A,B), A = a, B = b.
A = a,
B = b.

?- neq(A,B), A = f(C), B = f(D).
A = f($VAR(C)),
B = f($VAR(D)),
neq(f($VAR(C)),f($VAR(D))).

%% And some other tests which not in the slide.

?- neq([1,2,3], [1,2,X]).
neq([1,2,3],[1,2,$VAR(X)]).

?- neq([1,2,3], [1,2,X]), X=3.
false.

?- neq([1,2,3], [1,2,X]), X=4.
X = 4.

?- neq([1,2,3], X).
neq([1,2,3],$VAR(X)).

?- neq([1,2,3], X), X=[1,2,3].
false.

?- neq([1,2,3], X), X=[1,2,Y].
X = [1,2,$VAR(Y)],
neq([1,2,3],[1,2,$VAR(Y)]).

Кажется, что текущая реализация CHR запрещает переменные привязки, которые появляются в начале в гуардах (см. Самостоятельная проверка привязок сторожей ), даже если эти привязки можно было бы откатить через \+. Обратите внимание, что X \= Yэквиваленты \+ X = Y. Кроме того, предикат объединения =в охранах кажется только сравнение с идентификатором переменных, а не их унификация.

Недостатком этого обходного пути является то, что, например,

      ?- neq(A,B), A = [1,X], B=[].

A = [1,$VAR(X)],
B = [],
neq([1,$VAR(X)],[]).

Поскольку это не заземление, второе правило не срабатывает, но мы знаем, что Aа также Bне может быть равным, т.е. neq([1,$VAR(X)],[])должны были быть удалены.

В любом случае, это всего лишь временное решение. Если у кого-то есть лучшее решение или объяснение, я могу удалить этот ответ.