查看“︁构造演算”︁的源代码

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

CoC 最初由 [[Thierry Coquand]] 开发。

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

==构造演算的基础==

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

==项==

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

* '''T''' 是项（也叫做'''类型'''）
* '''P''' 是项（也叫做'''命题'''，所有命题的类型）
* 变量 <math>x, y, z...</math> 是项
* 如果 <math>A</math> 和 <math>B</math> 是项，则如下也是项
** <math>\mathbf{(} A B )</math>
** (<math>\mathbf{\lambda}x:A . B</math>)
** (<math>\forall x:A . B</math>)

构造演算有 5 种对象类型：
# '''证明'''，它是其类型都是命题的那些项
# '''命题'''，也叫做'''小类型'''
# '''谓词'''，它是返回命题的函数
# '''大类型'''，它是谓词的类型。（'''P''' 是大类型的例子）
# '''T''' 自身，它是大类型的类型。

==判断==

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

:<math> x_1:A_1, x_2:A_2, \ldots \vdash t:B</math>

它可以被读作蕴涵

: 如果变量 <math>x_1, x_2, \ldots</math> 分别有类型 <math>A_1, A_2, \ldots</math>，则项 <math>t</math> 有类型 <math>B</math>。

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

推理规则用如下形式写成

:<math> {\Gamma \vdash A:B} \over {\Gamma' \vdash C:D} </math><br><br>

它指示着

: 如果 <math> \Gamma \vdash A:B </math> 是有效判断，则 <math> \Gamma' \vdash C:D </math> 也是。

==构造演算的推理规则==

# <math> {{} \over {} \vdash P : T} </math><br><br>
# <math> {\Gamma \vdash A : K \over 
{\Gamma, x:A \vdash x : A}} </math><br><br>
# <math> {\Gamma, x:A \vdash t : B : K \over 
{\Gamma \vdash (\lambda x:A . t) : (\forall x:A . B) : K}} </math><br><br>
# <math> {\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma
\vdash N : A \over 
{\Gamma \vdash M N : B(x := N)}} </math>

==定义逻辑运算==

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

: <math>
\begin{matrix}
A \Rightarrow B & \equiv & \forall x:A . B & (x \notin B) \\
A \wedge B      & \equiv & \forall C:P . (A \Rightarrow B \Rightarrow C) \Rightarrow C & \\
A \vee B        & \equiv & \forall C:P . (A \Rightarrow C) \Rightarrow (B \Rightarrow C) \Rightarrow C & \\
\neg A          & \equiv & \forall C:P . (A \Rightarrow C) & \\
\exists x:A.B   & \equiv & \forall C:P . (\forall x:A.(B \Rightarrow C)) \Rightarrow C &
\end{matrix}
</math>

==定义数据类型==

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

; [[布尔逻辑|布尔]]: <math>\forall A: P . A \Rightarrow A \Rightarrow A</math>
; [[自然数]]: <math>\forall A:P . (A \Rightarrow A) \Rightarrow (A \Rightarrow A)</math>
; [[笛卡尔乘积|乘积]] <math>A \times B</math>: <math>A \wedge B</math>
; [[不交并]] <math>A + B</math>: <math>A \vee B</math>

==参见==
* [[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: [https://web.archive.org/web/20061128014645/http://www.inria.fr/rrrt/rr-0530.html The calculus of constructions]。Technical Report 530, INRIA, Centre de Rocquencourt, 1986.
*  M. W. Bunder and Jonathan P. Seldin: [http://citeseer.ist.psu.edu/bunder04variants.html Variants of the Basic Calculus of Constructions] {{Wayback|url=http://citeseer.ist.psu.edu/bunder04variants.html |date=20070310222532 }}。2004.

[[Category:Lambda演算]]
[[Category:类型论]]