2023/10/23 15:31

数学逻辑和计算机程序代码之间的深层联系：互为镜像

数学证明=计算机程序？什么是柯里-霍华德对应？

一些科学发现被赋予了重要的意义，因为揭示了一些新的东西，比如 DNA 的双螺旋结构或黑洞的存在。但是，揭示出的这些东西还具有更深远的意义，因为它们表明：两个之前看起来大不一样的老旧概念事实上却是一样的。比如詹姆斯・克拉克・麦克斯韦发现的方程组表明，电与磁是同一个现象的两个不同方面，而广义相对论则把引力和弯曲的时空联系到了一起。

柯里 - 霍华德对应（Curry-Howard correspondence）也是一样，并且它关联的不仅仅是一个领域中的两个不同概念，而是两个完整的学科：计算机科学和数学逻辑。这种对应关系也被称为柯里 - 霍华德同构（Curry-Howard isomorphism，同构是指两个事物之间存在某种一一对应关系），其为数学证明和计算机程序建立了某种关联。

简单来说，柯里 - 霍华德对应认为：计算机科学中的两个概念（类型和程序）分别等价于逻辑学中的两个概念（命题和证明）。

这种对应关系导致的一个结果是程序开发被提升到了理想化的数学层面，而之前人们通常认为程序开发就是个手艺活。程序开发不只是「写代码」，还变成了证明定理的行为。这能对程序开发的行为进行形式化，并能提供用数学方法推理程序正确性的方法。

而这种对应关系的名称则来自于两位研究者，他们各自独立地发现了这一对应关系。1934 年，数学家和逻辑学家哈斯凯尔・柯里（Haskell Curry）注意到了数学中的函数和逻辑学中的蕴涵（implication）关系之间的相似性。蕴涵关系的形式是两个命题之间呈现「if-then（如果 - 那么）」陈述的形式。

受柯里观察到的结果的启发，数理逻辑学家威廉・阿尔文・霍华德（William Alvin Howard）在 1969 年发现计算和逻辑之间存在更深度的关联；他的研究表明：运行计算机程序非常像是简化逻辑证明。在运行计算机程序时，每一行代码都会被「评估」以产生一个输出。类似地，在进行一个证明时，一开始是复杂的陈述，然后对其进行简化（例如通过消除冗余步骤或用更简单的表达式替换复杂表达式），直到得到某个结论 —— 从许多过渡陈述推导出一个更简明的陈述。

尽管这一描述大致说明了这种对应关系的含义，但要完全理解它，就需要更多地了解计算机科学家口中的「类型论（type theory）」。

让我们从一个著名的悖论谈起：在一个村庄中有一位理发师，他为且只为所有不给自己刮胡子的人刮胡子。那么这位理发师给自己刮胡子吗？如果答案为是，那么他就必定不为自己刮胡子（因为他只为不给自己刮胡子的人刮胡子）。如果答案为否，那么他就必定给自己刮胡子（因为他为所有不给自己刮胡子的人刮胡子）。这是伯特兰・罗素（Bertrand Russell）发现的一个悖论的非形式化版本，那时候他正尝试使用名为集合（set）的概念构建数学的基础。也即：定义一个包含所有不包含自身的集合的集合是不可能的，这个过程必然会出现矛盾。

罗素的研究表明，为了避免这个悖论，我们可以使用类型（type）。粗略地说，类型是指一些类别，其含有的具体值被称为对象（object）。举个例子，如果有一个类型 Nat 表示自然数，那么其对象就是 1、2、3 等等。研究人员通常使用冒号来表示对象的类型。比如对于整数类型的数值 7，可以写成「7: Integer」。我们可以使用函数将类型 A 的对象转换成类型 B 的对象，也可以使用函数将类型 A 和 B 的两个对象组成一个新类型「A×B」的对象。

因此，为了解决这个悖论，一种方法是对这些类型进行分层，让它们仅包含比其自身低一个层级的元素。然后一个类型不能包含自身，这就能避免造成上述悖论的自我指涉。

在类型论的世界中，证明一个陈述为真的过程可能与我们习惯的做法不一样。如果我们想证明整数 8 是偶数，那么问题的关键在于证明 8 实际上是「偶数」类型中一个对象，而这个类型定义元素的规则是能被 2 整除。在验证了 8 能被 2 整除后，我们就能得出结论：8 就是「偶数」类型中的一个「居民」。

柯里与霍华德证明类型在根本上等价于逻辑命题。当一个函数「居留（inhabit）」于某一类型时，也就是该函数是该类型的一个对象时，我们就能有效地证明对应的命题为真。因此，以类型 A 的对象为输入、以类型 B 的为输出的函数（表示成类型 A→B）必定对应于一个蕴涵：「如果 A，那么 B。」举个例子，假设有命题「如果下雨，那么地面是湿的。」在类型论中，这个命题会被建模成类型「下雨→地面湿」的一个函数。这两种表示方式看起来不一样，但在数学上却是一样的。

尽管这种关联看起来可能很抽象，但它不仅改变了数学和计算机科学的实践者思考其工作的方式，还为这两个领域带来了一些实用的应用。在计算机科学领域，这种关联为软件验证（即确保软件正确性的过程）提供了一个理论基础。通过逻辑命题的方式描述所需行为，程序开发者可以通过数学方式证明一个程序的行为是否符合预期。并且在设计更强大的函数式编程语言方面，这种关联也提供了坚实的理论基础。

而在数学领域，这种对应关系已经催生出了证明助手（proof assistant）工具，其也被称为交互式定理证明器（interactive theorem prover）。这些软件工具可以辅助构建形式化证明，具体的例子包括 Coq 和 Lean。在 Coq 中，每一步证明本质上都是一个程序，而证明的有效性则会通过类型检查算法来检验。数学家们也已经在使用证明助手（尤其是 Lean 定理证明器）来对数学进行形式化，其中涉及到以一种可通过计算机验证的严格格式来表示数学概念、定理和证明。这让有时候非形式化的数学语言可以通过计算机加以检验。

研究者还在探索数学和编程之间的这种关联的潜在成果。原始的柯里 - 霍华德对应将程序开发与某种名为直觉逻辑（intuitionistic logic）的逻辑融合到了一起，但事实证明还有更多逻辑类型可以被统一进来。

康奈尔大学计算机科学家 Michael Clarkson 说：「自柯里得出其见解的这一个世纪里，我们不断发现越来越多『逻辑系统 X 对应于计算系统 Y』的实例。」研究者也已经将编程和其它类型的逻辑联系起来，比如包含「资源」概念的线性逻辑以及涉及可能性和必要性概念的模态逻辑。

而且尽管这个对应关系秉承柯里与霍华德之名，但他们绝不是这种对应关系的唯二发现者。这佐证了这种对应关系的一个根本性质：人们反复不断地一次又一次地注意到它。Clarkson 说：「计算和逻辑之间存在深度关联似乎并非偶然。」

^{原文链接：https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/}

理论柯里 - 霍华德对应