SWI-Prolog 的`foreach/2` 是否涉及`freeze/2`？

Question

在 SWI Prolog 的 foreach/2 上，我们读到：

包含foreach/2谓词is stated to be的“聚合”库的兼容性

Quintus, SICStus 4. forall/2 是一个内置的 SWI-Prolog 和 term_variables/3 是一个内置的 SWI-Prolog，具有不同的语义。

来自SICStus Prolog documentation：

foreach(:Generator, :Goal)

对于 Generator 的每个证明，我们依次制作 Goal 的副本 适当的替换，然后我们执行这些副本 顺序。例如，foreach(between(1,3,I), p(I)) 是等价的 到p(1), p(2), p(3)。

请注意，这与forall/2 不同。例如， forall(between(1,3,I), p(I)) 相当于

\+ \+ p(1), \+ \+ p(2), \+ \+ p(3).

foreach/2 中的技巧是确保 Goal 的变量 Generator 中没有发生的事件被正确恢复。 （如果有 没有这样的变量，你还不如使用forall/2。）

与forall/2 一样，此谓词在 发电机。与forall/2 不同，Goals 是作为普通连词执行的，并且可能以多种方式成功。

以SWI Prolog页面为例，没有最终统一：

?- foreach(between(1,4,X), dif(X,Y)).
dif(Y, 4),
dif(Y, 3),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 3),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1).

我不确定为什么会有所有 dif/2 实例化的输出以及为什么会有相同子目标的重复。

foreach/2应该判断多个dif(Y,i)的合取为真，因为未绑定变量Y显然是来自整数i的dif。

但是现在：

?- foreach(between(1,4,X), dif(X,Y)), Y = 5.
Y = 5.

好的，所以除了Y=5 之外没有输出，因为目标成功了。但是Y=5 有什么变化？在foreach/2 之后，Prolog 已经能够确定foreach/2 为真（考虑到Y 在foreach/2 运行时的状态），所以添加Y=5 不应该改变任何东西。

然后：

?- foreach(between(1,4,X), dif(X,Y)), Y = 2.
false.

后来的统一改变了foreach/2 的结果。怎么样？

我认为Y 上的freeze/2 可能会让情况变得有趣，因为我们真的在计算：

freeze(Y,foreach(between(1,4,X), dif(X,Y))).

这或多或少可以解释打印输出。例如：

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))).
freeze(Y, foreach(between(1, 4, X), dif(X, Y))).

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))), Y=5.
Y = 5.

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))), Y=2.
false.

这是怎么回事？

Answer 1

您观察到的“冻结”行为是由于 dif/2 而不是 foreach/2。

谓词 dif/2 确保它的两个参数不相同并且不会变得相同。因此，如果两个参数可能变得相同，则 dif/2 将暂停，直到它可以确定它们是否相同。