Prolog:a(b,c) 和 a(X,Y):-a(Y,X)，查询 a(c,b) 返回无限真？

Question

这是我的知识库:

a(b,c). 
a(X,Y):-a(Y,X). 

这是我的查询:a(c,b).

我正在使用 SWI-Prolog。我认为这个查询会导致程序打印“true”。但是，它会打印“true”并在我按下分号时继续打印 true...直到永远。

为什么不停止？

我的想法:首先，X 绑定(bind)到 b，Y 绑定(bind)到 c。然后，Prolog 测试 a(b,c) 并​​发现这是真的。因此，a(c,b) 也为真，SWI-Prolog 应该打印一次为真。然而，由于只要我不断点击那个分号，它就会永远打印 true，这让我认为递归的事情正在发生。这是在哪里发生的？帮助!

编辑:更具体地说，我的问题是为什么程序在每个“真”之后暂停并等待我按下分号或另一个键而不是刚刚完成？如果我有两个谓词 human(socrates) 和 mortal(X):-humans(X)，对查询 mortal(socrates) 的响应将是一个“真”。 (抱歉，如果我没有在上面说清楚。)

Answer 1

Prolog 首先通过第二条规则和第一条规则证明a(c,b)。然后，它通过第三次调用第二条规则然后调用第一条规则来证明 a(c,b)。然后，通过第二条规则的五次调用，等等。Prolog 的推理算法是一种没有闭集的深度优先搜索，即它不会跟踪它已经证明的内容并愉快地再次证明它。

如果你不想要这种行为，你应该重写规则，例如，

a_fact(b, c).
a(X, Y) :- a_fact(X, Y).
a(Y, X) :- a_fact(X, Y).

... 或使用某种 tabling execution .不过，我认为 SWI-Prolog 不支持制表。