Prolog 和 miniKanren 在逻辑编程方面的主要技术差异是什么?

What are the main technical differences between Prolog and miniKanren, with respect to logic programming?

当我想阅读逻辑编程时,我现在总是偶然发现两种 "main" 方法:

我现在感兴趣的是:两者之间的主要技术差异是什么?它们在方法和实现上是否非常相似,或者它们是否采用完全不同的逻辑编程方法?它们来自哪些数学分支,有哪些理论基础?

暂定答案:

AFAIK,"The Reasoned Schemer" 介绍了 Scheme-y 语法和函数式编程风格中的基本逻辑编程,特别是将常量目标“#u”(失败)和“#s”(成功)添加到布尔值“#t”和“#f”。它使用与 Prolog 相同的逻辑编程方法:统一和回溯搜索。周末我会看看是否有时间从书架上取回那本书。数学分支是限制形式的一阶逻辑,在这种情况下是 Horn 子句和 Resolution Unfication。参见:计算逻辑:过去的记忆 John Alan Robinson 的 和 Robert Kowalski 的The early years of logic programming 的冷启动和未来的挑战。

首先,请允许我称赞您精美的 pw0n1e 图标。

这是一个很难回答的问题,主要是因为 miniKanren 和 Prolog 都有很多变体。 miniKanren 和 Prolog 实际上是语言家族,这使得很难比较它们的特性,甚至很难比较它们在实践中的使用方式。因此,请谨慎对待我要说的一切:如果我说 Prolog 使用深度优先搜索,请注意许多 Prolog 实现支持其他搜索策略,并且替代搜索策略也可以在 meta 中编码- 翻译水平。尽管如此,miniKanren 和 Prolog 有不同的设计理念,并做出不同的权衡。

Prolog是符号化人工智能编程的两种经典语言之一(另一种经典语言是Lisp)。 Prolog 擅长实现基于符号规则的系统,其中声明性知识以一阶逻辑编码。该语言针对这些类型的应用程序的表现力和效率进行了优化,有时会以牺牲逻辑纯度为代价。例如,默认情况下 Prolog 不统一使用 "occur check"。从 math/logic 的角度来看,这个版本的统一是不正确的。然而,发生检查是昂贵的,并且在大多数情况下缺少发生检查不是问题。这是一个非常务实的设计决定,就像 Prolog 使用深度优先搜索和使用 cut (!) 来控制回溯一样。我确信这些决定在 运行 在 1970 年代的硬件上运行时是绝对必要的,而今天在处理大型问题和处理巨大(通常是无限的!)搜索空间时非常有用。

Prolog 支持许多 "extra-logical" 或 "non-logical" 功能,包括剪切、assertretract、使用 is 进行算术变量投影等向前。许多这些特性使得表达复杂的控制流和操纵 Prolog 的全局事实数据库变得更加容易。 Prolog 的一个非常有趣的特性是 Prolog 代码本身存储在全局事实数据库中,并且可以在 运行 时间进行查询。这使得编写元解释器来修改解释下的 Prolog 代码的行为变得微不足道。例如,可以使用改变搜索顺序的元解释器在 Prolog 中对广度优先搜索进行编码。这是一种非常强大的技术,在 Prolog 世界之外并不为人所知。 'The Art of Prolog' 详细描述了此技术。

在改进 Prolog 实现方面付出了巨大的努力,其中大部分基于 Warren 抽象机 (WAM)。 WAM 使用副作用模型,其中值被破坏性地分配给逻辑变量,这些副作用在回溯时被撤销。通过扩展 WAM 的指令,可以将许多功能添加到 Prolog。这种方法的一个缺点是,如果对 WAM 没有透彻的理解,Prolog 实现论文可能很难阅读。另一方面,Prolog 实现者有一个共同的模型来讨论实现问题。对并行 Prolog 进行了大量研究,在 1990 年代在 Andorra Prolog 中达到顶峰。至少其中一些想法在 Ciao Prolog 中得以保留。 (Ciao Prolog 充满了有趣的想法,其中许多想法远远超出了 Prolog 的标准。)

Prolog 有一个漂亮的基于统一的 "pattern-matching" 风格的语法,可以生成非常简洁的程序。 Prologers 喜欢他们的语法,就像 Lispers 喜欢他们的 s 表达式一样。 Prolog 也有一个大型的标准谓词库。由于所有使 WAM 更快的工程,因此有非常强大和成熟的 Prolog 实现。因此,许多基于知识的大型系统完全用 Prolog 编写。

miniKanren 被设计为一种最小逻辑编程语言,具有小巧、易于理解且易于破解的实现。 miniKanren 最初嵌入在 Scheme 中,并在过去十年中被移植到其他几十种宿主语言中。最流行的 miniKanren 实现是 Clojure 中的 'core.logic',它现在有许多类似 Prolog 的扩展和一些优化。最近,miniKanren 实现的核心进一步简化,导致可以在这个 microKanren 核心之上实现一个名为 "microKanren." 的微型 "micro kernel" miniKanren。将 microKanren 或 miniKanren 移植到一种新的宿主语言已经成为程序员学习 miniKanren 的标准练习。因此,大多数流行的高级语言至少有一个 miniKanren 或 microKanren 实现。

