Prolog匹配vs miniKanren统一 [英] Prolog matching vs miniKanren unification

问题描述

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

In Prolog - Programming for Artificial Intelligence, Bratko says the following on page 58.

"Prolog中的匹配对应于逻辑上的统一.但是，我们避免使用统一一词，因为出于效率原因，在大多数Prolog系统中，匹配的实现方式并不完全对应于统一.需要所谓的发生检查:给定变量是否在给定条件下出现?发生检查会使匹配效率低下."

"Matching in Prolog corresponds to what is called unification in logic. However, we avoid the word unification because matching, for for efficiency reasons in most Prolog systems, is implemented in a way that does not exactly correspond to unification. Proper unification requires the so-called occurs check: does a given variable occur in a given term? The occurs check would make matching inefficient."

我的问题是，miniKanren中的统一会遭受这种效率损失还是如何解决?

My questions is if unification in miniKanren suffers this efficiency penalty or how is this problem solved?

推荐答案

这里有一些误解.首先，使用ISO谓词unify_with_occurs_check/2在Prolog中也可以实现声音统一.

There are several misconceptions here. First, sound unification is available also in Prolog, using the ISO predicate unify_with_occurs_check/2.

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

Second, this sound unification can be enabled in some Prolog systems by default for all unifications. See for example the occurs_check Prolog flag in SWI-Prolog.

第三，构造示例很容易，在这些示例中，启用发生检查比禁用检查可以更快地使您的程序顺序变得更容易.

Third, it is easy to construct examples where enabling the occurs check makes your program orders of magnituted faster than disabling the check.

第四，使用术语 matching 来描述省略事件检查的统一是一个非常糟糕的主意: Matching 表示功能语言中的单向统一.在Prolog中，即使禁用了发生检查，统一也始终在所有方向上起作用.

Fourth, using the term matching to describe unifications that omit the occurs check is a very bad idea: Matching means one-way unification in functional languages. In Prolog, unifications always work in all directions, also if the occurs check is disabled.

因此，对于问题的Prolog部分，如果您的Prolog系统支持，我强烈建议启用发生检查以测试您的程序.通常，要求进行统一检查的统一表示Prolog程序中存在编程错误.因此，您可以设置标志，例如系统抛出 exception ，否则将创建循环项.

So, for the Prolog part of the question, I highly recommend to enable the occurs check to test your programs, if your Prolog system supports it. Usually, a unification where an occurs check is required indicates a programming error in Prolog programs. For this reason, you can for example set the flag in such a way that the system throws an exception where it would otherwise create a cyclic term.

这篇关于Prolog匹配vs miniKanren统一的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！