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

06-27

來自專欄類型論驛站

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

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

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

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

強[可]正規性（strong normalisation，或譯為強規範化性）是一個類型系統內在邏輯的可確定性的基石。Luo 採用了 Girard-Tait 可歸約性策略（reducibility method）來證明 ECC 的強正規性。

在有類型 λ 演算 à la Curry 學習筆記-4（強正規性）中， $lambda2 ext{-Curry}$ 的強正規性證明也採用了 Girard-Tait 可規約性策略。

基於項的結構的直接歸納難以證明強正規性，因為 $eta$ 歸約會得到一個更長的項。 Girard-Tait 策略是一種更強的歸納法。其主要步驟如下：

定義飽和集合（saturated sets）或可歸約性候選項（candidates of reducibility）。
定義基於類型變數賦值函數 $ho$ 的類型 $A$ 的釋義（指稱語義） $Eval_ ho A$ 。
證明 $Eval_ ho A$ 對於每一個類型 $A$ 來說都是一個飽和集合。
證明釋義 $Eval$ 的健全性（可靠性，soundness），即對於任意類型為 $A$ 的對象 $a$ ， $a$ 都屬於 $Eval_ ho A$ 。
最後，基於飽和集合的定義，飽和集合中的每一個項都是（強）正規的。

子章節目錄：

零、環境

一、飽和集合

二、指稱

三、指派和賦值（見下次筆記）

四、釋義和取值（見下次筆記）

五、釋義的健全性和強正規性（見下次筆記）

零、環境

定義1（環境，environment）

環境 $mathcal{E}$ 是一個無限序列

$mathcal{E}equiv e_1:E_1, e_2:E_2,dots$

其中 $e_1$ 是一個變數， $E_i$ 是一個項，使得對於任何 $iinomega$ ，

$mathcal{E}^iequiv e_1:E_1,dots,e_i:E_i$ 是一個有效語境（valid context），且
對於任何 $mathcal{E}^i$ 類型 $A$ 來說，都存在無限多的 $k$ 使得 $E_kequiv A$

引理1（環境是是存在的）

存在一個環境。

一、飽和集合

定義2（基項，base terms）

基項和基項的關鍵變數（key variable）歸納地定義於項的結構如下：

一個變數是一個基項，同時也是其自身的關鍵變數；
如果 $M$ 是一個基項，那麼 $MN$ ， $pi_1(M)$ 以及 $pi_2(M)$ 也都是基項，它們的關鍵變數就是 $M$ 的關鍵變數。

基於上述定義，可知如果 $M$ 是基項，且 $M hd M$ ，那麼 $M$ 也是一個基項。如果變數 $y$ 不同於基項 $M$ 的關鍵變數，那麼 $[N/y]M$ 也是一個基項。

定義3（關鍵規約式，key redex）

項 $M$ 的關鍵規約式定義如下：

如果 $M$ 是一個規約式，那麼 $M$ 擁有一個關鍵規約式，即其本身；
如果 $M$ 擁有一個關鍵規約式，那麼 $MN, pi_1(M)$ 以及 $pi_2(M)$ 也都擁有一個關鍵規約式，它們的關鍵規約式就是 $M$ 的關鍵規約式。

因此，一個項至多有一個關鍵規約式。若 $M$ 有關鍵規約式，我們用 $ext{red}_k(M)$ 來表示收縮了這個關鍵規約式之後的結果。

引理2

如果 $M$ 擁有關鍵規約式，且沒有收縮任何關鍵規約式，我們有 $M hd M$ ，那麼 $ext{red}_k(M) hd ext{red}_k(M)$ 。

接下來，我們就可以定義飽和集合了。設 $A$ 為一個 $mathcal{E}$ -類型，那麼 $SN(A)$ 用來表示在 $mathcal{E}$ 中類型為 $A$ 所有強可正規項的集合。

定義4（飽和集合，saturated sets）

設 $A$ 為一個 $mathcal{E}$ -類型。 $S$ 是一個 $A$ -飽和集合（A-saturated set）當且僅當

（S1） $Ssubseteq SN(A)$

（S2）如果 $Min SN(A)$ 是一個基項，那麼 $Min S$

（S3）如果 $Min SN(A)$ 有一個關鍵規約式，且 $ext{red}_k(M)in S$ ，那麼 $Min S$

$Sat(A)$ 定義為 $A$ -飽和集合的集合。

二、指稱

我們需要先定義偽正規性，即不涉及命題類型的直謂性類型層面上的一種「偽正規性」。

定義5（ $mathcal{E}$ -類型的層次，levels）

