1

我正在学习 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.

如何获得与幻灯片中相同的结果？

我在 Windows 上的 swi-prolog 版本（线程，64 位，版本 8.2.4）。

谢谢。

4

2 回答 2

2

您可以使用?=/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 = [].
于 2021-11-29T15:33:23.700 回答
0

这是一个临时解决方法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)],[]).

由于Ais not ground，第二条规则不会触发，但我们知道它A不能B相等，即neq([1,$VAR(X)],[])应该被删除。

无论如何，这只是一个临时的解决方法。如果有人有更好的解决方案或解释，我可以删除这个答案。

于 2021-11-29T10:09:22.363 回答