构造演算(CoC)是高阶有类型 lambda 演算,这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数,同从整数到整数的函数一样。CoC 是强规范化的。
CoC 最初由 Thierry Coquand 开发。
CoC 是 Coq 定理证明器早期版本的基础;它后来的版本建造在归纳构造演算之上,这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中,归纳数据类型必须模拟为它们的多态解构函数。
构造演算的基础[编辑]
构造演算可以被当作 Curry-Howard同构的扩展。Curry-Howard 同构把在简单类型 lambda 演算中项关联上在直觉命题逻辑中自然演绎证明。构造演算扩展了这个同构为在完全的直觉谓词逻辑中的证明,这包括了量化陈述(它也叫做"命题")的证明。
在构造演算中项使用如下规则构造:
- T 是项(也叫做类型)
- P 是项(也叫做命题,所有命题的类型)
- 变量
是项
- 如果
和
是项,则如下也是项
![{\displaystyle \mathbf {(} AB)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6c8641dccd1861f5cd2847a784610f7e2942683a)
- (
)
- (
)
构造演算有 5 种对象类型:
- 证明,它是其类型都是命题的那些项
- 命题,也叫做小类型
- 谓词,它是返回命题的函数
- 大类型,它是谓词的类型。(P 是大类型的例子)
- T 自身,它是大类型的类型。
在构造演算中,判断是类型推理:
![{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8e7008dd0d3b06110b77e7dab6e23737a59178e)
它可以被读作蕴涵
- 如果变量
分别有类型
,则项
有类型
。
构造演算的有效判断是从推理规则集合可推导的。在下面,我们使用
来指示类型指派的序列
,并使用 K 来指示要么 P 要么 T。我们将写
来指示“
有类型
,和
有类型
”。我们将写
来指示用项
代换在项
中变量
的结果。
推理规则用如下形式写成
![{\displaystyle {\Gamma \vdash A:B} \over {\Gamma '\vdash C:D}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4aef5197e90b7f5dd04fed1bfd2bd4f1e1156a5b)
它指示着
- 如果
是有效判断,则
也是。
构造演算的推理规则[编辑]
![{\displaystyle {{} \over {}\vdash P:T}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fd4d3d391ce3c7100c0ef6b91cb9ffa7dcb749b8)
![{\displaystyle {\Gamma \vdash A:K \over {\Gamma ,x:A\vdash x:A}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28f7f33a1d9f0788e20ae06d07548e10abb2e8cd)
![{\displaystyle {\Gamma ,x:A\vdash t:B:K \over {\Gamma \vdash (\lambda x:A.t):(\forall x:A.B):K}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/58ff12109aedb1adb6590a44131c775fe6aa1982)
![{\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B(x:=N)}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff1b2e16d9065d7443c08a8f75e825185e66e78b)
定义逻辑运算[编辑]
构造演算在引入基本算子的时候是非常简约的:唯一形成命题的逻辑算子是
。但是,这个唯一的算子足够定义所有其他逻辑算子:
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6ade109adb555798de24db624f33b9041c4bc167)
定义数据类型[编辑]
在构造演算中可以定义计算机科学中使用的基本数据类型:
- 布尔
![{\displaystyle \forall A:P.A\Rightarrow A\Rightarrow A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/34ebd8538ed58b315f0c9257afbe7fbcf8db6e71)
- 自然数
![{\displaystyle \forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d14b3d5796b1114c586202c625479179cab461c)
- 乘积
![{\displaystyle A\times B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/65f31ae45b0098f06b5d22c38d317eb097a88fa9)
![{\displaystyle A\wedge B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e86fbe93c98e68dc66cd518c98d5f6a624f5022b)
- 不交并
![{\displaystyle A+B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4279cdbd3cb8ec4c3423065d9a7d83a82cfc89e3)
![{\displaystyle A\vee B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e4039c1a12cca22bb4df619c295c9a6f8be045f9)