Prolog 匹配 vs miniKanren 统一答案

【问题标题】：Prolog matching vs miniKanren unificationProlog 匹配 vs miniKanren 统一
【发布时间】：2016-02-18 11:39:34
【问题描述】：

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

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

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

【问题讨论】：

【解决方案1】：

这里有几个误解。首先，在 Prolog 中也可以使用 ISO 谓词 unify_with_occurs_check/2 进行声音统一。

其次，默认情况下，可以在某些 Prolog 系统中为 all 统一启用此声音统一。例如，参见 SWI-Prolog 中的 occurs_check Prolog 标志。

第三，很容易构建启用发生检查的示例，使您的程序顺序放大比禁用检查更快。

第四，使用术语匹配来描述省略发生检查的统一是一个非常糟糕的主意：匹配在函数式语言中意味着单向统一。在 Prolog 中，统一总是在各个方向上起作用，即使发生检查被禁用。

因此，对于问题的 Prolog 部分，如果您的 Prolog 系统支持，我强烈建议启用发生检查来测试您的程序。通常，发生检查的统一需要表示Prolog程序中的编程错误。出于这个原因，例如，您可以设置标志，使系统抛出一个异常，否则它会创建一个循环项。

【讨论】：

“需要发生检查的统一表示编程错误”：您可以更明确地说明这一点。我仍然需要看到一个需要循环术语的 Prolog 代码的一个很好的实际示例。你知道这样的例子吗？
一个相关问题：您能否展示或链接到实际示例，其中发生检查使程序更快，resp。慢点？我不得不承认我从未尝试过使用循环术语，而只是使用了香草统一（没有发生检查），因为我认为这无关紧要。
我曾经见过 Stefan Kral 对循环项的巧妙应用，他用循环项来表示图灵机的无限带（最初用0 填充），以Tape = [0|Tape] 开头，并从那里开始。有关 with 发生检查工作速度快数百倍的实际示例，请参阅 Ulrich Neumerkel 等人。 “Declarative Language Extensions for Prolog Courses”。
@Boris：无限树的“实用”示例是当前 SWI 中 CHR 的实现。
@Boris Coinduction 为循环项提供了一个很好的例子。参见例如github.com/LogtalkDotOrg/logtalk3/tree/master/examples/… 举几个例子。

【解决方案2】：

在 Prolog 中，发生检查是可选的。在 SWI Prolog 中，您可以将其全局打开、关闭或配置 Prolog 以在发生检查成功时引发error（这对于调试旨在在关闭发生检查的情况下运行的程序非常有用）

另一方面，在 miniKanren 中，发生检查是非可选的。

【讨论】：