Prolog中的统一算法可以无限递归吗？

Question

我正在使用 swi-prolog 在 Prolog 课程中为学生生成一些示例。关于统一，我想提请他们注意统一过程中无限递归的危险。然而，像 swi-prolog 这样成熟的 Prolog 实现足够智能，可以在大多数情况下避免统一过程的无限递归。在所有情况下都是如此吗？还是可以构建更复杂的例子，使统一仍然无限递归？

?- foo(bar(X)) = X.
X = foo(bar(X)).

?- foo(X) = X.
X = foo(X).

?- foo(X) = Y, X = Y.
X = Y, Y = foo(Y).

?- foo(X) = Y, X = foo(Y).
X = Y, Y = foo(foo(Y)).

作为一个相关的附带问题，为什么（再次，我使用了 swi-prolog）统一在下面的示例中将 X 绑定到 Y？我没想到会这样。

?- X = f(X), Y = f(Y).
X = Y, Y = f(Y).

Answer 1

这完全取决于您对统一算法和Prolog的理解。

你的例子表明你对句法统一感兴趣。在这里，统一被明确定义并终止，只要它是NSTO（不受发生检查）的约束。所有 Prolog 都同意这一点。

许多 Prolog 提供合理的树统一。SWI 从 2004 年 5.3 版开始提供该算法。而且该算法也即将终止。考虑到这些假设，你的问题的答案是否定的，它不能无限递归。

然而，理性树对于编程的用处相当有限。其主要动机是效率考虑。也就是说，可变项统一的发生检查成本高达项的大小，只有有时它们可​​以减少到恒定成本。但对于理性树来说它们总是恒定的。

由于您的兴趣主要集中在教学上，请考虑通过更改统一算法来避免创建无限树，如下所示（SWI 自 5.6.38 起，Scryer）：

?- set_prolog_flag(occurs_check, error).
true.

?- X = f(X).
ERROR: =/2: Cannot unify _G2368 with f(_G2368): would create an infinite tree

在程序开发时，可以启用该标志。并且可以帮助学生找出错误。只要不存在这样的错误，程序就会产生与有理树统一完全相同的结果。

句法统一就这么多。一般来说，在存在约束或协程的情况下，不能保证终止。考虑到

inf :- inf.

?- freeze(X, inf), X = 1.

对于你的附带问题，这是 SWI 顶层的一个特殊性，它有助于在答案中发现相同的术语。

?- X = 1, Y = 1.
X = Y, Y = 1.