为什么编写正确的软件很难

为什么编写正确的软件很难

发布日期：2016年7月23日

数学无法单独解决软件正确性问题

在正式规范与验证领域，计算复杂性理论揭示了程序正确性的根本局限。尽管现代工具（如 Quasar 等）能辅助确保程序行为符合预期，但实现“完全正确”的软件面临着巨大的成本。这种成本并非源于工程实践的疏忽，而是计算自然规律的直接结果。

本文旨在梳理可计算性理论与复杂性理论中的关键结论，阐明为何对程序及其正确性要求的完全理解在本质上是不一致的。通过回顾希尔伯特计划、哥德尔不完备定理、图灵停机问题以及赖斯定理等经典成果，我们将看到：程序的正确性验证不仅困难，在某些情况下甚至是不可能的。

第一章：理论基础与不可判定性

理论计算机科学的历史始于约一百年前。当时，数学家大卫·希尔伯特提出了著名的“希尔伯特计划”，试图将所有数学形式化。该计划包含三个核心目标：

一致性：证明形式主义体系中不存在矛盾。
完整性：所有真实的数学命题均可在该体系内被证明。
可决定性（Entscheidungsproblem）：存在一个算法，能够判定任意形式陈述的真伪。

希尔伯特坚信，凡是可以被形式推理的事物，必然可以被完全理解。他在1930年的演讲中反驳了“我们不知道，我们也不会知道”的悲观论调，留下了著名的格言：“我们必须知道，我们必将知道。”然而，在他发表这一宣言的前一天，其计划的核心支柱已被逻辑学突破所瓦解。

库尔特·哥德尔的不完备性定理摧毁了希尔伯特计划的前两个支柱。随后，阿隆佐·丘奇和艾伦·图灵在1936年分别独立证明了“停机问题”不可判定，从而打破了第三个支柱——决策问题。

停机问题与对角线论证

停机问题是计算理论中最基本的定理之一。它指出：不存在任何算法，能够决定任意给定的程序在特定输入下是否会终止。

假设存在这样一个判定程序 $H$：

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)$）时，会产生逻辑矛盾：如果 $H$ 判定 $G(G)$ 会停机，则 $G$ 进入无限循环；如果 $H$ 判定 $G(G)$ 不停机，则 $G$ 立即返回 TRUE 并停机。因此，假设存在的 $H$ 不可能成立。

有趣的是，停机问题的证明过程可以直接推导出哥德尔第一不完备定理的一个版本。如果每个真实陈述都有逻辑证明，且定理集合是可数的，我们可以通过枚举所有定理来判定程序是否停机，这再次违反了停机定理。

赖斯定理与程序属性

停机定理衍生出若干直接影响软件验证的结论。首先是关于可达性的简单推论：

不存在一个程序 $R$，给定程序 $M$、初始状态集 $I$ 和状态配置 $S$，能确定 $M$ 是否在从 $I$ 中某状态开始时达到 $S$。

更深刻的结论是赖斯定理（Rice's Theorem）。程序计算的是部分函数，赖斯定理指出：

对于部分函数的任何非平凡属性，不存在算法可以决定某个图灵机 $M$ 计算的函数是否具有该属性。

例如，没有算法能判断程序的输出是否总是输入的平方。这意味着，除了极少数平凡情况外，我们无法通过静态分析自动验证程序的行为特性。

忙碌海狸函数与定量难度

为了量化分析程序的复杂性，我们可以引入“忙碌海狸”（Busy Beaver）概念。定义函数 $f(n)$ 为拥有 $n$ 个控制状态的图灵机在停机前可能采取的最大步数。

$f(n)$ = 具有 $n$ 个控制状态的停机图灵机在停止前执行的最大步骤数

该函数是不可计算的。若 $f(n)$ 可计算，我们便可结合停机判定逻辑来解决停机问题，导致矛盾。事实上，任何已知大于 $f(n)$ 的函数也是不可计算的。

类似地，从静态视角看，定义 $g(n)$ 为证明大小为 $n$ 的图灵机停机的最短证明的最大长度。$g(n)$ 同样不可计算。这两个函数揭示了程序大小与其正确性证明难度之间的非线性关系，且增长速度快于任何可计算函数。

值得注意的是，虽然通用算法不存在，但对于特定小规模的程序，其行为可能独立于标准公理系统（如 ZFC）。例如，Adam Yedidiya 和 Scott Aaronson 曾发布基于此原理的程序，Stefan O’Rear 进一步构建了一台拥有 1919 个控制状态的图灵机，其停机性在 ZFC 系统中既不能被证明也不能被证伪。这台机器仅相当于 100-200 行的 Python 代码，却代表了数学能力的边界。

计算机科学不同于纯数学

哥德尔、丘奇和图灵的工作表明，计算机程序是一类特殊的数学对象：它们可以被形式化推理，但不能被完全理解。这与希尔伯特最初的设想背道而驰。

图灵在其工作中强调，算法是由人或机器在物理世界中执行的。Church-Turing 论题认为，宇宙中任何可实现的物理过程都可以由通用计算模型模拟。然而，程序的根本性质与“完全理解”、“证明”和“绝对正确性”之间存在内在冲突。数学关注封闭的小圈子内的真理，而计算机科学处理的是开放系统中的行为。

第二章：计算复杂性

仅仅知道问题是否可判定是不够的，实际工程中更关心的是解决问题的资源消耗。正如 Juris Hartmanis 和 Richard Stearns 在1965年的开创性论文中所指出的，可计算序列之间存在固有的难度差异。

“在实践中，代数阶与指数阶的区别往往比有限与无限的区别更为重要。”

图灵早在1947年就意识到时间因素的重要性。Max Newman 曾质疑：“说一台机器可以做某事是很好的……但在机器上解决问题并不意味着在现在和永恒之间找到方法，而是在合理的时间内。”图灵回应称，时间因素涉及所有技术困难的核心。

有界停机问题

为了精确衡量难度，我们考察“有界停机问题”：判定任意程序 $M$ 是否在输入 $x$ 上于 $n$ 步内停机。

假设存在快速算法 $H_n$：

$H_n(M, x)$ := IF $M$ 在 $n$ 步内于 $x$ 上停机 THEN TRUE ELSE FALSE
且满足 $TIME(H_n) \leq n - 2$

我们可以构造程序 $G(y)$：

$G(y)$ := IF $H_n(y, y)$ = FALSE THEN TRUE ELSE 循环 $n$ 次并返回 FALSE

当执行 $G(G)$ 时，由于 $H_n$ 在 $n-2$ 步内返回结果，$G$ 将在第 $n-1$ 或 $n$ 步完成判定。这导致了与 $H_n$ 定义相矛盾的时序逻辑。因此，我们无法比运行程序本身更快地知道程序的行为。有界停机问题的复杂度为 $\theta(n)$。

均摊有界停机

能否通过对某些输入进行预处理，从而在其他输入上加速？这引出了“均摊有界停机”问题。即使允许在大量输入上进行预计算，也无法显著降低最坏情况下的复杂度。通过归约至有界停机问题，可以证明该方案同样不可行。

综上所述，$\Omega(|S|)$ 的结果极其稳健。即便剥离图灵机的完备性，降至较弱的计算模型，验证程序行为的最低成本依然与状态空间规模成正比。在一般情况下，图灵机拥有无限状态，导致最坏情况复杂度为无穷大，这正是通用停机问题不可判定的特例。