我试图理解为什么Prolog实现不会根据教科书中的执行模型来表现 - 例如,Sterling和Shapiro的书中的"Prolog的艺术"(第6章,"纯粹的Prolog",第6.1节, "Prolog的执行模式").
我引用的执行模型是这个(Sterling和Shapiro的第93页):
输入:目标G和程序P.
输出: G的一个实例,它是P的逻辑结果,否则不是
算法:
Initialize resolvent to the goal G
while resolvent not empty:
choose goal A from resolvent
choose renamed clause A' <- B_1, ..., B_n from P
such that A, A' unify with mgu ?
(if no such goal and clause exist, exit the "while" loop)
replace A by B_1, ..., B_n in resolvent
apply ? to resolvent and to G
If resolvent empty, then output G, else output NO
此外(同一本书的第120页),Prolog choose goal A以从左到右的顺序选择目标(),并choose renamed clause ...按照它们在程序中显示的顺序搜索子句().
下面的程序有一个定义not(n在程序中调用)和一个事实.
n(X) :- X, !, fail.
n(X).
f(a).
如果我试图证明n(n(f(X))),它会成功(根据两本教科书以及SWI Prolog,GNU Prolog和Yap).但这不是有点奇怪吗？根据几本书所揭示的执行模型,这就是我期望发生的事情(跳过重命名变量以保持简单,因为无论如何都不会发生冲突):
预解: n(n(f(Z)))
统一X在第一个子句中匹配n(f(Z)),并用该子句的尾部替换目标.
解决:n(f(Z)), !, fail.
unification X在第一个子句中再次匹配f(Z),并用该子句的尾部替换解决方案中的第一个目标
解决:f(Z), !, fail, !, fail.
统一比赛f(Z)- >成功!现在这已从解决方案中消除.
解决:!, fail, !, fail.
而" !, fail, !, fail"应该不会得逞!切割后有一个失败.故事结局.(实际上,!,fail,!,fail作为查询输入将在我有权访问的所有Prolog系统中失败).
那么我可以假设教科书中的执行模型不正是Prolog使用的模型吗？
编辑:更改第一个子句,n(X) :- call(X), !, fail使我尝试的所有Prolog没有区别.
下面的标题会告诉您这个特定算法的含义:
图4.2逻辑程序的抽象解释器
此外,其描述如下:
输出:G的一个实例,它是P的逻辑结果,否则不是.
也就是说,4.2中的算法仅向您展示如何计算逻辑程序的逻辑结果.它只会让您了解Prolog的实际工作方式.而且特别无法解释!.此外,4.2中的算法只能解释如何找到一个解决方案("结果"),但Prolog试图以系统的方式找到所有这些解决方案,称为按时间顺序回溯.切割以非常特殊的方式干扰按时间顺序的回溯,这在该算法的级别上无法解释.
你写了:
此外(同一本书的第120页),Prolog(choose goal A)以从左到右的顺序选择目标,并(choose renamed clause ...)按照它们在程序中显示的顺序搜索子句.
这错过了一个重要的观点,你可以在第120页阅读:
Prolog的执行机制是通过选择最左边的目标从抽象解释器获得的......并通过顺序搜索一个可统一的子句和回溯来替换子句的非确定性选择.
所以这是一个小小的补充"和回溯",使事情变得更加复杂.您无法在抽象算法中看到这一点.
这是一个很小的例子,表明在算法中没有明确处理回溯.
p :-
q(X),
r(X).
q(1).
q(2).
r(2).
我们将从p哪个开始重写q(X), r(X)(没有其他方法可以继续).
然后,q(X)选择,θ= { X= 1}.所以我们已经r(1)解决了.但是现在,我们没有任何匹配的子句,所以我们"退出while循环"并回答否.
但是等等,有一个解决方案!那么我们如何得到它呢？当q(X)选择时,θ还有另一个选项,即θ= { X= 2}.算法本身并未明确执行此操作的机制.它只说:如果你到处做出正确的选择,你会找到答案.为了从抽象算法中获得真正的算法,我们需要一些机制来做到这一点.
你的程序不是一个纯粹的Prolog程序,因为它包含一个n/1的!/ 0.您可能会问自己一个更简单的问题:使用您的定义,为什么查询?- n(f(X)). 会失败,尽管程序中明显存在n(X)事实,这意味着每个 X 都有 n(X)为真,因此应特别注意f(X)也是？这是因为由于使用了!/ 0而无法再单独考虑程序的子句,并且不能使用纯Prolog的执行模型.对于这种不纯的谓词,更现代和纯粹的替代方法通常是约束,例如dif/2,您可以使用约束将变量约束为与术语不同.
当您到达最后一步时：
这里的剪切削减在这里根本没有任何意义，第一个!意味着“擦除所有内容”。所以解析器变空了。（这当然是伪造的，但已经足够接近了）。fail说要翻转决定，第二个是fail将其翻转回来。现在 resolvent 是空的 - 决定是“是”，并且仍然如此，两次翻转。（这也是伪造的……“翻转”只有在存在回溯的情况下才有意义）。
您当然不能!在解决方案中的目标列表上进行削减，因为它不仅仅是要实现的目标之一。它具有操作意义，通常说“停止尝试其他选择”，但该解释器不会跟踪任何选择（它“好像”一次做出所有选择）。fail不仅是一个要实现的目标，它还说“你成功了就说你没有成功，反之亦然”。
那么我可以假设教科书中的执行模型不是 Prolog 使用的吗？
是的，当然，真正的 Prolog 具有cut并且fail与您提到的抽象解释器不同。该解释没有明确的回溯，而是用魔法有多个成功（其选择本身是不确定的，就好像所有的选择都在一经作出，并行-真正Prologs只是模拟，通过顺序执行与明确的回溯，到了cut是指的是 - 否则它根本没有任何意义）。