Curry-Howard同构

维基百科，自由的百科全书

Curry-Howard 对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做 Curry-Howard 同构或公式为类型对应。已经采用了一些不同的公式化，它的原理现在被认为是由美国数学家 Haskell Curry 和逻辑学家 William Alvin Howard 独立发现的。

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

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

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

[编辑] 类型

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

v (这里的 v 是个变量)
λv.E (这里的 v 是个变量，而 E 是个 λ-演算表达式)
(E F) (这里的 E 和 F 是 λ-演算表达式)

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

类型可以依赖于类型变量，它被指示为小写的希腊字母 α, β 等等。在我们概念中类型变量是被隐含的全称量化的，就是说，如果一个值有包括类型变量的一个类型，则它必须由这个类型变量的所有可能实例组成。我们可以定义任意表达式的类型为如下: 一个变量比如 x 可以有任意类型。如果变量 x 有类型 α，而表达式 E 有类型 β，则 λx.E 有指示为 α → β 的类型；就是说，它是取类型 α 的值，并映射到类型 β 的值。在表达式 (E F) 中，如果 F 有类型 α，则 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，忽略参数，并返回恒等函数)，却没有类型 (α → α) → β 的函数，如果存在的话，它会是转换恒等函数到任意值的函数。

[编辑] 直觉逻辑

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

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

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

[编辑] 希尔伯特式证明

形式上刻画直觉逻辑的一个简单方式如下。它有两个公理模式。所有形式为

α → β → α

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

(α → β → γ) → (α → β) → α → γ

的公式都是公理。

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

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

[编辑] 程序是证明

Curry-Howard 同构的第二个方面是其类型对应于一个程序自身对应于这个公式的一个证明。

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

K: λxy.x

S: λxyz. (x z (y z))

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

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

[编辑] 证明 α → α

作为一个简单的例子，我们将构造定理 α → α 的证明。这是恒等函数 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，这次是替代 α 为 (β → γ)，替代 β 为 α:

α → β → α

(β → γ) → α → (β → γ)

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

(β → γ) → (α → β) → α → γ

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

(β → α) → (γ → β) → γ → α

这就是我们要证明的。

[编辑] 相继式演算

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

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

${{} \over \Gamma, \alpha \vdash\alpha }$ (公理)

${ \Gamma, \alpha\vdash\beta \over \Gamma\vdash\alpha\rarr\beta}$ (Right →)

${\Gamma\vdash\alpha\qquad\qquad\Sigma, \beta\vdash\gamma \over \Gamma, \Sigma, \alpha\rarr\beta \vdash \gamma}$ (Left →)

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

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

$\cfrac { \gamma \vdash \gamma \qquad \cfrac { \beta \vdash \beta \qquad \alpha \vdash \alpha} {\beta,\beta \rightarrow \alpha \vdash \alpha} Left \rightarrow }{\qquad \cfrac {\gamma, \beta \rightarrow \alpha, \gamma \rightarrow \beta \vdash \alpha } { \qquad \cfrac {\beta \rightarrow \alpha, \gamma \rightarrow \beta \vdash \gamma \rightarrow \alpha } { \qquad \cfrac { \beta \rightarrow \alpha \vdash (\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha } { \vdash (\beta \rightarrow \alpha) \rightarrow (\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha } Right \rightarrow } Right \rightarrow } Right \rightarrow } Left \rightarrow$

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

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

${ \Gamma, \alpha\vdash\beta \over \Gamma\vdash\alpha\rarr\beta}$ (Right →)

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

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

${ \Gamma \vdash \alpha \qquad \Sigma, \beta \vdash \gamma \over \Gamma, \Sigma, \alpha\rarr\beta \vdash\gamma}$ (Left →)

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

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