Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

侦探指南：如何让事物匹配

想象你是一名侦探，正试图破解一个谜案：两个不同的犯罪现场描述实际上必须是同一事件。一位目击者说：“嫌疑人戴着红帽子，穿着蓝外套。”另一位目击者说：“嫌疑人戴着红帽子，穿着蓝外套。”这很简单，对吧？但如果第二位目击者说：“嫌疑人戴着红帽子，穿着蓝外套，但那顶帽子其实是蓝外套的一个伪装”呢？现在你必须弄清楚，是否可以通过用正确的数值替换掉这些“变量”（比如特定的颜色或物品），使这两个故事能够达成一致。在计算机科学的世界里，这个谜题被称为合一（unification）。它是驱动从下棋的人工智能到检查代码编写是否正确的软件等一切事物的引擎。

几十年来，计算机科学家一直试图教机器自动解决这个谜题。目标不仅仅是让计算机说“是的，它们匹配”，而是要让计算机发明出匹配它们的步骤式配方（即算法）。这被称为演绎程序综合（deductive program synthesis）。可以把它想象成要求一个超级聪明的机器人去证明一个数学定理，但它不只是在最后写下“证毕（Q.E.D.）”，而是必须交给你一段能够解决问题的可用软件。难点在于？机器人必须绝对确定该软件是正确的，因为证明本身就是保证。如果证明成立，程序就有效；如果证明失败，程序就是垃圾。

论文的核心发现：教机器人构建自己的解谜器

这篇由理查德·沃尔丁格（Richard Waldinger）撰写的论文讲述了一个关于名为 Snark 的机器人的故事。Snark 被要求仅利用逻辑规则，从零开始构建一个合一算法。作者并没有直接把答案交给 Snark，而是给了它一套逻辑规则（一个“公理理论”）和一个目标：“寻找一个能使这两个表达式变得完全相同的替换方案。”

该论文的主要发现是，Snark 成功地自动推导出了一个可用的合一算法。它不仅仅是复制了一个旧算法，而是发现了一个比以往某些人工尝试更高效、更易于理解的新版本。机器人通过将创建程序的过程视为一个巨大的逻辑谜题来完成这一任务。它从一个模糊的目标开始，通过一个拆解问题为更小案例的过程（例如“如果第一个项是一个常量？”或“如果它是一个变量？”），构建了一个复杂的“if-then-else”决策树。这棵树就是最终的程序。

论文明确排除了这仅仅是一个简单的单步技巧的观点。作者承认，这个过程需要大量的“人工帮助”，形式包括设定正确的逻辑规则以及选择正确的“良基关系”（well-founded relations，这是一种高级说法，意指确保机器人不会陷入死循环的规则）。论文还反对认为合一是一个简单、直接的问题的看法。正如论文中的一段话所言：“当尝试进行彻底的陈述时，人们会意识到这个问题相当微妙且充满陷阱。”论文并未声称这解决了所有的程序综合问题，也没有声称它是所有软件工程的灵丹妙药。相反，它将此作为一个成功的案例研究，证明了全自动推导复杂算法是可能的，尽管对于许多其他类型的程序来说，这仍然是一个研究目标。

机器人是如何“思考”的

要理解 Snark 是如何做到这一点的，想象你正在教一个孩子分类乱七八糟的玩具。你不会只说“分类”。你会给他们一套规则：“如果是积木，把它放进红筐；如果是车，把它放进蓝筐。”但如果这个玩具既是积木又是车呢？你也需要一条针对这种情况的规则。

Snark 使用了一种称为**演绎表格法（dedctive tableaux）**的方法。想象一个白板，有两个列：“我们已知的”（断言）和“我们需要寻找的”（目标）。

1. 目标： “找到一种方法，使表达式 A 和表达式 B 看起来一样。”
2. 过程： Snark 查看目标并询问：“如果 A 是一个变量怎么办？如果它是一个常量怎么办？”它将问题拆分为这些不同的“案例”。
3. “顿悟”时刻： 当 Snark 意识到要解决一个大问题，它可能需要先解决一个较小的同类问题时，它引入了递归（recursion）。这就像是在说：“为了整理这堆大玩具，我先整理左半部分，然后再整理右半部分，最后把它们合并起来。”论文解释说，Snark 在这里必须非常小心，以确保它不会陷入无限循环。它使用了一个“良基关系”（一种数学保证，确保每一步都使问题严格变小，就像从 100 倒数到 0 一样），以此来证明过程最终会停止。

“环境”的小技巧

论文中最巧妙的举措之一是稍微改变了问题，使其更容易被机器人解决。与其仅仅问“如何匹配 A 和 B？”，不如问 Snark：“在已知你已经拥有一个之前的匹配列表的情况下，如何匹配 A 和 B？”这个列表被称为环境（environment）。

这就像是在玩“老师说（Simon Says）”的游戏。如果老师说“摸鼻子”，你就去做。但如果老师在说了“戴上帽子”之后又说“摸鼻子”，你就必须记住帽子，同时还要执行摸鼻子的动作。通过记录“环境”（帽子），机器人可以构建出一个更高效的算法。论文指出，这个三参数版本（表达式 A、表达式 B 和环境）实际上比人类通常使用的简单的两参数版本更容易让计算机自动合成。

最终结果：一个新的配方

论文以展示 Snark 生成的实际代码作为结尾。它看起来像是一长串“如果……那么……”的指令。

• 如果环境损坏，返回“失败”信号。
• 如果两个表达式已经相同，则返回当前的匹配列表。
• 如果一个是变量而另一个是常量，则创建一个新的规则来进行交换。
• 如果两者都是复杂的结构（例如一个项目列表），则将其拆分为左侧和右侧部分，先解决左侧部分，然后利用该结果来解决右侧部分。

论文强调，这个程序是可证明正确的。因为程序是直接从逻辑证明中提取出来的，所以我们知道它是有效的。如果证明说“这一步是有效的”，那么代码步骤也是有效的。作者指出，虽然整个证明过程大约耗时 10 秒钟才被 Snark 系统找到，但其真正的价值在于方法论：它表明我们可以通过证明定理来构建软件，而不是仅仅靠猜测和尝试。

为什么这很重要（以及为什么它还不是魔法）

论文以对未来的幽默致敬结束。它提到，虽然现代 AI（如大语言模型）可以编写代码，但它们有时会“幻觉”或编造事实。它们可能会写出一个看起来正确但带有隐藏漏洞的程序。相比之下，演绎综合更像是数学证明：如果步骤正确，结果必然正确。

作者建议了一个未来，在那里我们可以将这两个世界结合起来：利用聪明的 AI 来协助设置逻辑规则和证明中的“猜测”，然后使用严谨的定理证明器来验证最终结果。但就目前而言，这篇论文是逻辑力量的见证：一台机器能够观察一个复杂且棘手的问题，并一步步地发明出自己的解决方案，证明了通往完美软件的路径或许正是纯数学之路。