SWI-Prolog合一算法是否会出现无限递归？及相关变量绑定问题咨询

好问题！我来帮你拆解这两个关于SWI-Prolog合一的核心疑问：

一、SWI-Prolog的合一是否能避免所有无限递归场景？ #

首先明确：SWI-Prolog的标准合一谓词=/2通过支持循环项（cyclic terms），几乎不会在合一过程中陷入无限递归。它内置了循环检测逻辑，当发现绑定会形成循环时，会用共享内存结构来表示这个循环项，而不是无限展开结构。比如你给出的所有示例，返回的都是合法的循环项结果，而非无限递归：

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

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

这些结果是Prolog用指针共享实现的，不会触发栈溢出或无限迭代。

那有没有可能触发合一过程的无限递归？答案是仅当使用自定义的、未添加循环检测的合一逻辑时。标准=/2已经做了完善的循环检测，但如果自己手动实现合一逻辑却忽略这一点，就会出现问题。比如下面这个简陋的自定义合一谓词：

my_unify(X, X).
my_unify(S1, S2) :-
    compound(S1), compound(S2),
    functor(S1, F, Arity), functor(S2, F, Arity),
    unify_args(S1, S2, 1, Arity).

unify_args(_, _, N, A) :- N > A.
unify_args(S1, S2, N, A) :-
    arg(N, S1, A1), arg(N, S2, A2),
    my_unify(A1, A2),  % 缺少循环检测，会触发无限递归
    Next is N + 1,
    unify_args(S1, S2, Next, A).

当你查询my_unify(foo(X), X)时，这个谓词会不断尝试展开foo(X)和X的绑定，没有终止条件，最终会导致栈溢出的无限递归。

另外，一些依赖深度遍历结构的内置谓词（比如默认设置下的write_canonical/1处理循环项时）会出现无限输出，但这是后续操作的递归问题，并非合一本身的问题。

二、为什么X = f(X), Y = f(Y).会将X和Y绑定？ #

这是因为Prolog的合一遵循**最一般合一（MGU, Most General Unifier）**的核心原则。当执行第一个目标X = f(X)时，X被绑定为循环项f(X)；执行第二个目标Y = f(Y)时，Prolog会寻找能同时满足两个目标的最通用的绑定方式。

如果让X和Y成为两个独立的循环项（比如X = f(X), Y = f(Y)作为分离的绑定），这确实是一个合法解，但不是最一般的。而将X和Y绑定为同一个循环项（即X = Y, Y = f(Y)）是更通用的解——它涵盖了X和Y完全相同的所有情况，而独立的解只是这个通用解的一个特例。

Prolog的合一器总是优先返回最一般的合一结果，所以会选择将X和Y绑定，而非生成两个独立的循环项。

内容的提问来源于stack exchange，提问作者Kim Mens