问题描述
许多论文确实注意到，当occurs_check=true 时，如下所示的等式统一问题可能会在指数时间内运行.没有规定这是顶级查询或子句主体，它只是等式统一问题:
Many papers do note that an equational unification problem such as below, might run in exponential time, when occurs_check=true. There is no stipulation that this is a top-level query or a clause body, its just the equational unification problem:
X1 = f(X0, X0),
X2 = f(X1, X1),
..
Xn-1 = f(Xn-2, Xn-2),
Xn = f(Xn-1, Xn-1).
如果为真，这可能是发生检查的最坏情况，因为正常变量共享统一是线性的.是否每个 Prolog 系统一定要把这个方程统一问题作为最坏的情况吗?
If true this could be a worst case for occurs check, since normal variable sharing unification is linear. Does every Prolog systemnecessarely feature this equational unification problem as a worst case?
如果 Prolog 系统没有 occurs_check=true 标志，可以尝试用 unify_with_occurs_check/2 代替 (=)/2>.
If the Prolog system does not have an occurs_check=true flag, one could try unify_with_occurs_check/2 in place of (=)/2.
推荐答案
这里有一个比较.我在子句主体中测试了等式统一问题.链接到测试的源代码和基准测试结果位于此答案的末尾:
Here is a comparison. I tested the equational unification problem inside a clause body. Link to source code of the test and the benchmark results is at the end of this answer:
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:
Jekejeke Prolog 1.4.6 and SWI-Prolog 8.3.17 is still linear. Jekejeke Prolog uses a static analysis, doesn't work always. SWI-Prolog does it dynamically, I guess side effect of dealing with cyclic terms. But GNU Prolog 1.4.5 is exponential. I was using n=4, 6, 8 and 10:
开源:
线性还是指数?
https://gist.github.com/jburse/2d5fd1d3dd8436acceca5752f1c#请
这篇关于Prolog 中发生检查的简单最坏情况是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！