Prolog的逻辑更新视图如何用于断言和撤销?

Cod*_*ork 5 prolog iso-prolog prolog-assert

有人可以解释关于断言和撤回的Prolog逻辑视图吗?

例如,在下面的代码中,在第一次运行时Prolog返回true,在后续运行中返回false.我不知道为什么因为Prolog逻辑视图 asserta(nextBound(100))满足时,nice(X)在启动时仍然被值冻结,因此这个更改应该被忽略并且nextbound(100)必须为false.

nextBound(10000).

nice(X) :-
   asserta(nextBound(100)),
   retract(nextBound(10000)),
   nextBound(100).
Run Code Online (Sandbox Code Playgroud)

lur*_*ker 5

您可以执行trace以确定发生的情况:

| ?- nice(_).
      1    1  Call: nice(_17) ?
      2    2  Call: asserta(nextBound(100)) ?
      2    2  Exit: asserta(nextBound(100)) ?   <-- 1st assert of netBound(100) succeeds
      3    2  Call: retract(nextBound(10000)) ?
      3    2  Exit: retract(nextBound(10000)) ? <-- retract nextBound(10000) succeeds
      4    2  Call: nextBound(100) ?
      4    2  Exit: nextBound(100) ? <-- Succeeds because netBound(100) now a fact
      1    1  Exit: nice(_17) ?

(1 ms) yes
{trace}
| ?- nice(_).
      1    1  Call: nice(_17) ?
      2    2  Call: asserta(nextBound(100)) ?
      2    2  Exit: asserta(nextBound(100)) ?   <-- 2nd assert of netBound(100) succeeds
      3    2  Call: retract(nextBound(10000)) ?
      3    2  Fail: retract(nextBound(10000)) ? <-- retract nextBound(10000) fails
      1    1  Fail: nice(_17) ?

(3 ms) no
{trace}
| ?-
Run Code Online (Sandbox Code Playgroud)

你可以看到,在第一种情况下,首先nextBound(100)成功断言事实(第一次).然后,retract(nextBound(10000))成功因为nextBound(10000).是数据中存在的事实.之后,查询nextBound(100)成功,因为在此事实之前的两个步骤被声明为数据.

在第二次执行时nice(_),nextBound(10000)不存在,因为它在第一次执行中被收回,并且代码没有重新断言它.因此,在第二次执行中nice(_),retract(nextBound(10000))失败是因为事实nextBound(10000)不存在,并且整个第二次执行nice(_)在该点失败,因为回溯asserta并且retract不重新执行并产生额外的结果.

列表显示现在有两个nextBound(100)事实,因为我们在两次运行中都声明了一个nice(_),并且nextBound(10000)自从它在第一次运行中收回时没有nice(_):

| ?- listing.

% file: user

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

% file: user_input

nextBound(100).
nextBound(100).

(1 ms) yes
| ?-
Run Code Online (Sandbox Code Playgroud)

逻辑更新视图,如SWI文档中所述,从SWI-Prolog 3.3.0开始,我们遵循逻辑更新视图,其中输入谓词定义的可回溯谓词将不会看到任何更改(由assert/1或由retract/1)到谓词.

换句话说,逻辑更新视图可防止谓词在执行时动态更改自身.这不是这里的情景.

实际上,在Prolog中,在执行谓词期间,如果在谓词中的某一点断言事实,则该结果必须立即在其中可见,或者谓词可能无法正常运行,这一点至关重要.有许多常见的库谓词依赖于此行为.


fal*_*lse 5

从历史角度出发,逻辑更新视图首先在Quintus 2.0(其当前的后继者是SICStus)中实现,并在1987年的文献中进行了描述.它已在ISO Prolog ISO/IEC 13211-1:1995中采用.主要的想法是,动态谓词的任何目标都将完全考虑那些在执行目标时出现的子句.任何进一步的更改 - 无论是添加还是删除 - 都不会被考虑用于执行该目标.

在逻辑更新视图之前,存在各种或多或少一致的实现,大多数与Prolog系统的各种优化不兼容.请注意,差异仅显示您是否有可能有多个答案的目标.无论是作为一个简单的目标,还是使用撤回,你正在使用retract/1assertz/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.
Run Code Online (Sandbox Code Playgroud)

所以第一个目标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.
Run Code Online (Sandbox Code Playgroud)

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

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

... findall(Xi, p(Xi), Xis), member(X, Xis) ...
Run Code Online (Sandbox Code Playgroud)

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

呃,上述观点并不完全正确,因为只有在条款p/1都是这样处理的.也就是说,只要你只存储事实,上面的解释是完美的,但如果你也存储规则,你需要一个更复杂的解释,粗略地说:

 ... findall(Xi-Bi, clause(p(Xi),Bi), XiBis), member(X-B,XiBis), B ...
Run Code Online (Sandbox Code Playgroud)

而且,这不是一个明确的事实,因为一些更奇特的问题,如削减可能会介入.我将暂时离开它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.
Run Code Online (Sandbox Code Playgroud)

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


脚注

1实际上,更换

... p(X) ...
Run Code Online (Sandbox Code Playgroud)

通过

... findall(Xi-Bi, clause(p(Xi),Bi), XiBis), answs_goal_x(XiBis,X, G), G ...
Run Code Online (Sandbox Code Playgroud)

answs_goal_x([], _, true).
answs_goal_x([Xi-Bi|XiBis], X, ( X = Xi, Bi ; G) ) :-
   answs_goal_x(XiBis, X, G).
Run Code Online (Sandbox Code Playgroud)