数学证实=计算机程序？什么是柯里-霍华德对应？
一些科学发觉被赋予了重要的意义，因为揭示了一些新的东西，比如 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/