Curry-Howard 同构

定义

Curry-Howard 同构（Curry-Howard correspondence）指逻辑系统与计算系统之间的结构性对应：逻辑命题对应程序类型，命题的证明对应该类型的程序（项），证明化简对应程序求值。该对应由 Haskell Curry 与 William Howard 先后揭示。

对应关系

具体而言：蕴含 A→B 对应函数类型 A→B；合取 A∧B 对应积类型（元组）；析取 A∨B 对应和类型；恒真对应单元类型；恒假对应空类型；全称量词与存在量词分别对应依赖类型中的 Π 类型与 Σ 类型。直觉主义逻辑对应简单类型 λ 演算，经典逻辑则与续延（continuation）机制相关。

应用

Coq、Agda、Lean 等证明助手直接建立在这一同构之上：写出类型正确的程序就是完成证明。

意义

它把逻辑学、类型论与程序设计统一起来，是现代编程语言理论最重要的思想之一。