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

当我想要研究逻辑编程的时候,我总是在两种“主要”的方法上磕磕绊绊:

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

24013 次浏览

试探性回答:

AFAIK,“理性的方案”引入了一种 Scheme-y 语法和函数式编程风格的基本逻辑编程,特别是在布尔值“ # t”和“ # f”中添加了常量目标“ # u”(失败)和“ # s”(成功)。它使用了与 Prolog 相同的逻辑编程方法: 统一和回溯搜索。我要看看周末是否有时间从书架上取回那本书。数学的分支是一个受限制的形式一阶逻辑,在这种情况下,号角子句,和解决统一。参见: 《计算逻辑: 过去的记忆》 《未来的挑战》约翰 · 艾伦 · 罗宾逊,罗伯特 · 科瓦尔斯基,逻辑编程的早期,冷启动

首先,请允许我赞美你的优秀品牌。

这是一个很难回答的问题,主要是因为 miniKanren 和 Prolog 都有很多变体。MiniKanren 和 Prolog 实际上是语言的家族,因此很难比较它们的特性,甚至难以比较它们在实践中的使用方式。因此,请谨慎对待我接下来要说的每一句话: 如果我说 Prolog 使用了深度优先搜索,请注意许多 Prolog 实现都支持其他搜索策略,而且替代的搜索策略也可以在 meta 解释器级别进行编码。不过,miniKanren 和 Prolog 有着不同的设计理念,并做出了不同的权衡。

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

Prolog 支持许多“超逻辑”或“非逻辑”特性,包括削减、 assertretract、使用 is进行算术变量投影等等。许多这些特性使得表达复杂的控制流和操作 Prolog 的全局事实数据库变得更加容易。Prolog 的一个非常有趣的特性是,Prolog 代码本身存储在全局事实数据库中,可以在运行时查询。这使得编写元解释器来修改解释下 Prolog 代码的行为变得很简单。例如,可以使用元解释器在 Prolog 中对广度优先搜索进行编码,从而改变搜索顺序。这是一个非常强大的技术,在 Prolog 世界之外并不为人所知。“序言的艺术”详细描述了这种技术。

在改进 Prolog 实现方面已经做出了巨大的努力,其中大部分都是基于 Warren 抽象机(WAM)的。WAM 使用一个副作用模型,其中值被破坏性地分配给逻辑变量,这些副作用在回溯时被撤销。通过扩展 WAM 的指令,可以向 Prolog 添加许多特性。这种方法的一个缺点是,如果对 WAM 没有扎实的理解,Prolog 实现文件可能很难阅读。另一方面,Prolog 实现者有一个讨论实现问题的通用模型。有大量的研究平行序言,在安道尔序言在20世纪90年代达到高潮。至少其中一些想法在 Ciao Prolog 仍然存在。(Ciao Prolog 充满了有趣的想法,其中许多远远超出了 Prolog 的标准。)

Prolog 有一个漂亮的基于统一的“模式匹配”样式的语法,它可以生成非常简洁的程序。Prologer 喜欢他们的语法,就像 Lispers 喜欢他们的 s 表达式一样。Prolog 还有一个大型的标准谓词库。由于所有的工程已经进入使 WAM 快速,有非常能干和成熟的 Prolog 实现。因此,许多大型知识推理系统完全是在 Prolog 撰写的。

MiniKanren 被设计成一种最小的逻辑编程语言,有一个小巧、易于理解和易于被黑客攻击的实现。MiniKanren 最初是嵌入在 Scheme 中的,在过去的十年中已经被移植到几十种其他主机语言中。最流行的 miniKanren 实现是 Clojure 的“ core.logic”,它现在有许多类似 Prolog 的扩展和许多优化。最近 miniKanren 实现的核心被进一步简化,产生了一个称为“ microKanren”的微型“微内核”然后可以在这个 microKanren 核心上实现 miniKanren。将 microKanren 或 miniKanren 移植到一种新的宿主语言已经成为学习 miniKanren 的程序员的标准练习。因此,大多数流行的高级语言至少有一个 miniKanren 或 microKanren 实现。

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

