构造微积分

在数理逻辑和计算机科学中，构造微积分（CoC）是ThierryCoquand创建的一种类型理论。

它既可以作为一种类型化的编程语言，也可以作为数学的构造基础。基于这第二个原因，CoC及其变体一直是Coq和其他证明辅助工具的基础。

它的一些变体包括归纳构造的微积分（增加了归纳类型），（共同）归纳构造的微积分（增加了共同归纳），以及归纳构造的预测性微积分。

CoC是一个高阶类型的λ微积分，最初由ThierryCoquand开发。它因处于Barendregt的lambdacube的顶端而闻名。

在CoC中可以定义从术语到术语的函数，以及术语到类型，类型到类型，以及类型到术语的函数。CoC是强规范化的，因此也是一致的。

根据哥德尔不完全性定理，不可能从CoC内部证明一致性。

CoC是与Coq证明助手一起开发的。随着该理论功能的增加（或可能的责任的删除），它们在Coq中也可用。CoC的变种被用于其他证明助手，如Matita。

构造微积分可以被认为是库里-霍华德同构的延伸。

库里-霍华德同构将简单类型的λ微积分中的一个术语与直觉命题逻辑中的每个自然演绎证明联系起来。

构造微积分将这种同构扩展到完整的直觉主义谓词微积分中的证明，其中包括量化语句的证明（我们也将称之为命题）。

在构造微积分中，一个术语是用以下规则构造的。{displaystyle(λx:A.B)},{displaystyle(λx:A.B)}是变量。证明，是类型为命题的术语；命题，也被称为小类型；谓词，是返回命题的函数；大类型，是谓词的类型(P{displaystylemathbf{P}}}就是一个大类型的例子）。{displaystylemathbf{T}}是大类型的例子；T}本身，这是大类型的类型。

构造的微积分允许证明类型判断。构造微积分的有效判断可以从一组推理规则中推导出来。在文中，我们使用{displaystyle/Gamma}是指一个类型赋值序列。