Curry–Howard 对应

形式陈述 ​

先固定本页的核心系统：带蕴含、合取、析取与假命题的直觉主义命题自然演绎理路直觉主义命题逻辑Intuitionistic propositional logic · IPC · IPL以构造性证明规则解释命题联结词、且不无条件接受排中律或双重否定消去的逻辑。，对应带函数、积、和与空类型的简单类型 λ 演算理路简单类型 λ 演算Simply typed lambda calculus · STLC以基础类型和箭头类型约束 λ 项，获得类型安全与强正规化的最小函数演算。。在这对具体演算之间，命题对应类型，证明推导对应有类型项，证明化简对应程序归约。基本连接为

自然演绎的引入规则对应类型的构造器，消去规则对应使用方式；β-归约消去“刚构造后立刻拆解”的局部迂回。对归纳类型理路归纳类型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 规则视为同一个关系。