柯里-霍华德同构

柯里-霍华德对应（英语：Curry-Howard correspondence）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍华德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德（William Alvin Howard）独立发现的。

对应可以在两个层面上看到，首先是类比层次，它声称对一个函数计算出的值的类型的断言可类比于一个逻辑定理，计算这个值的程序可类比于这个定理的证明。在理论计算机科学中，这是连接λ演算和类型论的毗邻领域的一个重要的底层原理。它被经常以下列形式陈述为“证明是程序”。一个可选择的形式化为“命题为类型”。其次，更加正式的，它指定了在两个数学领域之间的同构，就是以一种特定方式形式化的自然演绎和简单类型λ演算之间是双射，首先是证明和项，其次是证明归约步骤和beta归约。

有多种方式考虑柯里-霍华德对应。在一个方向上，它工作于“把证明编译为程序”级别上。这里的“证明”最初被限定为在构造性逻辑中—典型的是直觉逻辑系统中的证明。而“程序”是在常规的函数式编程的意义上的；从语法的观点上看，这种程序是用某种λ演算表达的。所以柯里-霍华德同构的具体实现是详细研究如何把来自直觉逻辑的证明写成λ项。（这是霍华德的贡献；柯里贡献了组合子，它是相对于是高级语言的λ演算是能写所有东西的机器语言）。最近，同样处理经典逻辑的柯里-霍华德对应的扩展可被公式化了，通过对经典有效规则比如双重否定除去和皮尔士定律关联上明确的用续体比如call/cc处理的一类项。

还有一个相反的方向，对一个程序的正确性关联上“证明提取”的可能性。这在非常丰富的类型论环境中是可行的。实际上理论家对推进非常丰富类型的函数式编程语言的开发的动机，已经部分地混合了希望带给柯里-霍华德对应更加显著的地位的因素。

依据λ演算，我们将使用λx.E来指示带有形式参数x和函数体E的函数。在应用于参数比如a的时候，这个函数生成E，并带有x的所有自由出现都被替换为a。有效的λ演算表达式有如下形式之一：

通常我们将缩写(（A B）C)为(A B C)，缩写λa.λb.E为λab.E。一个表达式被称为是“闭合的”，如果它不包含自由变量。

类型可以依赖于类型变量，它被指示为小写的希腊字母α, β等等。在我们概念中类型变量是被隐含的全称量化的，就是说，如果一个值有包括类型变量的一个类型，则它必须由这个类型变量的所有可能实例组成。我们可以定义任意表达式的类型为如下：

例如，考虑函数K = λa.λb.a。假定a有类型α而b有类型β。则λb.a有类型β→α，而λa.λb.a有类型α→(β→α)。我们接受→是右结合的约定，所以这个类型也可以写为α→β→α。这意味着K函数接受类型α的参数并返回一个函数，它接受类型β的参数并返回类型α的值。

类似的，考虑函数B = λa.λb.λc.(a (b c))。假定c有类型γ，则b必须有形如γ→β的某种类型，表达式(b c)有类型β。a必须有形如β→α的某种类型，表达式(a (b c))有类型α。那么λc.(a (b c))有类型γ→α；λb.λc.(a (b c))有类型(γ→β)→γ→α，而λa.λb.λc.(a (b c))有类型(β→α)→(γ→β)→γ→α。你可以把这解释为意味着B函数接受类型(β→α)的参数和类型(γ→β)的参数并返回一个函数，它接受类型γ的参数并返回类型α的结果。

很明显λ-表达式可以有非常复杂的类型。你可能要问是否有带有给定类型的λ-表达式。找到带有特定类型的λ-表达式的问题叫做类型居留问题。

答案是非常引人注目的：有带有特定类型的闭合λ-表达式，当且仅当这个类型对应于一个逻辑定理，在这里的→符号再次解释为意味着逻辑蕴涵的时候。

例如，考虑恒等函数λx.x，它接受类型ξ的参数并返回类型ξ的结果，所以有类型ξ→ξ。ξ→ξ当然是逻辑定理：给定一个公式ξ，你可以结论出ξ。