$mathcal{E}$ -類型 $A$ 的層次 $mathcal{L}(A)$ 定義如下：

如果 $A$ 是一個 $mathcal{E}$ -命題，那麼 $mathcal{L}(A)=_{df} -1$
如果 $A$ 不是一個個 $mathcal{E}$ -命題，那麼 $mathcal{L}(A)$ 定義為對於某個 $Bsimeq A$ ，能夠滿足 $mathcal{E}vdash B:Type_j$ 的最小 $jin omega$ 。

定義6（偽正規式，quasi-normal forms，或譯為準正規式）

一個 $mathcal{E}$ -對象是偽正規的當且僅當它不包含任何主項包含非命題主要類型的 $sigma$ -規約式或 $eta$ -規約式。

任何一個偽正規的 $mathcal{E}$ -類型都只可能是下列四種形式之一：一個宇宙 $U$ ，一個基項， $Pi x:A.B$ 或 $Sigma x:A.B$ 。

層次和度（degree）是類型的複雜性量度的兩個方面。下面我們定義度：

定義7（ $j$ -度）

$mathcal{E}$ -類型 $A$ 對於任何 $jinomega$ 的 $j$ -度 $mathcal{D}_jA$ 定義如下：

如果 $A$ 是偽正規式，那麼 $mathcal{D}_jA$ 歸納地定義如下：

如果 $mathcal{L}(A) eq j$ ，那麼 $mathcal{D}_j A =_{df} 0$
如果 $Aequiv Type_{j-1}$ ，那麼 $mathcal{D}_j A=_{df} 1$
如果 $A$ 是一個基項，且 $mathcal{L}(A)=j$ ，那麼 $mathcal{D}_j A =_{df} 1$
如果 $Aequiv Pi x:A_1.A_2$ 或 $Aequiv Sigma x:A_1.A_2$ ，且 $mathcal{L}(A)=j$ ，那麼 $mathcal{D}_j A =_{df} max {mathcal{D}_j A _1,mathcal{D}_j A _2}+1$

如果 $A$ 不是偽正規式，那麼設 $A^circ$ 為滿足 $A hd A^circ$ 的偽正規 $mathcal{E}$ -類型，那麼 $mathcal{D}_jA=_{df}D_jA^circ$

定義8（ $mathcal{E}$ -類型的複雜性 $eta$ ）

$eta A=_{df}(mathcal{L}(A)+1,mathcal{D}_{mathcal{L}(A)}A)$

藉助上述定義，Luo 證明了 ECC 系統的偽正規性。

接著，我們來定義指稱集合（denotation-sets），即 $mathcal{E}$ -對象的可能指稱的集合。具體來說， $mathcal{E}$ -類型 $A$ 的可能指稱就是 $A$ -飽和集合。

定義9（ $mathcal{E}$ -對象的指稱集合）

$mathcal{E}$ -對象 $M$ 的（可能）指稱集合 $V(M)$ ，依照其主要類型 $T_mathcal{E}(M)$ 的形式定義，該類型是一個偽正規式（quasi-normal form），定義還依照複雜性量度（complexity measure） $eta(T_mathcal{E}(M))$ 上的歸納：

如果 $T_mathcal{E}(M)$ 是一個宇宙，即 $M$ 是一個 $mathcal{E}$ -類型，那麼 $V(M)=_{df} Sat(M)$
如果 $T_mathcal{E}(M)$ 是一個 $mathcal{E}$ -命題（即 $M$ 是一個 $mathcal{E}$ -證明），那麼 $V(M)=_{df} { heta}$ ，其中 $heta$ 是一個固定的任意符號。
如果 $T_mathcal{E}(M)$ 是一個基項，那麼 $V(M)=_{df}{ heta}$
如果 $T_mathcal{E}(M)equiv Pi x:A_1.A_2$ 是一個非命題 $mathcal{E}$ -類型，那麼 $V(M)$ 定義為滿足下列條件的函數 $f$ 的集合：（a） $f$ 的定義域 $dom (f)={(N,v)mid mathcal{E}vdash N:A_1,vin V(N)}$ ；（b）對於 $(N,v)in dom(f)$ ， $f(N,v)in V(MN)$ ；（c）對於滿足 $Nsimeq N$ 的 $(N,v),(N,v)in dom(f)$ ， $f(N,v)=f(N,v)$
如果 $T_mathcal{E}(M)equiv Sigma x:A_1.A_2$ ，那麼 $V(M)={df}{(v_1,v_2)mid v_1in V(pi_1(M)),v_2in V(pi_2(M))}$