类型检查器也会出错柯里 - 霍华德对应关系揭示证明辅助工具局限Max 的博客[/][~/][~/关于我/](/about-me/) [~/系列文章/](/series/) [~/博客文章/](/blog/)2026 年 7 月 25 日在编写代码时类型检查器多次为我们节省了时间。它能确保你不会将字符串与整数相加或者返回值的引用而非值本身。然而尽管类型检查器很实用有时也会让人烦恼除了帮我们避免错误它的能力似乎也有限……你可能会惊讶地发现类型检查器也是证明辅助工具如 Lean 和 Rocq 等语言的核心。它们利用类型的结构明确检查某个陈述是否能从其他陈述推导出来或者更通俗地说验证数学证明。在这篇博客中我先介绍柯里 - 霍华德对应关系的一些基础知识接着说明它在证明辅助工具中的应用最后解释为什么这可能意味着你的类型检查器“出错”了或者说它可能不知道你是对的。柯里 - 霍华德对应关系柯里 - 霍华德CH对应关系可简单定义为证明可以表示为程序……证明可以运行。这个定义没给出太多信息我们可以这样思考既然证明能表示为程序那我们就需要一种方法让程序返回证明。但返回证明到底意味着什么呢回到基础概念如果一个程序要返回一个整数我们说它返回的类型是 $\text{int}$它可以是任意整数所以 $\text{int}$ 代表整数集。同样如果一个程序要返回 $\text{True}$ 或 $\text{False}$我们说它返回的类型是 $\text{bool}$它包含这两种可能性。将类型近似看作集合并不完全准确但对于本文来说已经足够。尝试将这种思路扩展到证明上我们可以说当一个程序返回某个事实的证明时它返回的是类型 $P(X)$ 的一个元素其中 $P(X)$ 是事实 $X$ 的所有证明的集合。为深入研究这个新的证明对象我们首先要将命题逻辑和谓词逻辑中的一些逻辑运算转换到这个新的范式中。我们从最简单的开始$$ X \text{ 为真} $$在我们的例子中要使 $X$ 为真我们必须有 $X$ 的证明即$$ \exists p : p \in P(X) $$我们这样表述$P(X)$ 是可构造的。例如$P(5 5)$ 是可构造的但 $P(5 2 6)$ 不是因为在皮亚诺算术中没有这个证明它是错误的。接下来要表示的逻辑运算是“与”$\wedge$。对于不熟悉的人来说当且仅当 $X$ 和 $Y$ 都为真时才有 $X \wedge Y$。所以 $P(X)$ 和 $P(Y)$ 都是可构造的即 $\exists p: p \in P(X)$ 且 $\exists p\prime : p\prime \in P(Y)$。这意味着我们可以构造一个对象 $(p, p\prime)$所以$$ P(X) \times P(Y) $$其中 $\times$ 表示笛卡尔积是可构造的$(p, p\prime) \in P(X) \times P(Y)$。接下来我们要表示蕴含运算。如果 $X \implies Y$那么要么 $X$ 为假要么 $X$ 为真且 $Y$ 为真。我们将其表示为从 $P(X)$ 到 $P(Y)$ 的函数的存在$$ P(X) \to P(Y) $$如果这个函数存在那么只要我们有 $X$ 的证明就可以推导出 $Y$ 的证明。如果 $X$ 为假即 $P(X)$ 不可构造那么函数没有输入所以 $P(Y)$ 可能成立也可能不成立。为简洁起见我省略了对其他标准逻辑运算的讨论。它们在集合论中的表示如下但对本文的其余部分无关紧要| 逻辑运算 | 集合论表示 || --- | --- || $X \lor Y$ | $P(X) P(Y)$其中 $$ 表示不相交并集 || $(\forall(n \in \mathbb{N})X(n))$ | $(n: \mathbb{N}) \to P(X(n))$ || $(\exists(n \in \mathbb{N})X(N))$ | $(n: \mathbb{N}) \times P(X(n))$ |证明辅助工具如何运用柯里 - 霍华德对应关系证明辅助工具利用这种对应关系和它们的类型检查器来验证证明。但它们是如何做到的呢为说明这一点让我们用 [Lean](https://lean - lang.org/) 符号来证明一个简单的定理。一个定理考虑下面名为 blog 的定理theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z它首先声明 $X$、$Y$ 和 $Z$ 是逻辑陈述即它们可能为真也可能为假。这就像构造集合 $P(X)$、$P(Y)$ 和 $P(Z)$但还没有说明它们是否可构造。接下来我们有一个假设 $h_1 : X$它是 $X$ 的证明。回想一下我们之前的讨论有 $X$ 的证明就相当于 $X$ 为真所以 $h_1 : X$ 简单地表明 $X$ 为真。$h_2$ 也是类似的它是 $Y$ 的证明。然后我们有最后一个假设我用无限的创造力和智慧将其命名为 $h_3$。它的类型是$$ Y \to Z $$这意味着存在一个函数从 $Y$ 的证明可以得到 $Z$ 的证明这相当于 $Y \implies Z$之前也讨论过。定理的最后一部分是期望的结果 $X \land Z$。为证明这一点我们必须构造一个属于 $P(X) \times P(Z)$ 的元素为此我们必须构造 $X$ 和 $Z$ 的证明。理解这个定理陈述花了不少功夫。不过我希望你现在能明白之前将逻辑运算映射到集合论的讨论是如何让我们将定理从类型语言转换到逻辑领域的。该定理的证明现在我们要证明这个定理。眼尖的人可能已经注意到我们已经有了一个想要的组件。我们需要元素来填充 $P(X)$ 和 $P(Z)$而我们有 $h_1$它是 $X$ 的证明因此可以填充 $P(X)$这很容易。现在我们需要证明 $P(Z)$。我们有 $h_2 : Y$ 和 $h_3$$h_3$ 是一个函数它接受 $Y$ 的证明并给出 $Z$ 的证明。通过将 $Y$ 的证明$h_2$传递给 $h_3$我们得到了 $Z$ 的证明它可以填充 $P(Z)$。现在如何在 Lean 中编写这个证明呢有很多方法下面是其中一种我们首先将期望的结果分解为两部分然后依次填充。使用 constructor 语句我们让 Lean 告诉我们要实现期望的结果需要做什么。Lean 忠实地给出了两个目标一个是填充 $X$另一个是填充 $Z$。为填充 $X$我们可以直接告诉 Lean 它是 $h_1$使用 exact h_1。为填充 $Z$我们需要将 $h_3$ 应用到 $h_2$ 上记住$h_3$ 是一个函数。在 Lean 中这很简单就是 h_3 h_2或者你可以写成 h_3 (h_2)让它更像非函数式语言。所以我们定义一个变量 z类型为 Zhave z : h_3 h_2然后再次使用 exact 完成证明。Lean 会用“目标达成”的消息祝贺我们。完整的代码如下theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z : by constructor exact h_1 have z: Z : h_3 (h_2) exact z类型检查器在文章开头我承诺要解释为什么你的类型检查器可能出错现在我就来解释。如前所述为让证明辅助工具验证你已经证明了期望的结果它会检查你是否成功输出了正确的类型即填充 $P(\text{你想要证明的内容})$ 的东西。类型检查器的局限性为让类型检查器安全地断言你已经做到了这一点它需要评估你提供的表达式序列中每个表达式的类型。这个要求存在一个问题它要求所有表达式都能完成求值。有两种情况可能导致表达式永远无法完成求值一种比较特殊的情况是 C 或 Python 中的 exit()它通过直接退出程序来逃避完成求值的要求。我们的解决方法是限制编程语言中允许的表达式这正是 Lean 和 Agda 等语言所做的。另一种表达式可能永远无法完成求值的情况更难解决。我们必须确保表达式序列不会陷入某种无限循环否则它们将永远无法完成。所以我们只需要一种方法来检查给定输入时表达式序列是否会停止。不幸的是这在有限时间内是不可能做到的。1936 年艾伦·图灵证明了一个程序是否会在有限时间内停止即停机问题是不可判定的这意味着在有限时间内无法计算。如果你想了解他用来证明这一点的图灵机的一些直觉可以看看我关于这个主题的文章 [这里](/blog/an_introduction_to_turing_machines_and_computation/)。形式语言试图回避这个事实的方法是进一步限制计算语言。在某些情况下递归可以被证明是有限的例如对自然数的向下递归。所以通过只允许可以被证明会停止的递归我们确保类型检查器总是能在有限时间内完成。需要注意的是这不是当前技术或软件的限制而是证明辅助工具的一个基本限制无法解决。总会存在一些结果其证明是无法验证的。数学后果及证明这种限制极大地降低了这些语言的表达能力意味着它们无法表示每一个可能的证明。但为什么会这样呢为进行反证我们假设受限语言有足够的表达能力来表示每个命题陈述的证明或反证明即 $\forall S$我们可以在语言中证明 $S$ 或 $\lnot S$。现在既然我们假设语言是无所不知的那就来玩一玩吧……考虑一个任意程序 $P$它有一组有限的任意输入 $A$以及命题 $H$$P$ 在输入 $A$ 时会停止。现在使用我们的语言我们知道可以写出这个命题的证明或反证明并在有限时间内验证它。我们的做法是生成 $H$ 和 $\lnot H$ 的所有可能证明然后使用类型检查器检查其中一个是否有效。由于类型检查器在有限时间内运行并且其中一个证明是正确的因为我们的语言有足够的表达能力这个过程是有限的。由于我们可以对任何程序都这样做我们现在已经能够在有限时间内检查任意程序是否会停止然而正如之前讨论的这是不可能的又是图灵的停机问题。所以我们的假设一定是错误的因此受限语言没有足够的表达能力来表示每个命题陈述的证明或反证明。柯里 - 霍华德对应关系告诉我们证明和程序是等价的但这现在导致了一个令人不安的事实。如果我们的语言必然受到限制无法证明或反驳某些命题那么这表明一般情况下可能无法做到这一点……这是数学中的一个著名问题。哥德尔第一不完备性定理指出任何能够进行一定量初等算术运算的一致形式系统都是不完备的。通俗地说对于任何用于计算的形式系统数学中的每个形式系统都是如此都存在既无法证明也无法反驳的陈述。现在我们已经证明了哥德尔第一不完备性定理的否定意味着图灵停机问题的否定因此通过逆否命题柯里 - 霍华德对应关系得出了一个令人震惊的结果。图灵停机问题意味着哥德尔不完备性定理。如果你想了解逆否命题的一些直觉可以看看我以鱼为主题的关于逆否命题的文章 [这里](/blog/some_intuition_behind_the_contrapositive/)。你的类型检查器可能出错我们现在已经看到类型检查器并不完美事实上它被证明是不完美的。因此……在某些情况下……你的类型检查器可能……出错。可能会有这样的情况你的类型检查器为了避免无限运行而拒绝了你的代码但实际上它是正确的。当然这种情况不太可能发生例如 Rust 中的类型检查器递归限制是 128。但这是有可能的所以当你的同事抱怨你的代码无法通过类型检查时要知道……你可能是正确的虽然可能性不大 :)。结论在这篇文章中我们绕了一大圈说明了类型检查器可能无法验证你的代码是否正确。不过它永远不会接受错误的代码所以如果它接受了你的代码你可以放心它是正确的。现在只需要找出逻辑错误了……* * *1. 特别要排除 JavaScript在那里像 $5 \text{five}$ 这样的杰作是可能的。 ↩︎2. ↩︎3. ↩︎4. ↩︎5. ↩︎6. 我们所说的可能证明是指语言中任何可能的语法表达式序列。 ↩︎7. ↩︎8. 嗯……实际上我们称这种情况为不完备而不是错误。它不会接受错误的东西只是可能不接受正确的东西。 ↩︎9. ↩︎10. Rust 类型检查器检查代码的过程当然与 Lean 或 Agda 中的检查器不同但基本限制是相同的所以这个玩笑还是成立的 。 ↩︎[ 上一篇文章](https://max - amb.github.io/blog/zero_knowledge_tolstoyan_art/)|~~下一篇文章 ~~使用 [Hugo ʕ•ᴥ•ʔ Bear](https://github.com/janraasch/hugo - bearblog/) 构建