prolog - Prolog 匹配 vs miniKanren 统一

Question

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

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

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

score 5 · Accepted Answer

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

其次，默认情况下，可以在某些 Prolog 系统中为所有统一启用这种声音统一。例如，参见occurs_checkSWI-Prolog 中的 Prolog 标志。

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

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

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

score 2 · Accepted Answer

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

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

2 回答 2