柯里-霍华德同构

在编程语言理论和证明理论中，柯里-霍华德同构（也称为 Curry-Howard 同构或等价）是两者之间的直接关系计算机程序和数学证明。

它是美国数学家 Haskell Curry 和逻辑学家 William Alvin Howard 最先发现的形式逻辑系统和计算演算系统之间句法类比的概括。

柯里-霍华德同构的起源在于几个观察：

• 1934 年，Curry 观察到组合子的类型可以被视为直觉蕴涵逻辑的公理方案。
• 1958 年，他观察到某种证明系统（称为希尔伯特式演绎系统）在某些片段上与标准计算模型（称为组合逻辑）的类型化片段重合。
• 1969 年，Howard 观察到另一个更高级的证明系统，称为自然演绎，可以在其直觉版本中直接解释为称为 lambda 演算的计算模型的类型变体。

换句话说，柯里-霍华德同构观察到两个看似无关的形式主义家族——即一方面是证明系统，另一方面是计算模型——实际上是同一类数学对象。

如果对任何一种形式主义的特性进行抽象，就会出现以下概括：证明是程序，它证明的公式是程序的类型。更通俗地说，这可以看作是一个类比，它指出函数的返回类型（即函数返回值的类型）类似于逻辑定理，服从与传递的参数值类型相对应的假设 到函数；并且计算该函数的程序类似于该定理的证明。这在严格的基础上建立了一种逻辑编程形式：证明可以表示为程序，尤其是 lambda 项，或者可以运行证明。

在发现这种对应关系之后，它一直是大量新研究的起点，特别是导致了一类新的形式系统，旨在充当证明系统和类型化的函数式编程语言。这包括 Martin-Löf 的直觉类型理论和 Coquand 的构造演算，这两种演算中，证明是话语的常规对象，并且可以用与任何程序相同的方式陈述证明的属性。 这个研究领域通常被称为现代类型理论。

这种源自 Curry-Howard 范式的类型化 lambda 演算导致了像 Coq 这样的软件，在其中可以形式化、检查和运行被视为程序的证明。

一个相反的方向是使用一个程序来提取一个证明，给定它的正确性——一个与证明携带代码密切相关的研究领域。 这只有在编写程序所针对的编程语言类型非常丰富时才可行：开发此类系统的部分原因是希望柯里-霍华德架构具有实际意义。

柯里-霍华德同构还对 Curry 和 Howard 的原始作品中未涉及的证明概念的计算内容提出了新的问题。 特别是，经典逻辑已被证明对应于操纵程序连续性的能力和相继演算的对称性，以表达称为按名称调用和按值调用的两种评估策略之间的二元性。

据推测，柯里-霍华德同构可能有望导致数理逻辑与基础计算机科学之间的实质性统一：

希尔伯特式逻辑和自然演绎只是一大类形式主义中的两种证明系统。 替代语法包括序贯演算、证明网、结构演算等。如果承认柯里-霍华德同构作为任何证明系统隐藏计算模型的一般原则，则这些类型的底层无类型计算结构的理论 的证明系统应该是可能的。 那么，一个自然的问题是关于这些底层计算演算是否可以说出一些数学上有趣的东西。

相反，组合逻辑和简单类型的 lambda 演算也不是唯 一的计算模型。