问题标签 [occurs-check]

在 Prolog 中将谓词与未绑定变量进行比较是什么意思？

在 ISO Prolog 中，统一仅针对 NSTO（不受发生检查）的情况定义。背后的想法是涵盖那些主要用于程序中并且实际上被所有 Prolog 系统支持的统一案例。更具体地说，ISO/IEC 13211-1:1995 内容如下：

7.3.3 受发生检查（STO）和不受
发生检查（NSTO）

一组方程（或两个项）是“服从发生
检查”（STO），如果存在通过
Herbrand 算法的步骤进行的方法，使得 7.3.2 g
发生。

一组方程（或两项）是“不受
发生检查”（NSTO）的，如果没有办法继续执行
Herbrand 算法的步骤，从而
发生 7.3.2 g。

...

此步骤 7.3.2 g 内容如下：

g) 如果存在X = t形式的方程，其中
X是一个变量，t是一个包含该变量的非变量项
，则以失败退出（不可
统一，正发生检查）。

完整的算法称为 Herbrand 算法，也就是通常所说的Martelli-Montanari 统一算法——它本质上是通过以非确定性方式重写方程组来进行的。

请注意，新方程的引入如下：

d) 如果存在f(a ₁ ,a ₂ , ...a _N ) =
f(b ₁ ,b ₂ , ...b _N )形式的方程，则将其替换为方程组
a _i =我。_{_}

这意味着具有相同函子但不同元数的两个复合术语永远不会对 STO 产生影响。

这种不确定性是 STO 测试难以实施的原因。毕竟，仅测试是否需要发生检查是不够的，但要证明对于执行算法的所有可能方式，这种情况永远不会发生。

这里有一个案例来说明情况：

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

Prolog 系统首先将这个方程重写为：

现在，他们选择

• 1 = 2这使得算法失败退出，或者

• A = s(A)其中步骤 g 适用并且检测到 STO-ness。

我的问题是双重的。首先，它是关于 ISO Prolog 中的一个实现unify_sto(X,Y)（仅使用第 1 部分定义的内置函数），它适用于以下内容：

• 如果统一是 STO，则unify_sto(X,Y)产生错误，否则

• 如果unify_sto(X,Y)成功则也X = Y成功

• 如果unify_sto(X,Y)失败则也X = Y失败

我的第二个问题是关于在这种情况下发出的具体错误。请参阅 ISO 的错误类别。

这是一个简单的开始步骤：所有成功案例都包含在unify_with_occurs_check(X,Y). 剩下要做的是区分 NSTO 故障和 STO 错误情况。那是事情开始变得困难......

在 Prolog - 人工智能编程中，Bratko 在第 58 页说了以下内容。

“Prolog 中的匹配对应于所谓的逻辑统一。但是，我们避免使用统一这个词，因为在大多数 Prolog 系统中出于效率原因，匹配的实现方式并不完全对应于统一。正确的统一需要这样-称为发生检查：给定变量是否出现在给定术语中？发生检查会使匹配效率低下。

我的问题是 miniKanren 中的统一是否会遭受这种效率损失，或者这个问题是如何解决的？

是否有发生检查的差异？这在这里有效：

但上面是不可行的，因为发生检查是一个全局标志，我得到以下信息：

根据维基百科：

为所有统一提供声音统一的实现是 Qu-Prolog 和 Strawberry Prolog 以及（可选地，通过运行时标志）：XSB、SWI-Prolog和 Tau Prolog。

但是，当我这样做时，apropos(occur)它只会找到unify_with_occurs_check/2. 手册页也没有提到“发生” 。如何为 SWI-Prolog 中的所有统一启用发生检查？

As far as I can tell, with sound unification, SLD resolution should not create cyclic data structures (Is this correct?)

If so, one could, in theory, implement Prolog in such a way that it wouldn't need garbage collection (GC). But then again, one might not.

• Is this true for WAM-based Prolog implementations?

• Is this true for SWI-Prolog? (I believe it's not WAM-based) Is it safe to disable GC in SWI-Prolog when the occurs check is globally enabled?

Specifically:

我正在阅读的一篇论文说：

Plaisted [3] 表明，可以使用一阶谓词演算语义编写形式上正确的 PROLOG 程序，并得出诸如 3 < 2 之类的无意义结果。

它指的是Prologs当时（1980年代）没有使用发生检查的事实。

不幸的是，它引用的论文位于付费墙后面。我仍然希望看到这样的例子。直觉上，似乎省略了发生检查只是将结构的范围扩大到包括圆形结构（但根据作者的说法，这种直觉一定是错误的）。

我希望这个例子不是

那将令人失望。

编辑：这个问题假设您启用了发生检查。这与设置 Prolog 标志无关。

30 年前有一堆关于自动优化发生检查的论文，当它是安全的时（大约 90% 的谓词，在典型的代码库中）。提出了不同的算法。现代 Prolog 编译器（例如 SWI Prolog）是否会做类似的事情（当发生检查打开时）？他们喜欢什么算法？

例如，他们会在编译这样的谓词时删除发生检查：

（来自这个答案下面的讨论）

有这篇论文：

William E. Byrd、Eric Holk、Daniel P. Friedman，2012
miniKanren，
通过关系解释器实时和未标记的 Quines 生成
http://webyrd.net/quines/quines.pdf

它使用逻辑编程来查找 Scheme Quine。这里考虑的 Scheme 子集不仅包含 lambda 抽象和应用程序，还包含通过以下归约处理的小列表处理，已翻译为 Prolog：

因此，除了用于 lambda 抽象和绑定变量的 lembda 之外，唯一的符号是引号、[] 和 cons。我们将使用 Prolog 列表作为 Scheme 列表。目标是通过 Prolog 找到一个 Scheme 程序 Q，这样我们得到 Q ~~> Q，即对自身求值。

有一个复杂性，这使得努力变得不平凡，[lembda,X,Y] 不会在语法上对其自身进行评估，而是应该返回一个环境闭包。因此，评估器与此处的 Plotkin 评估器不同。

周围有任何 Prolog 解决方案吗？圣诞快乐

得到了这种奇怪的行为。我正在运行这些测试用例：

现在我得到了这些结果，其中的结果s2是错误的。结果在两个方面是错误的，第一个_3434被触发，第二个unify_with_occurs_check成功：

这_3434不应该从 ISO 核心标准中的 7.3.2 Herband 算法中触发。根据条款 7.3.2 f) 1) 变量 X 到项 t 的实例化仅在其 X 不在 t 中出现时传播。

根据第 7.3.2 g) 节，统一应该失败。因此，在 SWI-Prolog 中，诸如 freeze/2、dif/2 等各种形式的属性变量似乎会干扰 unify_with_occurs_check。

任何解决方法？

编辑 06.02.2021：
该错误已在 SWI-Prolog 8.3.17 (devel) 中修复，并且
也向后移植到 SWI-Prolog 8.2.4 (stable)。