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

07-09

來自專欄類型論驛站

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

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

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

後一篇：Luos UTT 學習筆記之六：ECC 的內部邏輯

子章節目錄：

零、環境（見上次筆記）

一、飽和集合（見上次筆記）

二、指稱（見上次筆記）

三、指派和賦值

四、釋義和取值

五、釋義的健全性和強正規性

三、指派和賦值

引理1（同時替換引理, simultaneous substitution）

如果 $mathcal{E}^kvdash M:A$ ，且對於所有 $ile k,mathcal{E}vdash N_i:[N_1,dots,N_{i-1}/e_1,dots,e_{i-1}]E_i$ ，那麼

$mathcal{E}vdash [N_1,dots,N_k/e_1,dots,e_k]M:[N_1,dots,N_k/e_1,dots,e_k]A$ .

定義1（ $mathcal{E}$ -指派和 $mathcal{E}$ -賦值，E-assignment and E-valuation）

$mathcal{E}$ -指派是函數 $phi:FV(mathcal{E^k}) omathcal{T}$ ，其中 $kinomega$ 且對於每一個 $1le ile k, mathcal{E}_iequiv e_i:E_i$ ，我們有 $mathcal{E}vdash phi(e_i):phi(E_i)$ 。

$mathcal{E}$ -賦值是一對函數 $ho=(phi,val)$ ，其中 $phi$ 是一個 $mathcal{E}$ -指派， $val$ 的定於域就是 $phi$ 的定義域。對於每個 $e_iin dom(phi), val(e_i)in V(phi(e_i))$ 。 $ho$ 的定義域也就是 $phi$ 的定義域。

以 $FV(mathcal{E}^k)$ 為定義域的 $mathcal{E}$ -賦值 $ho$ 涵蓋（covers）一個 $mathcal{E}$ -對象 $M$ 當且僅當對於某個 $A$ ，我們有 $mathcal{E}^kvdash M:A$ 。

四、釋義和取值

在這裡，釋義（interpretation）就是取值（evaluation）。

定義2（取值，Evaluation）

設 $ho =(phi, val)$ 為一個 $mathcal{E}$ -賦值。 $ho$ 所 涵蓋（covers）的 $mathcal{E}$ -對象的取值函數 $Eval_ ho$ 定義如下：

如果 $M$ 是一個 $mathcal{E}$ -證明，那麼 $Eval_ ho(M)=_{df} heta$ .
如果 $M$ 不是一個 $mathcal{E}$ -證明，那麼 $Eval_ ho$ 可以基於 $M$ 的結構遞歸地定義如下：

（a）如果 $M$ 是一個宇宙，那麼 $Eval_ ho(M)=_{df} SN(M)$ 。

（b）如果 $M$ 是一個變數，那麼 $Eval_ ho(M)=_{df} val(M)$ 。

（c）如果 $Mequiv Pi x:M_1.M_2$ 。我們可以假定 $x otin dom( ho)$ ，那麼 $Eval_ ho(M)$ 定義為滿足下列條件的項 $F$ 的集合：i. $mathcal{E}vdash F:phi(M)$ ，且 ii. 對於每一個擴展 $ho$ ，使得 $phi(x)=Nin Eval_ ho(M_1)$ 的 $mathcal{E}$ -賦值 $ho=(phi,val)$ ， $FNin Eval_{ ho}(M_2)$ 。

（d）如果 $Mequiv lambda x:M_1.M_2$ 。我們可以假定 $x otin dom( ho)$ ，那麼 $Eval_ ho(M)$ 定義為滿足下列條件的函數 $f$ 的集合：i. $dom(f)={(N,v)mid mathcal{E}vdash N:phi(M_1),vin V(N)}$ ，且 ii. 對於 $(N,v)in dom(f),$ $f(N,v)=Eval_{ ho}(M_2)$ 其中 $ho$ 擴展擴展 $ho$ ，使得 $ho(x)=(N,v)$ 。

