SWI Prolog 中的约束处理规则：`neq` 约束不起作用
Constraint Handling Rules in SWI Prolog: The `neq` constraint doesn't work
我正在学习 swi-prolog 中的约束处理规则 (CHR)。
我从 Tom Schrijvers 的教程开始 Constraint Handling Rules A Tutorial for (Prolog) Programmers。
作者在p.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。
谢谢。
这是 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 实现似乎禁止出现在守卫头部的绑定变量（参见 Check guard bindings yourself），即使这些绑定可以通过 \+ 回滚。请注意 X \= Y 等同于 \+ X = Y。此外，守卫中的统一谓词 = 似乎只是与变量的标识符进行比较而不是统一它们。
此解决方法的缺点是，例如，
?- neq(A,B), A = [1,X], B=[].
A = [1,$VAR(X)],
B = [],
neq([1,$VAR(X)],[]).
由于 A 不是地面，第二条规则不会触发，但我们知道 A 和 B 不能相等，即 neq([1,$VAR(X)],[]) 应该有已删除。
无论如何，这只是一个临时的解决方法。如果有人有更好的解决方案或解释，我可以删除这个答案。
您可以在第二个子句中使用 ?=/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 = [].
我正在学习 swi-prolog 中的约束处理规则 (CHR)。
我从 Tom Schrijvers 的教程开始 Constraint Handling Rules A Tutorial for (Prolog) Programmers。
作者在p.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。
谢谢。
这是 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 实现似乎禁止出现在守卫头部的绑定变量（参见 Check guard bindings yourself），即使这些绑定可以通过 \+ 回滚。请注意 X \= Y 等同于 \+ X = Y。此外，守卫中的统一谓词 = 似乎只是与变量的标识符进行比较而不是统一它们。
此解决方法的缺点是，例如，
?- neq(A,B), A = [1,X], B=[].
A = [1,$VAR(X)],
B = [],
neq([1,$VAR(X)],[]).
由于 A 不是地面，第二条规则不会触发，但我们知道 A 和 B 不能相等，即 neq([1,$VAR(X)],[]) 应该有已删除。
无论如何，这只是一个临时的解决方法。如果有人有更好的解决方案或解释，我可以删除这个答案。
您可以在第二个子句中使用 ?=/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 = [].