类型检查器也会出错？柯里 - 霍华德对应关系揭示证明辅助工具局限

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`，类型为 `Z`：

have 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/) 构建