構造演算

構造演算(CoC)是高階有類型 lambda 演算，這裏的類型是一級值。因此在 CoC 內有可能定義從整數到類型、從類型到類型的函數，同從整數到整數的函數一樣。CoC 是強規範化的。

CoC 最初由 Thierry Coquand 開發。

CoC 是 Coq 定理證明器早期版本的基礎；它後來的版本建造在歸納構造演算之上，這是帶有對歸納數據類型的天然支持的 CoC 擴展。在最初的 CoC 中，歸納數據類型必須模擬為它們的多態解構函數。

構造演算的基礎

構造演算可以被當作 Curry-Howard同構的擴展。Curry-Howard 同構把在簡單類型 lambda 演算中項關聯上在直覺命題邏輯中自然演繹證明。構造演算擴展了這個同構為在完全的直覺謂詞邏輯中的證明，這包括了量化陳述（它也叫做"命題"）的證明。

項

在構造演算中項使用如下規則構造：

• T 是項（也叫做類型）
• P 是項（也叫做命題，所有命題的類型）
• 變量 ${\displaystyle x,y,z...}$ 是項
• 如果 ${\displaystyle A}$ 和 ${\displaystyle B}$ 是項，則如下也是項
  • ${\displaystyle \mathbf {(} AB)}$
  • (${\displaystyle \mathbf {\lambda } x:A.B}$)
  • (${\displaystyle \forall x:A.B}$)

構造演算有 5 種對象類型：

1. 證明，它是其類型都是命題的那些項
2. 命題，也叫做小類型
3. 謂詞，它是返回命題的函數
4. 大類型，它是謂詞的類型。（P 是大類型的例子）
5. T 自身，它是大類型的類型。

判斷

在構造演算中，判斷是類型推理：

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$

它可以被讀作蘊涵

如果變量 ${\displaystyle x_{1},x_{2},\ldots }$ 分別有類型 ${\displaystyle A_{1},A_{2},\ldots }$，則項 ${\displaystyle t}$ 有類型 ${\displaystyle B}$。

構造演算的有效判斷是從推理規則集合可推導的。在下面，我們使用 ${\displaystyle \Gamma }$ 來指示類型指派的序列 ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$，並使用 K 來指示要麼 P 要麼 T。我們將寫 ${\displaystyle A:B:C}$ 來指示「${\displaystyle A}$ 有類型 ${\displaystyle B}$，和 ${\displaystyle B}$ 有類型 ${\displaystyle C}$」。我們將寫 ${\displaystyle B(x:=N)}$ 來指示用項 ${\displaystyle N}$ 代換在項 ${\displaystyle B}$ 中變量 ${\displaystyle x}$ 的結果。

推理規則用如下形式寫成

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

它指示着

如果 ${\displaystyle \Gamma \vdash A:B}$ 是有效判斷，則 ${\displaystyle \Gamma '\vdash C:D}$ 也是。

構造演算的推理規則

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

定義邏輯運算

構造演算在引入基本算子的時候是非常簡約的：唯一形成命題的邏輯算子是 ${\displaystyle \forall }$。但是，這個唯一的算子足夠定義所有其他邏輯算子：

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

定義數據類型

在構造演算中可以定義計算機科學中使用的基本數據類型：

布爾

${\displaystyle \forall A:P.A\Rightarrow A\Rightarrow A}$

自然數

${\displaystyle \forall A:P.(A\Rightarrow A)\Rightarrow (A\Rightarrow A)}$

乘積 ${\displaystyle A\times B}$

${\displaystyle A\wedge B}$

不交並 ${\displaystyle A+B}$

${\displaystyle A\vee B}$

參見

• 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: 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.