miniKanren 和 microKanren 的标准实现不包含突变或其他副作用,只有一个例外:某些版本的 miniKanren 使用指针相等性来比较逻辑变量。我认为这是一个 "benign effect," 尽管许多实现通过在实现中传递一个计数器来避免这种影响。也没有全球事实数据库。 miniKanren 的实现理念受到函数式编程的启发:应避免突变和效果,所有语言结构都应尊重词法范围。如果仔细查看实现,您甚至可能会发现几个 monad。搜索实现基于组合和操作惰性流,同样没有使用变异。这些实现选择导致与 Prolog 中截然不同的权衡。在 Prolog 中,变量查找是常数时间,但回溯需要撤消副作用。在 miniKanren 中,变量查找更昂贵,但回溯是 "free." 实际上,由于流的处理方式,miniKanren 中没有回溯。

miniKanren 实现的一个有趣的方面是代码本质上是线程安全的,并且——至少在理论上——可以简单地并行化。当然,并行化代码而不使其 变慢 并不是微不足道的,因为必须为每个线程或进程提供足够的工作来弥补并行化的开销。不过,这是 miniKanren 实现的一个领域,我希望能得到更多的关注和试验。

mini看人统一使用occurrence check,使用完全交错搜索代替深度优先搜索。交织搜索比深度优先搜索使用更多的内存,但在深度优先搜索将永远 diverge/loop 的某些情况下可以找到答案。 miniKanren 支持一些额外的逻辑运算符---例如condaconduprojectcondacondu可以用来模拟Prolog的cut,project可以用来获取逻辑变量关联的值。

condaconduproject的存在---以及轻松修改搜索策略的能力---允许程序员将miniKanren用作嵌入式Prolog - 像语言。对于 Clojure 'core.logic' 的用户来说尤其如此,其中包括许多类似 Prolog 的扩展。这种 "pragmatic" miniKanren 的使用似乎占了 miniKanren 在工业中使用的大部分。希望将基于知识的推理系统添加到用 Clojure 或 Python 或 JavaScript 编写的现有应用程序的程序员通常对用 Prolog 重写他们的整个应用程序不感兴趣。在 Clojure 或 Python 中嵌入一种小型逻辑编程语言更具吸引力。据推测,嵌入式 Prolog 实现也可用于此目的。我怀疑 miniKanren 作为一种嵌入式逻辑语言变得流行,是因为其微小而纯粹的核心实现,以及自 'The Reasoned Schemer' 发布以来出现的演讲、博客文章、教程和其他教育材料。

除了将 miniKanren 用作与 Prolog 精神相似的实用嵌入式逻辑编程语言外,miniKanren 还用于 "relational" 编程研究。也就是说,在编写表现为数学关系而不是数学函数的程序时。例如,在 Scheme 中,append 函数可以追加两个列表,返回一个新列表:函数调用 (append '(a b c) '(d e)) returns 列表 (a b c d e)。但是,我们也可以将 append 视为三位关系而不是二元函数。然后,调用 (appendo '(a b c) '(d e) Z) 会将逻辑变量 Z 与列表 (a b c d e) 相关联。当然,当我们将逻辑变量放在其他位置时,事情会变得更有趣。调用 (appendo X '(d e) '(a b c d e))X(a b c) 相关联,而调用 (appendo X Y '(a b c d e))XY 与列表对相关联,这些列表在附加时是等于 (a b c d e)。例如 X = (a b)Y = (c d e) 就是一对这样的值。我们还可以编写 (appendo X Y Z),这将产生无限多的列表 XYZ 的三元组,这样将 X 附加到 Y产生 Z.

append 的这个关系版本可以很容易地用 Prolog 表达,并且确实在许多 Prolog 教程中都有展示。在实践中,更复杂的 Prolog 程序倾向于使用至少一些额外的逻辑特征,例如 cut,它抑制了将结果程序视为关系的能力。相比之下,miniKanren 明确设计为支持这种关系编程风格。 miniKanren 的最新版本支持符号约束求解(symbolonumberoabsento、不等式约束、名义逻辑编程),以便更轻松地将非平凡程序编写为关系。在实践中,我从不使用 miniKanren 的任何逻辑外功能,我将我所有的 miniKanren 程序都写成关系。最有趣的关系程序是 Scheme 子集的关系解释器。这些解释器有很多有趣的能力,例如生成一百万个评估列表 (I love you) 的 Scheme 程序,或者简单地生成 quines(对自己评估的程序)。

miniKanren 做出了许多权衡来启用这种关系编程风格,这与 Prolog 所做的权衡非常不同。随着时间的推移,miniKanren 添加了更多的符号约束,真正成为一种面向符号的约束逻辑编程语言。在许多情况下,这些符号约束使得避免使用像 conduproject 这样的额外逻辑运算符变得切实可行。在其他情况下,这些符号约束是不够的。更好地支持符号约束是 miniKanren 研究的一个活跃领域,还有更广泛的问题,即如何编写更大、更复杂的程序作为关系。

简而言之,miniKanren 和 Prolog 都有有趣的特性、实现和用途,我认为两种语言的思想都值得学习。还有其他非常有趣的逻辑编程语言,例如 Mercury、Curry 和 Gödel,每种语言都有自己的逻辑编程。

我将以一些 miniKanren 资源作为结尾:

迷你看人网主要网站: http://minikanren.org/

我对关系编程和 miniKanren 的采访,包括与 Prolog 的比较: http://www.infoq.com/interviews/byrd-relational-programming-minikanren

干杯,

--威尔