构造演算

维基百科,自由的百科全书
跳转至: 导航搜索

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

CoC 最初由 Thierry Coquand 开发。

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

构造演算的基础[编辑]

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

[编辑]

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

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

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

  1. 证明,它是其类型都是命题的那些项
  2. 命题,也叫做小类型
  3. 谓词,它是返回命题的函数
  4. 大类型,它是谓词的类型。(P 是大类型的例子)
  5. 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

构造演算的有效判断是从推理规则集合可推导的。在下面,我们使用 \Gamma 来指示类型指派的序列  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 也是。

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

  1.  {{} \over {} \vdash P : T}

  2.  {\Gamma \vdash A : K \over 
{\Gamma, x:A \vdash x : A}}

  3.  {\Gamma, x:A \vdash t : B : K \over 
{\Gamma \vdash (\lambda x:A . t) : (\forall x:A . B) : K}}

  4.  {\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

参见[编辑]

引用[编辑]