Prolog 子句单独终止，但不一起终止

Question

所以

?- canCall(mary, Person).

工作并终止

?- canFind(mary, Person).

也可以工作和终止。但不知何故

?- canCall(mary, Person), canFind(mary, Person). 

不终止。可能的原因是什么？

Answer 1

(您的实际意思是:查询单独终止，但有时它们的连接不会终止)

您已经在这里发现了 Prolog 终止属性的一个非常基本的方面。让我们通过以下纯¹ 程序来看看这一点:

canFind(mary, john).

canCall(mary, bob).
canCall(A, B) :-
   canCall(B, A).

?- canCall(mary, Person).
   Person = bob
;  ... .

?- canFind(mary, Person).
   Person = john.

一切看起来都很好!让我们 checkin 这段代码，以便每个人都可以使用它。现在你倒霉的同事尝试:

?- canCall(mary, Person), canFind(mary, Person).
   loops.

哦不，这会循环!也许我只需要重新排列目标:

?- canFind(mary, Person), canCall(mary, Person).
   loops.

再来一次!

当然，你也很沮丧。毕竟，您认真地测试了这段代码。它终止了。还是做到了？

终止的两种概念

这是 Prolog 中最令人困惑的事情之一:我们这里(至少)有两种不同的查询终止概念。您测试的(有时)称为存在终止。不过，我更建议将其简单地称为找到答案。正如您所经历的那样，它非常脆弱。

如果查询不仅找到了答案，而且找到了全部答案并完成了查询，则这称为通用终止或简称为终止>。如果 Prolog 程序员说查询终止，他们的意思是它普遍终止。

那么我们如何观察普遍终止呢？只需询问所有答案即可。在 GNU-Prolog 中输入 a。在其他系统中，您必须敲击SPACE或;Return直到完成，否则您疲劳的眼睛或腕管会阻止它。返回直到完成。 p>

?- canCall(mary, Person).
   Person = bob
;  Person = bob
;  Person = bob
;  Person = bob
;  Person = bob
;  ... .

所以在这里我们看到有无限多个答案(实际上，我们有限的存在必须证明这一点，但暂时相信我)。

有没有更便宜的方法来观察这一点？如果没有这些答案的文字墙？您可以通过添加一个永远不成立的条件来“关闭”答案，false。

所以问:

?- canCall(mary, Person), false.

这样的查询会产生什么结果？它永远不可能是true。如果它终止，它只能是false。因此，通过此查询，我们仅仅测试程序的终止属性。

现在，两个(通用)终止查询的结合将始终终止。所以这种终止方式更加稳健。

通用终止还有许多更酷的属性。例如，您可以随意交换子句(即事实和规则)的顺序:无论它们的顺序如何，所有程序都共享完全相同的终止属性。

另一个是，您可以借助 failure-slice 轻松找到程序中非终止的来源。 。从 this one 开始阅读.

在面向命令的编程语言中，这个概念并不容易出现。然而，对于迭代器，您有非常相似的概念:如果迭代器生成第一个项目，则对应于存在终止，并且如果生成有限多个项目，也就是说，如果在有限多个 next 之后它就完成了，这对应于普遍终止。有点像。

<小时/>

_{1 实际上，在不纯粹的程序中，你会出现各种无意义的行为。所以考虑它们是没有意义的。}