prolog - Prolog中发生检查的最坏情况是什么？

Question

许多论文确实指出，如下所示的等式统一问题可能在指数时间内运行，当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.

标签： prologoccurs-check

Answer 1

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

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