时间戳

首页 > 解决方案 > SWI-Prolog 的`foreach/2` 是否涉及`freeze/2`？

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

问题描述

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

描述

包含foreach/2谓词的“聚合”库的兼容性被声明为

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

来自SICStus Prolog 文档：

foreach(:Generator, :Goal)

对于生成器的每个证明，我们依次制作具有适当替换的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是确保正确恢复 未出现在Generator中的Goal变量。（如果没有这样的变量，你不妨使用。）forall/2

就像，这个谓词在Generatorforall/2上做了一个失败驱动的循环 。与 不同的是，目标作为普通连词执行，并且可能以多种方式成功。forall/2

以 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应该确定 multiple 的合取dif(Y,i)为真，因为未绑定的变量Y显然dif来自整数i。

但现在：

?- 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. 如何？

我认为可能会freeze/2涉及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))).

?- 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.

这是怎么回事？

标签： foreachprolog

解决方案

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

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

推荐阅读