SWI Prolog 使用什么发生检查优化？答案

【问题标题】：What occurs-check optimizations is SWI Prolog using?SWI Prolog 使用什么发生检查优化？
【发布时间】：2021-01-06 17:12:08
【问题描述】：

引用the SICStus Prolog manual：

逻辑编程背后的常用数学理论禁止创建循环项，指示发生检查应该是每次将变量与术语统一时完成。不幸的是，一个发生检查将非常昂贵，以至于 使 Prolog 不切实际 一种编程语言。

但是，我运行 these benchmarks（Prolog 的）并看到 SWI Prolog 中发生检查 (OC) 的开启和关闭之间存在相当小的差异（小于 20%）：

OC 关闭：:- set_prolog_flag(occurs_check, false). in .swiplrc（重新启动）

?- run_interleaved(10).
% 768,486,984 inferences, 91.483 CPU in 91.483 seconds (100% CPU, 8400298 Lips)
true.

?- run(1).
'Program'            Time     GC
================================
boyer               0.453  0.059
browse              0.395  0.000
chat_parser         0.693  0.000
crypt               0.481  0.000
fast_mu             0.628  0.000
flatten             0.584  0.000
meta_qsort          0.457  0.000
mu                  0.523  0.000
nreverse            0.406  0.000
poly_10             0.512  0.000
prover              0.625  0.000
qsort               0.574  0.000
queens_8            0.473  0.000
query               0.494  0.000
reducer             0.595  0.000
sendmore            0.619  0.000
simple_analyzer     0.620  0.000
tak                 0.486  0.000
zebra               0.529  0.000
           average  0.534  0.003
true.

OC 开启：:- set_prolog_flag(occurs_check, true). in .swiplrc（重新启动）

?- run_interleaved(10).
% 853,189,814 inferences, 105.545 CPU in 105.580 seconds (100% CPU, 8083669 Lips)
true.

?- run(1).
'Program'            Time     GC
================================
boyer               0.572  0.060
browse              0.618  0.000
chat_parser         0.753  0.000
crypt               0.480  0.000
fast_mu             0.684  0.000
flatten             0.767  0.000
meta_qsort          0.659  0.000
mu                  0.607  0.000
nreverse            0.547  0.000
poly_10             0.541  0.000
prover              0.705  0.000
qsort               0.660  0.000
queens_8            0.491  0.000
query               0.492  0.000
reducer             0.867  0.000
sendmore            0.629  0.000
simple_analyzer     0.757  0.000
tak                 0.550  0.000
zebra               0.663  0.000
           average  0.634  0.003
true.

这些基准是否不能代表实际使用情况？（我记得在某处读到它们被特别选为“相当有代表性”） SWI Prolog 是否实施了一些 SICStus 人不知道的优化技巧，这使得 OC 的成本很小？如果是这样，它们是否已发布？（我从 90 年代找到了一堆关于此的论文，但我不知道它们是否是最先进的）

【问题讨论】：

虽然我无法直接回答您的问题，但我们很高兴与 Jan Wielemaker（SWI Prolog 的创建者）在 SWI-Prolog Discourse (swi-prolog.discourse.group ) :-) 他相当活跃，所以我也可以建议您去那里。
这是交叉发布的here
@MostowskiCollapse 我的版本是 7.6.4 (Linux)。 current_prolog_flag(occurs_check, X) 同意 ~/.swiplrc 中的任何内容。
@MostowskiCollapse “试试这个：?- freeze(A,true),freeze(B,true),AB=s(A)-n.. 它会成功。” i> 我在 7.6.4 中看到一条错误消息（OC 设置为“错误”）。
@oguzismail：你在这里做的是破坏一个小标签。不，它对 Prolog 来说不仅仅是“有意义的”。与出现在很多地方的unification有关。

标签： prolog swi-prolog occurs-check

【解决方案1】：

主要优化使局部变量的统一成为一个常量操作。

许多abstract machines 像PLM、ZIP、WAM、VAM 为不能是某些结构的子项（称为局部变量）的逻辑变量提供了一种特殊情况。与这些变量的统一根本不需要任何发生检查，因此可以是恒定的。通过这种方式，可以“回传”大项，而无需进行额外的发生检查。

如果没有这种优化，语法处理（用于解析给定列表）的开销会在令牌数量上呈二次方。每次交回“输入列表”时（因此，从图形上讲，每次您在语法主体中的非终结符之后穿过逗号时），都需要扫描剩余的输入列表以查找该局部变量的出现。（在字符数上比二次方要好，因为正则表达式大多是尾递归编码的）。

此优化是在2007 in 5.6.39 引入的。令人惊讶的是，即使在像 tak 这样根本没有建造单一结构的情况下，您的测量结果也会显示开销。据我所知，SWI 5.6.39 中的发生检查统一比理性树统一（对于简单情况）运行得稍微快一点，因为（当时）不需要额外的设置。

