构造演算

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

CoC 最初由 Thierry Coquand 开发。

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

构造演算的基础

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

项

在构造演算中项使用如下规则构造：

• T 是项（也叫做类型）
• P 是项（也叫做命题，所有命题的类型）
• 变量 $x,y,z...$ 是项
• 如果 $A$ 和 $B$ 是项，则如下也是项
  • $\mathbf{(}AB)$
  • ($\mathit{\lambda }x:A.B$)
  • ($\mathrm{\forall }x:A.B$)

构造演算有 5 种对象类型：

1. 证明，它是其类型都是命题的那些项
2. 命题，也叫做小类型
3. 谓词，它是返回命题的函数
4. 大类型，它是谓词的类型。（P 是大类型的例子）
5. T 自身，它是大类型的类型。

判断

在构造演算中，判断是类型推理：

$x_1:A_1,x_2:A_2,\dots ⊢t:B$

它可以被读作蕴涵

如果变量 $x_1,x_2,\dots$ 分别有类型 $A_1,A_2,\dots$，则项 $t$ 有类型 $B$。

构造演算的有效判断是从推理规则集合可推导的。在下面，我们使用 $\mathrm{\Gamma }$ 来指示类型指派的序列 $x_1:A_1,x_2:A_2,\dots$，并使用 K 来指示要么 P 要么 T。我们将写 $A:B:C$ 来指示“$A$ 有类型 $B$，和 $B$ 有类型 $C$”。我们将写 $B(x:=N)$ 来指示用项 $N$ 代换在项 $B$ 中变量 $x$ 的结果。

推理规则用如下形式写成

$\frac{\mathrm{\Gamma }⊢A:B}{{\mathrm{\Gamma }}^{\prime }⊢C:D}$

它指示着

如果 $\mathrm{\Gamma }⊢A:B$ 是有效判断，则 ${\mathrm{\Gamma }}^{\prime }⊢C:D$ 也是。

构造演算的推理规则

1. $\frac{}{⊢P:T}$
   
   
2. $\frac{\mathrm{\Gamma }⊢A:K}{\mathrm{\Gamma },x:A⊢x:A}$
   
   
3. $\frac{\mathrm{\Gamma },x:A⊢t:B:K}{\mathrm{\Gamma }⊢(\lambda x:A.t):(\mathrm{\forall }x:A.B):K}$
   
   
4. $\frac{\mathrm{\Gamma }⊢M:(\mathrm{\forall }x:A.B)\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢MN:B(x:=N)}$

定义逻辑运算

构造演算在引入基本算子的时候是非常简约的：唯一形成命题的逻辑算子是 $\mathrm{\forall }$。但是，这个唯一的算子足够定义所有其他逻辑算子：

$\begin{array}{cccc}A\Rightarrow B& \equiv & \mathrm{\forall }x:A.B& (x\notin B)\\ A\wedge B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow B\Rightarrow C)\Rightarrow C& \\ A\vee B& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C& \\ \mathrm{\neg }A& \equiv & \mathrm{\forall }C:P.(A\Rightarrow C)& \\ \mathrm{\exists }x:A.B& \equiv & \mathrm{\forall }C:P.(\mathrm{\forall }x:A.(B\Rightarrow C))\Rightarrow C& \end{array}$

定义数据类型

在构造演算中可以定义计算机科学中使用的基本数据类型：

布尔

$\mathrm{\forall }A:P.A\Rightarrow A\Rightarrow A$

自然数

$\mathrm{\forall }A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)$

乘积 $A\times B$

$A\wedge B$

不交并 $A+B$

$A\vee B$

参见

• Curry-Howard同构
• 直觉逻辑
• 直觉类型论
• Lambda 演算
• Lambda立方体
• 系统F
• 有类型 lambda 演算

引用

• Thierry Coquand and Gerard Huet: The Calculus of Constructions. Information and Computation, Vol. 76, Issue 2-3, 1988.
• For a source freely accessible online, see Coquand and Huet: The calculus of constructions。Technical Report 530, INRIA, Centre de Rocquencourt, 1986.
• M. W. Bunder and Jonathan P. Seldin: Variants of the Basic Calculus of Constructions Template:Wayback。2004.