K函数的类型α→β→α也是一个定理。如果已知α为真，则你可以结论出如果β为真就能推出α。这有时也叫做重复规则。B的类型是 (β→α)→(γ→β)→γ→α。你可类似的把它解释为逻辑重言式；如果已知(β→α)为真，则如果已知(γ→β)为真，你就能推出γ蕴涵α。

在另一方面，考虑α→β，它不是定理。明显的没有这种类型的λ-项；它必定是接受类型α的参数并返回某个完全无关的和未约束类型的结果的函数。这是不可能的，因为你不能从这种函数里得到什么东西，除非把它放到其他什么地方之中。

尽管有类型β→(α→α)的函数（比如，λb.λa.a，它接受一个参数b，忽略参数，并返回恒等函数），却没有类型(α→α)→β的函数，如果存在的话，它会是转换恒等函数到任意值的函数。

尽管所有居留类型对应于逻辑定理为真，逆命题却不为真。即使我们限制我们的尝试到只包含→运算的逻辑公式，所谓的逻辑的蕴涵片段，不是所有经典有效的逻辑公式是居留类型。例如，类型((α→β)→α)→α是非居留的，尽管叫做皮尔士定律的对应逻辑公式是重言式。

直觉逻辑是比经典逻辑弱的系统。经典逻辑把自身关注于在抽象的、柏拉图主义意义上为真的公式，而直觉逻辑只在可以为它构造一个证明的时候认为公式为真。公式α ∨ ¬α示例了这种区别；它是经典逻辑的一个定理而不是直觉逻辑的定理。尽管它是经典的真的，在直觉逻辑中这个公式断言了我们要么证明α要么证明¬α。因为我们不是总能做到这些事情之一，它不是直觉逻辑的一个定理。

在居留类型和有效逻辑公式之间的对应完全是双向的，如果我们限制我们的注意力到直觉逻辑的蕴涵片段（这也叫做希尔伯特代数）。

形式上刻画直觉逻辑的一个简单方式是希尔伯特演绎系统。它有两个公理模式。所有形式为

的公式都是公理，所有形式为

的公式都是公理。

唯一的演绎规则是肯定前件，它声称如果我们已经证明了两个定理，一个有形式α→β而另一个有形式α，我们可以结论出β也是定理。以这种方式推导出来的公式的集合正好是直觉逻辑的集合。特别的是，皮尔士定律不能以这种方式演绎。（对皮尔士定律不能以这种方式演绎的证明请参见海廷代数条目）。

如果我们增加皮尔士定律为第三个公理模式，这个系统就有能力证明在经典逻辑的蕴涵片段中的所有定理。

考虑λ-表达式的下列两个函数：

可以证明任何函数都可以通过适当的K和S相互应用来建立。（有关证明请参见组合子逻辑）。例如，上面定义的函数B等价于(S(K S)K)。如果一个函数比如B，可以表达为S和K的复合，则这个表达式可以直接转换成类型B的一个证明，它被解释为逻辑公式，是直觉逻辑的一个定理。本质上，K的外观对应于第一个公理模式的使用，S的外观对应于第二个公理模式的使用，而函数应用对应于肯定前件演绎规则的使用。

第一个公理模式是α→β→α，并且它精确的是K函数的类型；类似的第二个公理模式(α→β→γ)→(α→β)→α→γ，是S函数的类型。肯定前件声称如果我们有两个表达式，一个类型是α→β（就是说，接受类型α的值并返回类型β的值）而另一个类型是α（就是说，类型α的值），则我们应当能够找到类型β的值；明显的，我们可以通过应用这个函数到这个值之上来得到；结果会有类型β。

作为一个简单的例子，我们将构造定理α→α的证明。这是恒等函数I = λx.x的类型。函数((S K)K)等价于恒等函数。作为对证明的描述，它声称了我们需要首先应用S到K。我们做如下：

