问题描述
SWI-Prolog 的源代码说，部署的统一是基于 Bart Demoen 的一些想法。 SWI-Prolog 统一的核心确实检测重复出现的化合物，因此可以处理循环项。但是当不涉及循环项时，也会检测到重复出现的化合物。
后面的特征使得非循环项的统一在时间上是线性的。但我不能 100% 确定 Wielemaker-Demoen 统一对于非循环项是否真的在时间上是线性的？
一种已知的时间线性算法是 Paterson-Wegman 统一。它在输入方程系统大小上是线性的。 Paterson-Wegman 统一大放异彩的一个典型例子是这里的这个例子，天真的统一变得指数化：
X1 = f(X0,X0),X2 = f(X1,X1),..
Xn-1 = f(Xn-2,Xn-2),Xn = f(Xn-1,Xn-1).
Y1 = f(Y0,Y0),Y2 = f(Y1,Y1),..
Yn-1 = f(Yn-2,Yn-2),Yn = f(Yn-1,Yn-1).
Xn = Yn
这是使用 n=4,6,8,10 使用 SWI-Prolog 和 GNU Prolog 进行的测试。使用 SWI-Prolog：
SWI-Prolog (threaded,64 bits,version 8.3.17)
?- run.
% 200,000 inferences,0.031 CPU in 0.032 seconds (98% CPU,6400000 Lips)
% 200,0.047 CPU in 0.042 seconds (112% CPU,4266667 Lips)
% 200,0.063 CPU in 0.055 seconds (114% CPU,3200000 Lips)
% 200,0.063 CPU in 0.064 seconds (98% CPU,3200000 Lips)
true.
使用 GNU-Prolog：
GNU Prolog 1.4.5
?- run.
% 36 ms
% 74 ms
% 206 ms
% 738 ms
当面对非循环项时，SWI-Prolog 本质上是否实现了 Paterson-Wegman 统一？另一个在上面的例子中表现良好的 Prolog 系统是 YAP 6.3.3，但我没有检查它们的来源以获得一些参考。
开源：
线性还是指数 II？
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-paterson-pl
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）