数学证明和计算机程序等同的深层链接
数学逻辑和计算机程序的代码，准确地说，是彼此的镜像。
作者：Sheon Han
译者：zzllrr小乐
一些科学发现之所以重要，是因为它们揭示了一些新的东西——例如DNA的双螺旋结构，或者黑洞的存在。然而，有些启示是深刻的，因为它们表明，曾经被认为是不同的两个旧概念，实际上是相同的。以詹姆斯·克拉克·麦克斯韦（James Clerk Maxwell）的方程为例，该方程表明电和磁是单一现象的两个方面，或者广义相对论将引力与弯曲时空联系起来。
柯里-霍华德对应（Curry-Howard correspondence）也做了同样的事情，但规模更大，不仅将一个领域的不同概念联系起来，而且将整个学科联系起来：计算机科学和数理逻辑。也称为柯里-霍华德同构（isomorphism同构，是一个术语，意思是两件事之间存在某种一对一的对应关系），它在数学证明和计算机程序之间建立了联系。
简单地说，柯里-霍华德对应假设计算机科学中的两个概念（类型和程序）分别等价于逻辑概念：命题和证明。
这种对应的一个后果是，编程——通常被视为个人的手艺——被提升到数学的理想化水平。编写一个程序不仅仅是“编码”，它变成了证明一个定理的行为。这形式化了编程行为，并提供了从数学上推理程序正确性的方法。
该对应以独立发现它的两位研究人员命名。1934年，数学家和逻辑学家哈斯克尔·柯里（Haskell Curry）注意到数学中的函数（function）与逻辑中的蕴涵关系（implication relationship）之间的相似性，它采用两个命题之间的“如果-那么”（if-then）的陈述形式。
受到柯里观察的启发，数理逻辑学家威廉·阿尔文·霍华德（William Alvin Howard）在1969年发现了计算和逻辑之间更深层次的联系，表明运行计算机程序很像简化逻辑证明。当计算机程序运行时，每一行都经过“求值”以产生单个输出。类似地，在证明中，你从复杂的陈述开始，你可以简化这些陈述（例如，通过消除多余的步骤，或者用更简单的表达式替换复杂的表达式），直到你得出结论——一个从许多临时陈述派生出来的更精简、更简洁的陈述。
虽然这种描述传达了对应的一般意义，但要完全理解它，我们需要更多地了解计算机科学家所谓的“类型论”（type theory）。
让我们从一个著名的悖论开始：在一个村庄里，住着一个理发师，他给所有不自己刮胡子的男人刮胡子，并且只给这类人刮胡子。理发师会给自己刮胡子吗？如果答案是肯定的，那么他一定不能给自己刮胡子（因为他只给不刮自己胡子的男人刮胡子）。如果答案是否定的，那么他必须给自己刮胡子（因为他给所有不刮自己胡子的男人刮胡子）。这是伯特兰·罗素（Bertrand Russell）在试图使用称为集合（Set）的概念建立数学基础时发现的悖论的非正式版本。也就是说，不可能定义一个包含所有不包含自身的集合而不遇到矛盾。
罗素指出，为了避免这种悖论，我们可以使用“类型”（type）。粗略地说，这些是其特定值称为对象（object）的范畴（category）。例如，如果有一个名为“Nat”（取单词自然Nature前3个字母，zzllrr小乐译注）的类型，表示自然数，则其对象为 1、2、3 等。研究人员通常使用冒号来表示物体的类型。整数类型的数字 7 可以写为“7:整数”。你可以有一个函数，该函数获取类型 A 的对象并吐出 B 类型的对象，或者将一对类型 A 和类型 B 的对象组合成一个名为“A × B”的新类型。
因此，解决悖论的一种方法是将这些类型放入一个层次结构（hierarchy）中，这样它们只能包含比它们自己“低级别”的元素。然后，类型不能包含自身，从而避免了产生悖论（paradox）的自指性（self-referentiality）。
在类型论的世界里，证明一个陈述是正确的可能看起来与我们习惯的不同。如果我们想证明整数 8 是偶数，那么就需要证明 8 确实是一个名为“偶数”（Even）的特定类型的对象，其中成员资格的规则是可以被 2 整除。在验证 8 能被 2 整除后，我们可以得出结论，8 确实是偶数类型的“居民”。
柯里和霍华德表明，类型在根本上等同于逻辑命题。当一个函数“栖居”在一个类型时——也就是说，当你能够成功地定义一个函数是该类型的对象时——你有效地表明相应的命题是正确的。因此，接受类型 A 的输入并给出类型 B 的输出（表示为 A → B）的函数必须对应于一个蕴含：“如果 A，那么 B。”例如，假设“如果下雨，那么地面是湿的。”在类型论中，这个命题将由“下雨 → 地面是湿的”的函数建模。外观不同的公式实际上在数学上是相同的。
尽管这种联系听起来很抽象，但它不仅改变了数学和计算机科学从业者对他们工作的看法，而且还导致了这两个领域的一些实际应用。对于计算机科学来说，它为软件验证提供了理论基础，即确保软件正确性的过程。通过根据逻辑命题构建所需的行为，程序员可以在数学上证明程序的行为符合预期。它还为设计更强大的函数式编程语言提供了坚实的理论基础。
对于数学来说，这种对应导致了证明助手（proof assistant）的诞生，也称为交互式定理证明器（interactive theorem prover）。这些是有助于构建形式证明的软件工具，例如Coq和Lean。在Coq中，证明的每一步本质上都是一个程序，证明的有效性通过类型检查算法进行检查。数学家也一直在使用证明助手——特别是Lean定理证明器——来形式化数学，这涉及以严格的、计算机可验证的格式表示数学概念、定理和证明。这使得有时非正式的数学语言可以被计算机检查。
研究人员仍在探索数学和编程之间这种联系的后果。最初的柯里-霍华德对应将编程与一种称为直觉逻辑（intuitionistic logic）的逻辑融合在一起，但事实证明，更多类型的逻辑也可以适应这种统一。
“自从柯里提出见解以来的一个世纪里发生的事情是，我们不断发现越来越多的'逻辑系统X对应于计算系统Y'的例子，”康奈尔大学的计算机科学家迈克尔·克拉克森（Michael Clarkson）说。研究人员已经将编程与其他类型的逻辑联系起来，如线性逻辑（linear logic），其中包括“资源”（resource）的概念，以及模态逻辑（modal logic），它处理可能性和必要性的概念。
虽然这个对应有柯里和霍华德的名字，但他们绝不是唯一发现它的人。这证明了对应的基本性质：人们一次又一次地注意到它。“计算和逻辑之间存在深刻的联系似乎并非偶然，”克拉克森说。