MiniKanren 实现的一个有趣的方面是,代码本身是线程安全的,并且——至少在理论上——可以平凡地并行化。当然,将代码并行化而不使其成为 慢一点并非易事,因为每个线程或进程都必须承担足够的工作,以弥补并行化的开销。尽管如此,这仍然是 miniKanren 实现的一个领域,我希望它能得到更多的关注和实验。

MiniKanren 使用出现检查进行统一,并使用完整的交错搜索而不是深度优先搜索。交错搜索比深度优先搜索搜索占用更多的内存,但是在某些情况下可以找到答案,在这种情况下深度优先搜索会永远发散/循环。MiniKanren 是的支持一些额外的逻辑运算符——例如,condaconduprojectcondacondu可以用来模拟 Prolog 的剪切,而 project可以用来获得与逻辑变量相关联的值。

condaconduproject的出现——以及轻松修改搜索策略的能力——允许程序员使用 miniKanren 作为嵌入式 Prolog 类语言。对于 Clojure 的“ core.logic”用户来说尤其如此,其中包括许多类似 Prolog 的扩展。这种对 miniKanren 的“务实”使用似乎占了 miniKanren 在工业中使用的大部分。如果程序员想在现有的用 Clojure、 Python 或 JavaScript 编写的应用程序中添加一个基于知识的推理系统,他们通常不会对在 Prolog 重写整个应用程序感兴趣。在 Clojure 或 Python 中嵌入一种小型逻辑编程语言要吸引人得多。一个嵌入式的 Prolog 实现大概也可以满足这个目的。我怀疑 miniKanren 之所以作为一种嵌入式逻辑语言而流行,是因为它有着微小而纯粹的核心实现,以及自《理性规划者》出版以来出现的演讲、博客文章、教程和其他教育材料。

除了将 miniKanren 用作与 Prolog 类似的实用的嵌入式逻辑编程语言之外,miniKanren 还被用于“关系”编程的研究。也就是说,在编写具有数学关系而不是数学函数行为的程序时。例如,在 Scheme 中,append函数可以附加两个列表,返回一个新列表: 函数调用 (append '(a b c) '(d e))返回列表 (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)关联起来,而调用 (append '(a b c) '(d e))0将 X(append '(a b c) '(d e))2与一对列表关联起来,这些列表在追加时等于 (a b c d e)。例如,X = (append '(a b c) '(d e))5和 (append '(a b c) '(d e))2 = (append '(a b c) '(d e))7就是这样一对值。我们还可以编写 (append '(a b c) '(d e))8,它将产生无限多个列表 X(append '(a b c) '(d e))2和 Z的三元组,以便将 X附加到 (append '(a b c) '(d e))2产生 Z

这个关系版本的 append可以很容易地在 Prolog 表达出来,实际上在许多 Prolog 教程中都有展示。在实践中,更复杂的 Prolog 程序倾向于使用至少一些额外的逻辑特性,比如 cut,这会抑制将生成的程序作为关系处理的能力。相比之下,miniKanren 的显式设计是为了支持这种类型的关系编程。最新版本的 miniKanren 支持符号约束求解(symbolonumberoabsento、不等式约束、名义逻辑编程) ,使得编写非平凡程序作为关系变得更加容易。在实践中,我从不使用 miniKanren 的任何额外的逻辑特性,并且我将所有 miniKanren 程序都写成关系式。最有趣的关系程序是 Scheme 子集的关系解释器。这些解释器有许多有趣的能力,比如生成一百万个 Scheme 程序,它们的计算结果是 (I love you)列表,或者生成一些琐碎的 quine (它们自己计算的程序)。

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

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

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

MiniKanren 的主要网站: Http://minikanren.org/

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

干杯,

威尔