构造演算

维基百科，自由的百科全书

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

CoC 最初由 Thierry Coquand 开发。

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

[编辑] 构造演算的基础

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

[编辑] 项

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

T 是项(也叫做类型)
P 是项(也叫做命题, 所有命题的类型)
如果 A 和 B 是项，则如下也是项
- $\mathbf{(} A B )$
- ( $\mathbf{\lambda}x:A . B$ )
- ( $\forall x:A . B$ )

构造演算有 4 种对象类型:

证明，它是其类型都是命题的那些项
命题，也叫做小类型
谓词，它是返回命题的函数
大类型，它是谓词的类型。(P 是大类型的例子)
T 自身，它是大类型的类型。

[编辑] 判断

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

$x_1:A_1, x_2:A_2, \ldots \vdash t:B$

它可以被读作蕴涵

如果变量 $x_1, x_2, \ldots$ 分别有类型 $A_1, A_2, \ldots$ ，则项

t

有类型

B

。

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

推理规则用如下形式写成

${\Gamma \vdash A:B} \over {\Gamma' \vdash C:D}$

它指示着

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

[编辑] 构造演算的推理规则

${{} \over {} \vdash P : T}$
${\Gamma \vdash A : K \over {\Gamma, x:A \vdash x : A}}$
${\Gamma, x:A \vdash t : B : K \over {\Gamma \vdash (\lambda x:A . t) : (\forall x:A . B) : K}}$
${\Gamma \vdash M : (\forall x:A . B)\qquad\qquad\Gamma \vdash N : A \over {\Gamma \vdash M N : B(x := N)}}$

[编辑] 定义逻辑运算

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

$\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}$

[编辑] 定义数据类型

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

布尔: $\forall A: P . A \Rightarrow A \Rightarrow A$
自然数: $\forall A:P . (A \Rightarrow A) \Rightarrow (A \Rightarrow A)$
乘积 $A \times B$: $A \wedge B$
不交并 $A + B$: $A \vee B$

[编辑] 参见

[编辑] 引用

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. 2004.

来自“http://zh.wikipedia.org../../../%E6%9E%84/%E9%80%A0/%E6%BC%94/%E6%9E%84%E9%80%A0%E6%BC%94%E7%AE%97.html”

页面分类: 递归论 | 类型论

We provide Linux to the World