我正在使用 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).