问题标签 [occurs-check]

事实证明，SICStus Prolog 没有occurrence_check Prolog 标志。至少我们找不到，这里给出了一条错误消息：

看起来“true”的值不是问题，关键的统一可以通过现有的内置unify_with_occurs_check/2. 一个发生检查 Prolog 标志的一个有趣的值是值“错误”。

如何实现谓词unify_with_occurs_check_and_error/2？请注意，unify_with_occurs_check_and_error/2 的解决方案应该表现得像 unify_with_occurs_check/2，即不触发属性变量。

以下是 Prolog 标志的示例用法：

这就是在 SICStus Prolog 中要做的事情：

引用SICStus Prolog 手册：

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

但是，我运行了这些基准测试（Prolog 的），并在 SWI Prolog 中发现发生检查（OC）打开和关闭之间存在相当小的差异（小于 20%）：

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

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

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

许多论文确实指出，如下所示的等式统一问题可能在指数时间内运行，当occurs_check=true. 没有规定这是顶级查询或子句主体，它只是等式统一问题：

如果为真，这可能是发生检查的最坏情况，因为正常的变量共享统一是线性的。是否每个 Prolog 系统都必须将这个方程统一问题作为最坏的情况？

如果 Prolog 系统没有occurs_check=true标志，可以尝试unify_with_occurs_check/2代替(=)/2.

我正在使用以下代码临时更改发生检查标志，其中 G 是一个不会创建任何延迟目标的目标：

下面是 with_occurs_check/1 的一个期望方面，因为我们希望所有回溯到目标 G 工作，并将发生检查标志设置为 true。最好只在创建选择点后，在 SWI-Prolog 中可以看到“;” 只问一次而不是两次：

但有一个警告。当 G 是非确定性的时，上述内容实际上并不适用。如果 G 有一个带有剩余选择点的出口端口，setup_call_cleanup/3将不会调用它的清理。因此发生的检查标志更改将泄漏到延续中：

有没有更安全的方法来临时更改发生检查？

我遇到以下情况：

为什么统一适用f(X) = X，但不适用f(a) = a？是不是因为第一个简单地说是f(X)as的名称返回值X，而第二个试图检查返回值是否f(a)是a？但是f()这里没有定义！！另外，我想，序言中没有“返回值”这样的概念。那么，这里发生了什么？

一个人将如何setarg_with_occurs_check/3在
Prolog 中进行引导。Prolog 似乎有两种方法来创建循环数据结构。
不仅统一可以做到这一点，setarg/3 也可以：

可以说我想要unify_with_occurs_check/2for的类似物
setarg/3。一个人将如何进行并实施相同的？

（顺便说一句，在某些 Prolog 系统中，setarg/3 有时使用
名称 change_arg/3，有些甚至根本没有）