构造演算

构造演算(CoC)是高阶 有类型 lambda 演算,这里的 类型是 一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数,同从整数到整数的函数一样。CoC 是 强规范化的。

CoC 最初由 Thierry Coquand 开发。

CoC 是 Coq 定理证明器早期版本的基础;它后来的版本建造在 归纳构造演算之上,这是带有对归纳 数据类型的天然支持的 CoC 扩展。在最初的 CoC 中,归纳数据类型必须模拟为它们的多态解构函数。

构造演算的基础

构造演算可以被当作 Curry-Howard同构的扩展。Curry-Howard 同构把在 简单类型 lambda 演算中项关联上在 直觉命题逻辑中自然演绎证明。构造演算扩展了这个同构为在完全的直觉谓词逻辑中的证明,这包括了量化陈述(它也叫做"命题")的证明。