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

本文介绍了Prolog 中发生检查的简单最坏情况是什么?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

许多论文确实注意到，当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/2d5fd1d3dd8436acceca5752f1c#请