Prolog匹配与miniKanren统一

Question

在Prolog -人工智能编程中，Bratko在第58页上写道。

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

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

Answer 1

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

第二，在某些Prolog系统中，对于所有的统一，默认情况下可以启用这种声音的统一。例如，请参见SWI中的occurs_check Prolog标志。

第三，很容易构造示例，在这些示例中，启用发生检查比禁用检查更快地使您的程序排序更快。

第四，使用术语匹配来描述省略发生检查的统一是一个非常糟糕的想法:匹配意味着功能语言中的单向统一。在Prolog中，统一始终在各个方向工作，如果已发生的检查被禁用，则也是如此。

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