相关疑难解决方法(0)

在ISO Prolog中,仅针对NSTO(不受发生检查)的情况定义统一.背后的想法是涵盖那些主要用于程序并且实际上得到所有Prolog系统支持的统一案例.更具体地说,ISO/IEC 13211-1:1995读取:

7.3.3发生检查(STO)但不受
发生检查(NSTO)

如果存在通过
Herbrand算法的步骤以便
发生7.3.2g 的方式,则一组方程(或两个项)是"经历发生 - 检查"(STO).

如果没有办法继续
Herbrand算法的步骤使得7.3.2g发生,则一组方程(或两个项)"不受发生检查"(NSTO)
.

...

此步骤7.3.2 g读取:

克)如果存在形式的公式X =吨这样
即X是一个变量,吨是非可变术语
包含该变量,然后用失败(退出不
unifiable,正发生检查).

完整的算法被称为Herbrand算法,并且通常被称为Martelli-Montanari统一算法 - 其基本上通过以非确定性方式重写方程组来进行.

请注意,引入了新的方程式:

d)如果存在形式为f(a ₁,a ₂,... a _N)=
f(b ₁,b ₂,... b _N)的等式,则将其替换为等式集
a _i = b _我.

这意味着具有相同算符但具有不同arity的两个复合词将永远不会对STO-ness做出贡献.

这种非确定性使得STO测试难以实现.毕竟,仅仅测试是否需要发生检查是不够的,但为了证明对于执行算法的所有可能方式,这种情况永远不会发生.

这是一个案例来说明情况:

?- A/B+C*D = 1/2+3*4.

统一可以从A = 1,也可以是任何其他对开始,并以任何顺序继续.为了确保NSTO属性,必须确保没有可能产生STO情况的路径.考虑一个对当前实现没有问题的情况,但仍然是STO:

?- 1+A = …

引用SICStus Prolog 手册：

逻辑编程背后的常用数学理论禁止创建循环项，规定每次变量与项统一时都应进行发生检查。不幸的是，发生检查会非常昂贵，以至于使 Prolog作为一种编程语言变得不切实际。

但是，我运行了这些基准测试（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 …