Yaron Minsky 在 Curry On 谈软件验证的计算复杂度难题

我很高兴能再次在 Curry On 上发表演讲。去年，在我们与 Quasar 合作之后，我讲了续延与 monad 的对比。今年，我讲的是软件验证中的计算复杂性结果——这是我在形式化规约并验证我们即将推出的新版 Galaxy 时产生兴趣的课题。以下是演讲的扩展版本（视频嵌入在上方），包含了一些我因时间关系未能覆盖的额外证明和结果，并附有脚注，供希望进一步研究这些主题的读者参考。阅读时间：约 45 分钟。

在本文中，我们试图理解程序与正确性之间的关系，特别是为什么编写正确的程序如此困难。我们将回顾可计算性理论和复杂性理论中的结果，并看到程序与完整理解——而完整理解正是正确性所必需的——在根本上是相互矛盾的。本文的主要贡献在于将一些与生产正确软件的本质困难相关的结果（以及一些参考文献）汇总在一处。我的动机是我在网上找到的各种说法（比如这个，尽管它远非唯一一个），它们声称借助正确的工具就能轻松实现软件正确性。虽然某些工具确实能够（而且确实）协助确保程序正确，但正确性需要付出巨大的代价。正确性的代价——就像减少熵的能量代价一样——是计算的“自然法则”所导致的结果，不可能被避免。

理论计算机科学的故事始于大约一百年前。随着数理逻辑的日益成功，数学家 David Hilbert 提出了一项将全部数学形式化的纲领。他希望证明形式系统的一致性和完备性，并找到一个判定程序——一种用于确定每个形式陈述真假的算法： Hilbert 相信，任何能够被形式推理的事物也能够被完全理解，我指的是其所有性质都能被证明。 19 世纪关于知识界限的观点可以用格言“ignoramus et ignorabimus”来表达，意思是“我们不知道，而且我们永远不会知道”。1930 年，Hilbert 在退休之际，于柯尼斯堡向德国科学家与医师协会发表了一场题为“Naturerkennen und Logik”（逻辑与对自然的理解）的演讲，在演讲中他挑战了这一观点。他说： 对于数学家来说，不存在 Ignorabimus，而且在我看来，对于自然科学也完全不存在。……在我看来，[没有人]成功找到一个不可解问题的真正原因，是不存在不可解的问题。与愚蠢的 Ignorabimus 相反，我们的信条是：我们必须知道，我们将会知道！1 这些话——Wir müssen wissen. Wir werden wissen——被刻在了他的墓碑上。 Hilbert 当时并不知道，他的纲领在前一天就已经被摧毁了，当时 Kurt Gödel 试探性地宣布了他的第一不完备性结果2。 Gödel 的不完备性定理摧毁了 Hilbert 纲领的前两根支柱（有人说也摧毁了第三根，只是他没有意识到3），而在 1936 年，Church 和 Turing 用今天被称为停机定理的证明击碎了第三根支柱——判定问题。 停机定理——计算机科学的第一个定理——在 1936 年 Alonzo Church4 和 Alan Turing5 的论文中分别得到了证明。这个定理对于计算的本质而言如此基础，以至于它与计算的两种表述同时出现绝非偶然。该定理指出，不存在一种算法能够判定任意给定程序是否会终止。证明（此处给出的是简化形式）基于对角化或自引用的思想，这与 Gödel 在其不完备性证明中使用的思想相同。 H(M, x) := IF M halts on x THEN TRUE ELSE FALSE 然后我们可以很容易地构造 $G$： G(y) := IF H(y, y) = FALSE THEN TRUE ELSE loop forever 如果我们然后把 $G$ 传递给自身（$G(G)$），我们就会得到 $G$ 的行为与 $H$ 所说的 $G$ 的行为之间的矛盾。 有趣的是，停机定理直接导出了 Gödel 第一不完备性定理的一个版本。证明简单地说6：假设对于每个真陈述，在某个逻辑理论（基本上是一组公理）中都有一个逻辑证明。那么，给定一个程序，从那些公理出发，我们可以通过逻辑演绎逐一枚举所有定理。因为所有陈述的数量——更不用说所有定理的数量——是可数的，而且因为每个陈述要么有证明要么其否定有证明，我们最终会找到其中一个的证明。因此，给定一个程序，我们可以开始枚举所有定理，直到找到一个表明该程序终止的定理，或者一个表明它不终止的定理，从而违反停机定理。 然而，停机定理还有一些其他直接推论，将它们与软件验证问题——我们的主要关注点——更直接地联系起来。第一个是关于可达性的简单结果。 不存在一个程序 R，当给定一个程序 M、一组初始状态 I 和状态配置 S 时，能够判定 M 从 I 中的某个状态出发是否曾经到达 S。 证明是从停机问题出发的一个简单归约：如果存在这样的算法，我们可以问它从输入 x 出发是否曾经到达停机状态，从而解决停机问题7。 一个更有趣的推论是 Rice 定理。程序可以计算所谓的部分函数。如果它们在给定输入时停止，我们认为写在纸带上的输出映射到初始输入；如果它们对给定输入永不停止，我们认为该输入未被映射。Rice 定理指出： 对于部分函数的任何非平凡性质，没有任何算法能够判定一个程序（图灵机）M 是否计算了一个具有该性质的部分函数。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）