许多论文确实指出,当 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 system necessarely 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:
开源:
线性还是指数?gist.github/jburse/2d5fd1d3dd8436acceca52fdfc537581#file-size-请
更多推荐
Prolog中发生检查的最坏情况是什么?
发布评论