微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦!

SWI Prolog 使用什么发生检查优化?

如何解决SWI Prolog 使用什么发生检查优化?

引用the SICStus Prolog manual

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

但是,我运行了 these benchmarks(Prolog 的那些)并且发现 SWI Prolog 在打开和关闭发生检查 (OC) 之间有相当小的差异(小于 20%):

OC 关闭:- set_prolog_flag(occurs_check,false). 中的 .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). 中的 .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 年代找到了一堆关于这个的论文,但我不知道它们是否是最先进的)

解决方法

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

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

如果没有这种优化,语法处理(用于解析给定列表)会在标记数量上获得二次开销。每次交回“输入列表”时(因此,从图形上讲,每次在语法正文中的非终结符之后跨一个逗号时),都需要扫描剩余的输入列表以查找该局部变量的出现。 (它在字符数上比二次方好,因为正则表达式大多是尾递归编码的)。

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

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

但是想一想:第一个 Prolog,称为 Prolog 0,默认支持发生检查。但是从序言 I(“马赛序言”)开始,只有借口(例如您引用的那些)。至少,标准没有排除默认的发生检查统一,只定义 NSTO 执行并要求 unify_with_occurs_check/2acyclic_term/1。现在,像 SWI、Tau 和 Scryer 这样的 Prolog 可以通过标志选择性地提供它。

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

,

这是一个测试用例,其中发生检查使时间加倍 执行查询。把这段代码放在这里,计算一个否定法线 形式。由于 (=)/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 = and(C,D).
Etc..

我们可以与此变体进行比较,其中 (=)/2 在复合尚未实例化时首先完成:

/* Variant 2 */
norm(A,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,fail;true)).
% 6,547,0.984 CPU in 0.983 seconds (100% CPU,6650921 Lips)
true.

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

/* Variant 2 */
/* occurs_check=false */
?- time((between(1,0.453 CPU in 0.456 seconds (99% CPU,8046345 Lips)
true.

/* occurs_check=true */
?- time((between(1,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

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。