Prolog 中发生检查的简单最坏情况是什么？

如何解决Prolog 中发生检查的简单最坏情况是什么？

许多论文确实注意到，当 occurs_check=true 时，如下所示的等式统一问题可能会在指数时间内运行。没有规定这是顶级查询或子句主体，它只是等式统一问题：

   X1 = f(X0,X0),X2 = f(X1,X1),..
   Xn-1 = f(Xn-2,Xn-2),Xn = f(Xn-1,Xn-1).

如果为真，这可能是发生检查的最坏情况，因为正常变量共享统一是线性的。是否每个 Prolog 系统一定要把这个方程统一问题作为最坏的情况吗？

如果 Prolog 系统没有 occurs_check=true 标志，可以尝试用 unify_with_occurs_check/2 代替 (=)/2。

解决方法

这是一个比较。我在子句主体中测试了等式统一问题。链接到测试的源代码和基准测试结果位于此答案的末尾：

test :-
    B = f(A,A),C = f(B,B),D = f(C,C),X = f(D,D).

Etc..

Jekejeke Prolog 1.4.6 和 SWI-Prolog 8.3.17 仍然是线性的。 Jekejeke Prolog 使用静态分析，并不总是有效。 SWI-Prolog 是动态的，我猜是处理循环项的副作用。但是 GNU Prolog 1.4.5 是指数级的。我使用的是 n=4、6、8 和 10：

开源：

线性还是指数？
https://gist.github.com/jburse/2d5fd1d3dd8436acceca52fdfc537581#file-size-pl

尚未完全验证的假设。有一些确认我们可以查看VM代码。有我仍然存在的危险看，看，看，……我什么也没看到。

这是我对 SWI-Prolog 的怀疑。关于这个
等式统一问题，现在在子句主体中：

X1 = f(X0,X0),X2 = f(X1,X1),..
Xn-1 = f(Xn-2,Xn-2),Xn = f(Xn-1,Xn-1).

当出现_check=true 时，只有一个方程被优化掉？这会
解释不同的 LIPS 数量和不同的性能：

/* (=)/2,occurs_check=false */
% % 2,000,000 inferences,0.222 CPU in 0.226 seconds (98% CPU,9007995 Lips)

/* unify_with_occurs_check/2 */
% % 12,1.382 CPU in 1.411 seconds (98% CPU,8680009 Lips)

/* (=)/2,occurs_check=true */
% 11,1.264 CPU in 1.270 seconds (100% CPU,8704963 Lips)

Oki，Doki。