Curry–Howard 对应

形式陈述 ​

先固定本页的核心系统：带蕴含、合取、析取与假命题的直觉主义命题自然演绎，对应带函数、积、和与空类型的简单类型 λ 演算公理库简单类型 λ 演算Simply typed lambda calculus · STLC以基础类型和箭头类型约束 λ 项，获得类型安全与强正规化的最小函数演算。。在这对具体演算之间，命题对应类型，证明推导对应有类型项，证明化简对应程序归约。基本连接为

$$A\Rightarrow B\leftrightarrow A\to B,A\wedge B\leftrightarrow A\times B,A\vee B\leftrightarrow A+B,\mathrm{\perp }\leftrightarrow 0.$$

自然演绎的引入规则对应类型的构造器，消去规则对应使用方式；β-归约消去“刚构造后立刻拆解”的局部迂回。对归纳类型公理库归纳类型Inductive type · Inductive datatype由有限构造步骤生成的最小递归数据类型，并以严格正性保障其递归结构良好。，构造器给出证明的引入方式，依赖消去子公理库消去子、递归子与归纳原理Eliminator · Recursor · Induction principle由归纳类型的构造器导出消费数据、定义递归函数和证明依赖性质的规则。把 motive、基例与归纳步组合成归纳证明。

更强系统必须逐对命名。System F 的全称类型 $\mathrm{\forall }\alpha .T$ 对应直觉主义二阶命题逻辑中的命题量化，其 impredicative polymorphism 允许量词实例化为仍含全称量词的类型；这不是任意经典二阶模型语义。依赖函数与依赖对分别对应带项量词的直觉主义逻辑中的 $\mathrm{\forall }$ 与 $\mathrm{\exists }$。线性逻辑则限制 weakening 与 contraction，并由子结构类型系统公理库子结构类型系统Substructural type system · Resource-sensitive type system通过限制弱化、收缩或交换等上下文结构规则，静态约束假设与程序资源的使用方式。解释资源使用。

在序列演算中，与这种正规化密切对应的是 cut elimination；二者服务于同一“消去中间引理”的结构，但在未指定证明系统及翻译前，不能直接把 β-归约与某一条 cut 规则视为同一个关系。

直觉

一个命题要被证明，就必须构造出携带其证据的数据；一个类型要有居民，就必须写出满足接口的程序。蕴含证明接收 $A$ 的证据并产生 $B$ 的证据，所以它正是函数；合取证据同时含两部分，所以是积；析取证据必须标明哪一侧，所以是和。运行证明项不是在检验真值，而是在消除证明中的中间构造，使证据正规化。对应是精确的形式翻译，不是“所有程序都有随便一个数学寓意”的宽泛比喻。

例子与边界

命题 $A\Rightarrow A$ 的证明对应恒等项 $\lambda x:A.x$。命题 $A\wedge B\Rightarrow B\wedge A$ 的证明对应

$$\lambda p:A\times B.({\pi }_{2}p,{\pi }_{1}p).$$

对析取作分类讨论，正对应对和类型做模式匹配。

边界是经典排中律 $A\vee \mathrm{\neg }A$：纯简单类型 λ 演算一般不能为任意 $A$ 构造其居民。要对应经典自然演绎或经典序列演算，需另行选择 CPS 翻译、双重否定翻译或带类型的续延/控制算子；这会改变项语言与归约行为，不能把“经典”二字直接贴到上述 STLC 或 System F 对应上。命题对应的是类型的可居住性，而不是说类型中的任意比特模式都天然是一份可信证明。

推论与应用

该对应把简单类型 λ 演算与直觉主义命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。统一起来；System F 和依赖类型则分别沿上述二阶命题量化与项依赖方向扩展。证明助理的内核通过类型检查验证证明项，程序提取再从构造性证明中得到算法。

证明正规化公理库正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。支撑逻辑一致性，积类型和和类型的程序规则也由逻辑引入/消去规则系统解释。Coq、Agda、Lean 以及 proof-carrying code 都建立在这一桥梁之上。

参考资料

• William A. Howard, “The Formulae-as-Types Notion of Construction,” 1980.
• Morten Heine Sørensen and Paweł Urzyczyn, Lectures on the Curry–Howard Isomorphism, Elsevier, 2006.