将数学证明与计算机程序等同起来的深层链接| 广达杂志

一些科学发现很重要，因为它们揭示了一些新的东西——例如DNA的双螺旋结构，或者黑洞的存在。 然而，一些启示意义深远，因为它们表明，两个曾经被认为截然不同的旧概念实际上是相同的。 以詹姆斯·克拉克·麦克斯韦的方程为例，该方程表明电和磁是单一现象的两个方面，或者广义相对论将引力与弯曲时空联系起来。

库里与霍华德的对应关系也做了同样的事情，但规模更大，不仅链接了一个领域内的不同概念，还链接了整个学科： 计算机科学 和 数学逻辑。 也称为柯里-霍华德同构（这个术语意味着两个事物之间存在某种一对一的对应关系），它在数学证明和计算机程序之间建立了联系。

简而言之，柯里-霍华德对应关系假设计算机科学中的两个概念（类型和程序）分别相当于命题和证明——逻辑中的概念。

这种对应关系的一个后果是，编程——通常被视为一种个人手艺——被提升到了理想化的数学水平。 编写程序不仅仅是“编码”，它还成为证明定理的行为。 这使编程行为形式化，并提供了对程序正确性进行数学推理的方法。

该信件以独立发现它的两位研究人员的名字命名。 1934年，数学家和逻辑学家哈斯克尔·柯里注意到数学中的函数与逻辑中的蕴涵关系之间的相似性，即两个命题之间的“if-then”陈述的形式。

受到库里观察的启发，数理逻辑学家威廉·阿尔文·霍华德 (William Alvin Howard) 在 1969 年发现了计算与逻辑之间更深层次的联系，表明运行计算机程序很像简化逻辑证明。 当计算机程序运行时，每一行都会被“评估”以产生一个输出。 类似地，在证明中，您从可以简化的复杂语句开始（例如，通过消除冗余步骤，或用更简单的表达式替换复杂表达式），直到得出结论 - 从许多临时语句派生出的更简洁的语句。

虽然这个描述传达了对应关系的一般意义，但为了充分理解它，我们需要更多地了解计算机科学家所说的“类型理论”。

让我们从一个著名的悖论开始：在一个村庄里住着一位理发师，他为所有不给自己刮胡子的人刮胡子，而且只给他们刮胡子。 理发师自己刮胡子吗？ 如果答案是肯定的，那么他一定不能给自己刮胡子（因为他只给不给自己刮胡子的男人刮胡子）。 如果答案是否定的，那么他必须给自己刮胡子（因为他给所有不给自己刮胡子的人刮胡子）。 这是伯特兰·罗素在尝试使用集合概念建立数学基础时发现的悖论的非正式版本。 也就是说，定义一个包含所有不包含自身的集合而不遇到矛盾的集合是不可能的。

罗素表示，为了避免这种悖论，我们可以使用“类型”。 粗略地说，这些类别的具体值称为对象。 例如，如果有一个名为“Nat”的类型，意思是自然数，那么它的对象就是 1、2、3 等等。 研究人员通常使用冒号来表示对象的类型。 数字7是整数类型，可以写成“7：Integer”。 您可以有一个函数，它接受类型 A 的对象并吐出类型 B 的对象，或者将一对类型 A 和类型 B 的对象组合成一种新类型，称为“A × B”。

因此，解决这个悖论的一种方法是将这些类型放入层次结构中，这样它们只能包含比它们自己“更低级别”的元素。 那么类型就不能包含自身，这避免了造成悖论的自引用。

在类型论的世界中，证明一个陈述是正确的可能看起来与我们习惯的不同。 如果我们想证明整数 8 是偶数，那么需要证明 8 确实是一个名为“Even”的特定类型的对象，其中成员资格的规则是能被 2 整除。在验证 8 能整除之后由2，我们可以得出结论，8确实是Even类型的“居民”。

库里和霍华德表明，类型从根本上等同于逻辑命题。 当一个函数“驻留在”一种类型时——也就是说，当你可以成功定义一个作为该类型对象的函数时——你就有效地证明了相应的命题是正确的。 因此，接受类型 A 的输入并给出类型 B 的输出（表示为类型 A → B）的函数必须对应于一个含义：“如果 A，则 B”。 例如，以命题“如果正在下雨，则地面是湿的”为例。 在类型理论中，这个命题将由类型为“Raining → GroundIsWet”的函数建模。 看似不同的公式实际上在数学上是相同的。

尽管这种联系听起来很抽象，但它不仅改变了数学和计算机科学从业者对他们工作的思考方式，而且还导致了这两个领域的一些实际应用。 对于计算机科学来说，它为软件验证（确保软件正确性的过程）提供了理论基础。 通过用逻辑命题构建期望的行为，程序员可以从数学上证明程序的行为符合预期。 它还为设计更强大的函数式编程语言提供了坚实的理论基础。

对于数学来说，对应关系导致了 证明助理，也称为交互式定理证明者。 这些是帮助构建形式证明的软件工具，例如 Coq 和 Lean。 在 Coq 中，证明的每一步本质上都是一个程序，并且通过类型检查算法来检查证明的有效性。 数学家也一直在使用证明助手——值得注意的是， 精益定理证明者 ——将数学形式化，这涉及以严格的、计算机可验证的格式表示数学概念、定理和证明。 这使得有时非正式的数学语言可以由计算机进行检查。

研究人员仍在探索数学和编程之间这种联系的后果。 最初的库里-霍华德对应将编程与一种称为直觉逻辑的逻辑融合在一起，但事实证明，更多类型的逻辑也可以接受这种统一。

“自库里提出见解以来，一个世纪以来发生的事情是，我们不断发现越来越多的实例，其中‘逻辑系统 X 对应于计算系统 Y’，”说 迈克尔·克拉克森，康奈尔大学计算机科学家。 研究人员已经将编程与其他类型的逻辑联系起来，例如线性逻辑（包括“资源”的概念）和模态逻辑（处理可能性和必然性的概念）。

虽然这封信上有库里和霍华德的名字，但他们绝不是唯一发现这封信的人。 这证明了信件的基本性质：人们不断地一次又一次地注意到它。 “计算和逻辑之间存在深刻的联系似乎并非偶然，”克拉克森说。