4

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

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

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

所以这是一个类似的问题，因为它存在于library(clpfd).

在这种情况下该怎么办？

更新：在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.
4

2 回答 2

2

在这种情况下该怎么办？

同时，也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.

在占卜器中，说：

?- 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.
于 2021-02-09T08:43:58.300 回答
0

是的，在 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。在此我推荐阅读：

使用 ECLiPSe
Krzysztof R. Apt 和 Mark Wallace进行约束逻辑编程
，2006 年 5 月 16 日，全文 PDF

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

在 ECLiPSe Prolog 中，井号 (#) 表示约束整数/1，美元符号 ($) 表示约束实数/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

verify_attribute/3 挂钩只会唤醒可能导致 Herbrand 域统一失败的约束。但是在将术语分配给 Prolog 变量之前，他们无法即时评估术语。

只有唤醒的约束可能会将值分配给其他变量。但例如，当前的 verify_atribute/3 的 SICStus 规范甚至建议不要直接这样做，而只能在延续队列中这样做。参见最近的 SWI-Prolog 小组讨论。

长话短说：永远不要忘记 (=)/1 仅适用于 Prolog 中的 Herbrand 域，即使我们加入了约束。我并不是说 Prolog 系统不能以不同的方式工作，但这是最先进的 Herd 或 Prolog 系统。

再见

于 2016-03-20T01:19:38.410 回答