仍有足够的空间进行许多进一步的发生检查优化。但是，只有当人们确实使用此功能时，才会发生这种情况。至于 SWI，在过去的 13 年里发生的事情并不多。

但是想一想：第一个 Prolog，称为 Prolog 0，默认情况下确实支持发生检查。但是从 Prolog I（“Marseille Prolog”）开始，只有借口（比如你引用的那些）。至少，该标准没有通过仅定义NSTO 执行并要求unify_with_occurs_check/2 和acyclic_term/1 来排除默认发生检查统一。而现在，像 SWI、Tau 和 Scryer 这样的 Prolog 可以选择通过标志提供它。

在同一方向上的进一步优化是 Joachim Beer 的 NEW_UNBOUND 标签，该标签避免了对某些堆变量的额外发生检查，但代价是更复杂的方案。看重新审视了发生检查问题。 JLP 5(3) 1988。和 LNCS 404。

【讨论】：

在 WG17 核心标准修订工作的背景下，ISO 早在 2009 就提出了该标志（后来缩短了名称）以进行标准化。希望更多的 Prolog 系统最终会实现它。
@PauloMoura：对标志有相当多的保留，因为如果将依赖于发生检查统一的代码和依赖于有理树的代码混合在一起，则很容易出错。一个这样的例子是 SWI 中的 CHR，它（在 10 年左右的当前实施中）依赖于创建无限树，因此不能在打开该标志的情况下一起运行。一个可能的（不完整的）解决方案可能是call_with_occurs_check/1。
我知道这些问题。 Coinduction 是另一个因打开此类标志而中断的代码示例。但是该标志的实现将/应该允许仅为需要发生检查的计算打开它（例如，使用setup_call_cleanup/3 目标）。这对于测试尤其有用。
不幸的是，setup_call_cleanup/3 用于此目的太粗糙了。需要为每次调用有效地维护该标志。但这意味着强加一些一般开销。而且，没有一个实现表明它并不难。
@MaxB：与那些案例无关。严肃地说，差异列表是 Prolog 的一个主要而不是“主要”点。在各种帖子中提到的那些发生检查的其他不良情况都依赖于术语的树与图表示，其中幼稚的遍历会获得指数开销。在早期的 LISP 用语中，这些是责备列表。在那里，散列表可能会很有趣。但不是简单的遍历，在那里，标记要便宜得多。一般来说，因式分解（基本上与有限自动机的最小化问题相同）总是会加快发生检查的速度。

【解决方案2】：

这是一个测试用例，其中发生检查的时间加倍执行查询。在这里使用此代码，以计算否定法线形式。由于 (=)/2 在规则的末尾，访问过的化合物变成二次方：

/* Variant 1 */
norm(A, R) :- var(A), !, R = pos(A).
norm((A+B), R) :- !, norm(A, C), norm(B, D), R = or(C,D).
norm((A*B), R) :- !, norm(A, C), norm(B, D), R = and(C,D).
Etc..

我们可以与这个变体进行比较，其中 (=)/2 先完成，而化合物尚未实例化：

/* Variant 2 */
norm(A, R) :- var(A), !, R = pos(A).
norm((A+B), R) :- !, R = or(C,D), norm(A, C), norm(B, D).
norm((A*B), R) :- !, R = and(C,D), norm(A, C), norm(B, D).
Etc..

以下是 SWI-Prolog 8.3.19 的一些测量结果。对于变体 1，将发生检查标志设置为 true 会使从数学原理转换一些命题公式所需的时间加倍：

/* Variant 1 */
/* occurs_check=false */
?- time((between(1,1000,_),test,fail;true)).
% 3,646,000 inferences, 0.469 CPU in 0.468 seconds (100% CPU, 7778133 Lips)
true.

/* occurs_check=true */
?- time((between(1,1000,_),test,fail;true)).
% 6,547,000 inferences, 0.984 CPU in 0.983 seconds (100% CPU, 6650921 Lips)
true.

另一方面，将 (=)/2 移到前面会有利地改变图片：

/* Variant 2 */
/* occurs_check=false */
?- time((between(1,1000,_),test,fail;true)).
% 3,646,000 inferences, 0.453 CPU in 0.456 seconds (99% CPU, 8046345 Lips)
true.

/* occurs_check=true */
?- time((between(1,1000,_),test,fail;true)).
% 6,547,000 inferences, 0.703 CPU in 0.688 seconds (102% CPU, 9311289 Lips)
true.

开源：

否定范式，非尾递归
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-norm-pl

否定范式，尾递归
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-norm2-pl

来自 Principia 的 193 个命题逻辑测试用例。
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-principia-pl

【讨论】：