構造演算(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)