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

Question

我正在使用 swi-prolog 在 Prolog 类(class)的上下文中为学生制作一些示例。关于统一，我想提请他们注意统一过程中无限递归的危险。然而，像 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 绑定(bind)到 Y？我没想到。

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

Answer 1

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

您的示例表明您对语法统一感兴趣。在这里，只要是NSTO (not subject to occurs-check)，统一就定义明确并终止。 .所有序言都同意这里。

许多序言提供有理树统一。 SWI 从 2004 年 5.3 开始提供它。而且这个算法正在终止。鉴于这些假设，您问题的答案是不，它不能无限递归。

然而，有理树对编程的用处相当有限。其主要动机是效率方面的考虑。即，具有发生检查成本的可变术语统一取决于术语的大小，只是有时它们可​​以是 reduced to constant cost。 .但对于有理树，它们始终是常数。

由于您的兴趣相当集中于教学，请考虑通过像这样更改统一算法来避免创建无限树(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.