如果我们在S中设γ = α，我们得到：

因为这个公式的前件(α→β→α)是一个已知定理，并且实际上正好是K，我们可以应用肯定前件并推导出后件：

这是函数(S K)的类型。现在我们需要应用这个函数到K。我们再次操纵公式使得前件看起来像K，这次我们替代β为(β→α):

我们再次应用肯定前件来推出后件：

我们完成了。

一般的说，这个过程是只要程序包含形如(P Q)的应用，我们应当首先证明对应于P和Q的类型的定理。因为P要被应用于Q，对于某种α和β，P的类型必定有形式α→β而Q的类型必定有形式α。我们可以通过肯定前件规则推出β。

作为一个更加复杂的例子，我们看对应于函数B的定理的证明。B的类型是(β→α)→(γ→β)→γ→α。B等价于(S(K S)K)。这是对证明定理(β→α)→(γ→β)→γ→α的指引。

首先我们需要构造(K S)。我要使K公理的前件看起来像S公理，通过设置α等于(α→β→γ)→(α→β)→α→γ，和β等于δ:

因为前件正好是S，我们可以推出后件：

这是对应于(K S)的定理。现在我们要应用S到这个表达式。取得S

我们设置α = δ，β = (α→β→γ)和γ = ((α→β)→α→γ)，生成

我们可以接着推出后件：

这是类型(S(K S))的公式。这个定理的一个特殊情况有δ = (β→γ):

我们需要应用最后这个公式到K。我们再次特殊化K，这次是替代α为(β→γ)，替代β为α:

这同于前者公式的前件，所以我们推出后件：

交换变量α和γ的名字得到

这就是我们要证明的。

在下表第一列中的推导规则定义了直觉蕴涵自然演绎（为蕴涵连结词准备一个介入和一个除去规则）的标准系统。在第二列中给出${\displaystyle \mathrm{\lambda <!--\; \lambda \; -->}}$-演算的标准类型指派（赋值）系统。

希尔伯特式证明是很难构造的。证明逻辑定理的更加直觉的方式是根岑的相继式演算。相继式演算以同希尔伯特式证明对应于组合子表达式一样的方式对应于λ-表达式程序。

直觉逻辑的蕴涵片段的相继式演算规则是：

Γ表示上下文，它是假设的集合。${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->a}$指示假定上下文Γ我们可以证明a。逻辑定理完全由其证明不需要假设的那些公式t组成的；就是说，t是一个定理，当且仅当我们可以证明${\displaystyle ⊢<!--\; ⊢\; -->t}$。详情请参见相继式演算。

在相继式演算中的证明是树，它的根是我们要证明的定理，而它的叶子是公理模式实例；每个内部节点必须标记为要么Right →要么Left →，并且必须包含依据指定规则从子节点推出的一个公式。

相继式演算证明紧密的对应于λ-演算表达式。断言${\displaystyle \mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->a}$可以被解释为意味着，给定带有在Γ中列出类型的值，我们可以制造带有类型a的一个值。公理对应于带有新的无约束的类型的新变量介入。

Right →规则对应于函数抽象：

什么时候我们能结论出某个程序Γ包含类型α→β的函数?在Γ加上类型α的一个值的时候，包含了足够的机械来允许我们制造类型β的一个值。

Left →规则对应于函数应用：

如果我们可以制造类型α的一个值，并且如果给出类型β的一个值，我们还可以制造类型γ的一个值，则类型α→β的一个函数将允许我们制造类型γ的一个值：首先我们可以制造α，接着应用α→β函数于它，并接着使用结果的β值来制造类型γ的一个值。

例如，(β→α)→(γ→β)→γ→α的相继式演算如下：

(β→α)→(γ→β)→γ→α的证明告诉我们如何制造带有这个类型的一个λ-表达式。首先，介入分别带有类型α和β的变量a和b。Left →规则声称制造程序 (λb.a b)，它构造类型α的一个值。我们再次使用Left →来构造(λb.a (λg.b g))，它仍有类型α。