Prolog中的双重否定和执行模型
我试图理解为什么Prolog的实现不按照教科书中的执行模式行事 - 例如，Sterling和Shapiro的“艺术之道”一书（第6章，“纯粹序言”，第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）。 但这不是很奇怪吗？ 根据这个几本书所揭示的执行模型，这是我期望发生的事情（跳过重命名变量以使事情简单化，因为不会有任何冲突）：
RESOLVENT： n(n(f(Z)))
统一将第一个子句中的X与n(f(Z))匹配，并用该子句的尾部替换目标。
决议： n(f(Z)), !, fail 。
统一将第一个子句中的X与f(Z)再次匹配，并将resolvent中的第一个目标替换为子句的尾部
决议： f(Z), !, fail, !, fail 。
统一匹配f(Z) - >成功！ 现在，这从解决方案中消除了。
决议： !, fail, !, fail 。
和“ !, fail, !, fail ”不应该成功！ 裁员后失败。 故事结局。 （事实上，输入!,fail,!,fail因为查询在我有权访问的所有Prolog系统中都会失败）。
那么我是否可以假定教科书中的执行模型并不完全是Prolog所使用的？
编辑 ：将第一个子句更改为n(X) :- call(X), !, fail在我尝试的所有Prolog中没有任何区别。
当你到达最后一步时：
切! 这里的意思是，“抹去一切”。 所以解决方法变得空虚。 （当然这是假的，但足够接近）。 削减在这里根本没有意义，第一次fail说翻转这个决定，第二次fail翻转。 现在解决方案是空的 - 决定是“是”，并保持如此，两次翻转。 （这也在伪装它......“翻转”只有在回溯的情况下才有意义）。
你当然不能放一个切! 在解决方案的目标列表中，因为它不仅仅是要实现的目标之一。 它具有操作意义，通常说“停止尝试其他选择”，但这个解释器没有跟踪任何选择（它“好像”一次做出所有选择）。 fail不仅仅是一个目标，它还会说“你成功的地方说你没有成功，反之亦然”。
那么我是否可以假定教科书中的执行模型并不完全是Prolog所使用的？
是的，当然，真正的Prologs已经cut和fail不像你提到的抽象解释。 该解释没有明确的回溯，而是用魔法有多个成功（其选择本身是不确定的 ，就好像所有的选择都在一经作出，并行-真正Prologs只是模拟，通过顺序执行与明确的回溯，以该cut是指 - 它根本就没有其他含义）。
下面的标题确实告诉你这个特定的算法是关于什么的：
图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循环”并回答no。
但等一下，有一个解决方案！ 那么我们如何得到它？ 当选择q(X)时，θ也有另一种选择，即θ= { X = 2}。 算法本身并不明确执行此操作的机制。 它只是说：如果你在任何地方做出正确的选择，你会找到答案。 为了从抽象的算法中获得真正的算法，我们需要一些机制来实现这一点。
你的程序不是一个纯粹的Prolog程序，因为它包含n / 1中的！/ 0。 你可能会问自己一个更简单的问题：用你的定义，为什么查询?- n(f(X)). 虽然在你的程序中显然有一个事实n（X），这意味着n（X）对于每一个X都是真实的，并且因此也应该对f（X）特别适用？ 这是因为由于使用！/ 0，程序的子句不再被孤立地考虑，并且纯Prolog的执行模型不能被使用。 对于这样不纯的谓词，更现代和纯粹的选择通常是约束条件，例如dif / 2，可以将变量约束为与术语不同。