CLPB 的不良特性

Question

library(clpb) 目前在 SICStus（原始版本）和 SWI（按 mat）中可用。让我很快进入本质：

?- X = 1+1, sat(X), X = 1+1.
X = 1+1.

?-          sat(X), X = 1+1.
false.

所以这是一个类似的问题，因为它存在于 library(clpfd) 的默认状态。

遇到这种情况怎么办？

更新：在 mat 的 library(clpfd) 中，现在有用于此目的的仿函数 # /1。理想情况下，伴随着运算符声明 op(150,fx,#)，我们现在可以写：

?- X = 1+1, #X #= Y.
ERROR: Type error: `integer' expected, found `1+1' (a compound)

为了确保完整的代数性质，必须声明：

:- set_prolog_flag(clpfd_monotonic, true).

现在，不明确的变量（因此，要么只是整数，要么是表达式）会产生实例化错误：

?-  1 + 1 #= Y.
ERROR: Arguments are not sufficiently instantiated
?- 1 + 1 #= #Y.
Y = 2.

Answer 1

是的，在 CLP(FD) 和 CLP(B) 中相同：

情况

CLP(FD)，(+)/2在有限域中作为加法：

?- X = 1+1, X #= 2.
X = 1+1.

?- X #= 2.
X = 2

?- X #= 2, X = 1+1.
false.

CLP(B)，(+)/2 在布尔域中充当析取：

?- X = 1+1, sat(X)
X = 1+1

?- sat(X)
X = 1

?- sat(X), X = 1+1.
false

但现在要小心，这样的事情在普通序言中已经发生了：

?- X = 3, X \= 4.
X = 3.

?- X \= 4, X = 3.
false.

问题

那么我们应该告诉学生什么呢？我不认为 CLP(FD) 或 CLP(B) 是罪魁祸首。

它在 (=)/2 中更加根深蒂固，并且无法挂钩 (=)/2 这样它做的不仅仅是 verify_attribute/3.

在理想世界中 (=)/2 可以用代数计算，而 X=1+1 不会失败，系统会看到 1+1 等于 2（FD 情况） 1+1 分别等于 1（B 情况）。

但是为此 Prolog 系统需要类型作为开始，否则 (=)/2 不能解释 (+)/2，它有两种不同的解释在我们的例子中。

解决方案

解决方案是避免在需要特定类型的地方使用 (=)/2。特此推荐阅读：

Constraint Logic Programming using ECLiPSe
Krzysztof R. Apt and Mark Wallace,
May 16, 2006, Full Text PDF

上述论文稍微强调了井号 (#) 作为 (=)/2、(<)/2 等运算符前缀的动机。它已经是一种类型注释。本文还有一个前缀，即美元符号($).

在 ECLiPSe Prolog 中，井号 (#) 表示约束 integers/1，美元符号 ($) 表示约束 reals/1。这些约束也可以独立使用，如下例所示：

?- integers([X,Y]), X = 3, Y = 4.5.
No

?- reals(X), X = [1,2.1,a].
No

回到你的 (=)/2 的非交换性问题。尽管 (=)/2 是不可交换的，但 (#=)/2 及其布尔兄弟当然是可交换的。我们有：

CLP(FD)，(+)/2在有限域中作为加法，与(#=)/2可交换：

?- X #= 1+1, X #= 2.
X = 2

?- X #= 2, X #= 1+1.
X = 2

CLP(B)，(+)/2 在布尔域中充当析取，并且具有 sat/1 和 (=:=)/2 交换性：

?- sat(X=:=1+1), sat(X).
X = 1.

?- sat(X), sat(X=:=1+1).
X = 1

A verify_attribute/3 挂钩只会唤醒约束，这些约束还会使 Herbrand 域统一失败。但是他们无法在将项分配给 Prolog 变量之前即时评估项。

只有被唤醒的约束才能为其他变量赋值。但是例如 verify_atribute/3 的当前 SICStus 规范甚至建议不要直接这样做，而只能在继续队列中这样做。请参阅最近的 SWI-Prolog 小组讨论。

长话短说：永远不要忘记 (=)/1 仅适用于 Prolog 中的 Herbrand 域，即使我们在约束中挂钩。我不是说 Prolog 系统不能以不同的方式工作，但这是 Herd 或 Prolog 系统的艺术状态。

再见

Answer 2

What to do in such a situation?

同时，library(clpb)也保证了类似于library(clpz)/library(clfd)的单调性。在此执行模式下，显式变量必须用 (v)/1.

修饰

?- current_prolog_flag(clpb_monotonic,B).
B = false.                             % the default

?- sat(X).
X = 1.

?- set_prolog_flag(clpb_monotonic,true).
true.

?- sat(X).
ERROR: Arguments are not sufficiently instantiated

?- sat(v(X)).
X = 1.

在 Scryer 中，说：

?- use_module(library(clpb)).
   true.
?- asserta(clpb:monotonic).
   true.
?- sat(X).
caught: error(instantiation_error,instantiation_error(unknown(_67),1))
?- sat(v(X)).
   X = 1
;  false.

CLPB 的不良特性

Undesirable properties of CLPB

prolog

clpb