Luos UTT學習筆記之三：元理論特性

來自專欄類型論驛站

Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.

目錄：類型論驛站寫作計劃

前一篇：Luos UTT學習筆記之二：擴充構造演算（ECC）簡介

後一篇：Luos UTT 學習筆記之四：強[可]正規性-上

在 Luo 1994 的第三章，作者研究了 ECC （擴充構造演算）的四大基本的元理論特性：Church-Rosser 定理，彙集性，判斷的可推導性，以及主要類型原則。

Church-Rosser 定理表明了可轉換項無論通過何種歸約途徑，最終都可以歸約為同一個項。這樣就確保了正規式（即計算結果）的唯一性。

定理1（Church-Rosser 定理）

如果 ，那麼存在 ，使得 且 。

Church-Rosser 定理的證明可以參見 無類型Lambda演算筆記-3（歸約和Church-Rosser定理）。Luo 的書中給出了如下證明策略：

首先定義平行一步歸約和平行 步歸約。一步歸約記為 ，通過對 中的可規約式（redex）從內到外（參見無類型 Lambda 演算筆記 3 中的 Lambda項的頭正規和頭歸約表示）進行歸約而得到正規式 。平行 步歸約可以歸納地定義為： 當且僅當 為正規式； 當且僅當存在某個 使得 。

然後通過平行一步歸約的定理來證明引理 。再通過這個引理證明引理 。

最後再多次使用上述引理證明。從而證明 Church-Rosser 定理。

如果納入 收縮模式，那麼 ECC 便不再具備 Church-Rosser 特性。

Church-Rosser 定理的一個重要推論就是正規式的唯一性。

接著，Luo 又介紹了彙集關係及其特性。

定義1（累積（彙集，cumulativity）關係的定義，版本1）

累積關係 被定義為項之間最小的二元關係：

1. 是一個基於轉換的偏序（partial order），即

（a）如果 ，則 ；

（b）如果 ，則 ；以及

（c）如果 ，則 。

2. ;

3. 如果 ，則

4. 如果 ，則

此外， 當且僅當 。

歸納地，我們可以如下定義彙集關係：

定義2（累積（彙集，cumulativity）關係的定義，版本2）

歸納地定義 為項之間的關係如下：

1. 當且僅當滿足下列條件之一：

(a)

(b) 對於某個

(c) 對於某些 ,

2. 當且僅當滿足下列條件之一：

(a)

(b) 對於某些 ，

(c) 對於某些 ，

3. 此外，我們定義 為 ，定義 當 。

Luo 證明了這兩種定義的等同性。

[可推導判斷] 如果一個判斷 （其中 ）是可以推導的，那麼

• 是有效語境（valid context）；
• 和 分別是語境 和 中的類型；
• 變數 互不相同， 和 中的自由變數取自 ， 中的自由變數取自

除此以外，下列四種操作保存判斷的可推導性：

• 用 進行語境替換（context replacement）
• 類型保存轉換（type-preserving substitution）或切（cut）
• 主語歸約（subject reduction）
• 弱化和強化（weakening and strengthening）

在這一章的最後，Luo 介紹了主要類型（principal types）這一概念。由於類型包含是由宇宙引發的，ECC 中上至轉換的類型唯一性不能成立。但主要類型概念的提出可以使得 ECC 的類型推導演算法變得簡單而直接。

定義3（主要類型）

被稱為 在 中的的主要類型當且僅當 且對於任意 ， 當且僅當 且 是一個 -類型。

實例：

1. 如果 中出現了 ，那麼 是 在 中的主要類型；
2. 是 在 中的的主要類型；
3. 如果 ，那麼 是 在 中的主要類型。

目錄：類型論驛站寫作計劃

前一篇：Luos UTT學習筆記之二：擴充構造演算（ECC）簡介

後一篇：Luos UTT 學習筆記之四：強[可]正規性-上

推薦閱讀：