（e）如果 $Mequiv M_1M_2$ 。 $Eval_ ho(M)=_{df} Eval_ ho(M_1)(phi(M_2),Eval_ ho(M_2))$ 。

（f）如果 $Mequiv Sigma x:M_1.M_2$ 。我們可以假定 $x otin dom( ho)$ ，那麼 $Eval_ ho(M)$ 定義為滿足下列條件的項 $P$ 的集合：i. $mathcal{E}vdash P:phi(M)$ ，且 ii. 對於每一個擴展 $ho$ ，使得 $phi(x)=pi_1(P)$ 的 $mathcal{E}$ -賦值 $ho=(phi,val)$ ， $pi_1(P)in Eval_ ho(M_1)$ 且 $pi_2(P)in Eval_{ ho}(M_2)$ 。

（g）如果 $Mequivlangle M_1,M_2 angle _A$ 。 $Eval_ ho(M)=_{df}(Eval_ ho(M_1),Eval_ ho(M_2))$ 。

（h） $Mequiv pi_i(M).$ 那麼如果對於 $iin{1,2}$ ， $Eval_ ho(M)=(v_1,v_2)$ ，則有 $Eval_ ho(M)=_{df}v_i$ 。

引理2（Eval 的有效定義）

設 $ho=(phi,val)$ 為涵蓋 $mathcal{E}$ -對象 $M$ 的一個 $mathcal{E}$ -賦值。

如果 $mathcal{E}$ -賦值 $ho=(phi,val)$ 涵蓋 $M$ ，且對於每一個 $xin FV(M)$ ， $phi(x)simeqphi(x)$ 且 $val(x)=val(x)$ ，那麼 $Eval_ ho (M)= Eval_{ ho}(M)$ .
$Eval_ ho(M)in V(phi(M))$ 。

推論3

如果 $A$ 是一個 $mathcal{E}$ -類型，且 $ho=(phi,val)$ 是一個涵蓋 $A$ 的 $mathcal{E}$ -賦值，那麼 $Eval_ ho(A)$ 是一個 $phi(A)$ -飽和集合。

五、釋義的健全性和強正規性

引理4（替換特性，substitution property）

假設 $ho=(phi,val)$ 是一個涵蓋 $N$ 以及 $[N/x]M$ 的 $mathcal{E}$ -賦值，其中 $x otin dom( ho)$ ，且 $ho=(phi,val)$ 是涵蓋 $M$ 的一個 $ho$ -擴展，使得 $ho(x)=(phi(N),Eval_ ho(N))$ 。那麼 $Eval_ ho([N/x]M)=Eval_ ho(M)$ 。

引理5（釋義尊重計算等同性和彙集關係）

假設 $ho=(phi,val)$ 是一個 $mathcal{E}$ -賦值。

如果 $ho$ 涵蓋 $mathcal{E}$ -對象 $M$ 和 $N$ 且 $Msimeq N$ ，那麼 $Eval_ ho(M)=Eval_ ho(N)$ 。
如果 $ho$ 涵蓋 $mathcal{E}$ -類型 $M$ 和 $N$ 且 $Mpreceq N$ ，那麼 $Eval_ ho(M)subseteq Eval_ ho(N)$ 。

引理6（健全性，soundness）

設 $ho=(phi,val)$ 是一個以 $FV(mathcal{E}^k)$ 為定義域的 $mathcal{E}$ -賦值，且對於 $e_iin dom( ho)$ ， $phi(e_i)in Eval_ ho(E_i)$ 。如果 $mathcal{E}^kvdash M:A$ ，那麼 $phi(M)in Eval_ ho(A)$ 。

定理7（強正規性1）

如果 $Gammavdash M:A$ ，那麼 $M$ 是強[可]正規[化]的。

定理8（強正規性2）

如果 $x_1:A_1,dots,x_n:A_nvdash M:A$ ，那麼 $A_1,dots,A_n,A$ 和 $M$ 都是強[可]正規[化]的。

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

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

後一篇：Luos UTT 學習筆記之五：ECC 的內部邏輯