prolog - Prolog 的逻辑更新 View 如何用于断言和收回？

Question

有人可以详细解释有关断言和撤回的 Prolog 逻辑 View 吗？

例如在下面的代码中，在第一次运行时 Prolog 返回 true，在后续运行中返回 false。我不知道为什么因为 Prolog 逻辑 View 时 asserta(nextBound(100))满足，nice(X) 在启动时仍然被值卡住，因此应该忽略此更改并且 nextbound(100)一定是假的。

nextBound(10000).

nice(X) :-
   asserta(nextBound(100)),
   retract(nextBound(10000)),
   nextBound(100).

Answer 1

从历史角度来看，逻辑更新 View 首先在 Quintus 2.0(其当前的继任者是 SICStus)中实现并在 1987 年的文献中进行了描述。它已被 ISO Prolog ISO/IEC 13211-1:1995 采纳。主要思想是，动态谓词的任何目标都将准确地考虑在执行目标时出现的那些子句。任何进一步的变化——无论是添加还是删除——都不会被考虑到执行那个目标。

在逻辑更新 View 之前，已经有各种或多或少一致的实现，大多数与 Prolog 系统的各种优化不兼容。请注意，差异仅在您的目标可能有多个答案时显示。无论是作为一个简单的目标，还是在使用回缩时 和 您正在使用 retract/1或 assertz/1 .使用asserta/1时不显示差异只要。所以你的例子无法澄清差异。

考虑一个动态谓词 p/1 .由于以下交互仅使用顶层，我将制作 p/1通过断言事实并立即撤回 p/1 的所有事实而被系统知晓.另外，我将使用 retractall(p(_)) 删除所有事实。在开始下一个查询之前。

?- asserta(p(1)).
true.  % now p/1 is known to the system.

?- retractall(p(_)), assertz(p(1)), p(X), assertz(p(2)).
X = 1.  % only one answer!

?- retractall(p(_)), assertz(p(1)), p(X), assertz(p(2)), p(Y).
X = 1, Y = X ;
X = 1,
Y = 2.

所以第一个目标p(X)只能看到 p(1) ，而第二个目标 p(Y)两者都看到。这适用于任何事件目标:

?- retractall(p(_)), assertz(p(1)), assertz(p(2)), p(X), assertz(p(3)), p(Y).
X = 1, Y = X ;
X = 1,
Y = 2 ;
X = 1,
Y = 3 ;
X = 2,
Y = 1 ;
X = 2, Y = X ;
X = 2,
Y = 3 ;
X = 2,
Y = 3 ;
false.

再次注意 X只有 1 或 2 但不是 3。

或者，您可以想象每个目标 p(X)被替换为:

... findall(Xi, p(Xi), Xis), member(X, Xis) ...

这向您展示了背后的想法:从概念上讲，所有答案都是临时存储的，然后才显示每个答案。

呃，上面说的不太对，只针对p/1的子句是这样处理的。也就是说，只要你只存储事实，上面的解释是完美的，但如果你还存储规则，你需要一个更复杂的解释，大致:

 ... findall(Xi-Bi, clause(p(Xi),Bi), XiBis), member(X-B,XiBis), B ...

而且，再一次，这不是简单的事实，因为一些更奇特的问题，如削减可能会干预。我暂时就这样吧1。

同样，retract/1还将查看和删除它在执行时看到的子句。对于大多数情况，这是非常直观的并且符合我们的预期。然而，也有一些非常荒谬的情况如下:

?- retractall(p(_)),
   assertz(p(1)), assertz(p(2)),
   retract(p(X)), ( X = 1, retract(p(Y)) ; X = 2, Y = none ).
X = 1,
Y = 2 ;
X = 2,
Y = none.

在这里，事实p(2)被删除了两次，尽管数据库只包含一个事实 p(2).
脚注

1 实际上，替换

... p(X) ...

经过

... findall(Xi-Bi, clause(p(Xi),Bi), XiBis), answs_goal_x(XiBis,X, G), G ...

和

answs_goal_x([], _, true).
answs_goal_x([Xi-Bi|XiBis], X, ( X = Xi, Bi ; G) ) :-
   answs_goal_x(XiBis, X, G).