Prolog 匹配 vs miniKanren 统一

Question

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

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

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

Answer 1

这里有几个误解。首先，Prolog 中也提供了声音统一，使用 ISO 谓词 unify_with_occurs_check/2 .

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

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

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

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