Cartesian Closed Categories 與簡單型別論 (二)

型別理論

簡單型別（simple type theory）由一部份的 lambda term 以及函數型別構成，我們先從基本的名稱開始講起。

變數（variable）僅是一個給定的可數集合的元素，通常用小寫英文字母 $x, y, z,\dots$ 代表，而 lambda term 係由以下規則建立的所有的 term

$$M := x \mid \lambda x . M \mid M M$$

其中 $x$ 爲一變數。有效的 lambda term 包含 $\lambda x . x$，$\lambda x . \lambda y . x$ 以及 $\lambda x . x x$ 等等。另外還有型別變數（type variable），我們常用 $\sigma, \tau, \dots$ 等希臘字母代表。對每個 term : type 的配對 $x : \tau := (x, \tau)$ 讀作 term $x$ 的型別為 $\tau$。最後，用作給定有限多個的(變數 : 型別變數)序列稱為環境（context）通常記作 $\Gamma := x_1:\tau_1,\, x_2:\tau_2,\, \dots,\, x_n:\tau_n$。

我們用 $\Gamma \vdash M : \tau$ 代表在環境 $\Gamma$ 下，lambda term $M$ 的型別爲 $\tau$，這樣的表述本身稱為 judgement。型別理論（type theory）或型別系統（type system）意指特定一組規則說明如何構造 $\Gamma \vdash M : \tau$。通常包含一組基本的結構規則（structural rules）： $$\begin{align*}\frac{}{x : \tau \vdash x : \tau}\text{(identity)} && \frac{\Gamma \vdash M : \sigma}{\Gamma, x : \tau\vdash M : \sigma}\text{(weakening)} && \frac{\Gamma, x:\tau, y:\sigma, \Delta\vdash M:\rho}{\Gamma, y:\sigma, x:\tau, \Delta\vdash M:\rho}\text{(exchange)}\end{align*}$$ 雖然實作上會用更有效率的規則，但為了解說方便這些便已足夠。由此我們可以推出一些常見的規則，例如使用一次 $\text{(identity)}$ 接著反覆使用 $\text{(weakening)}$ 以及 $\text{(exchange)}$ 兩個規則做有限次的歸納後可得到： $$\frac{}{\Gamma, x : \tau \vdash x : \tau}\text{(variable)}$$

簡單型別論

簡單型別理論除了結構規則外，多了兩個規則說明如何建構與消除函數型別：

$$\begin{align*}\frac{\Gamma,x:\sigma\vdash M:\tau}{\Gamma\vdash\lambda x . M:\sigma \to \tau} \text{($\to$-introduction)}&&\frac{\Gamma\vdash M:\sigma\to\tau\quad\Gamma\vdash N:\sigma}{\Gamma\vdash M\,N:\tau}\text{($\to$-elimination)}\end{align*}$$

其中 $\text{($\to$-introduction)}$ 代表如果能在 $\Gamma, x : \sigma$ 下推得 $M : \tau$ 的話，則我們能在 $\Gamma$ 下推得 $\lambda x . M$ 的型別為 $\sigma \to \tau$ 也就是 $\Gamma \vdash \lambda x . M : \sigma \to \tau$，這條規則也被稱為 abstraction。同樣地，$\text{($\to$-elimination)}$ 代表如果給定 $M : \sigma \to \tau$ 以及另一個 term $N$ 的型別為 $\sigma$ 的話，我們可以推論 $M N$ 的型別為 $\tau$，這條規則常被稱為 application。

舉例來說，我們可以判斷 $\lambda x . x$ 的型別為 $\sigma \to \sigma$，因為我們可以透過 $\text{(identity)}$ 以及 $\text{($\to$-introduction)}$ 得知：
$$\frac{x:\sigma \vdash x:\sigma}{\vdash \lambda x . x : \sigma \to\sigma}$$ 對於 $\lambda x . \lambda y . x$ 則有 $\vdash (\lambda x . \lambda y . x ) : \sigma \to (\tau \to \sigma)$，演繹的過程留給讀者練習。最後要注意的是，並不是所有的 lambda term 都能夠推得型別，像是 $x x$ 就沒辦法，這類的問題在此不考慮。

語法範疇

簡單型別本身也能夠構成範疇，這類的範疇稱為語法範疇（syntactic category）或是 classifying category。首先定義 $\mathbf{STT}$ 範疇：

1. 物件為所有的 context $\Gamma$。仔細來說，假定我們有可數無窮多的 $x_i : \tau_i$，則物件是所有的有限子集合。
2. 給定 context $\Gamma, \Delta$，從 $\Gamma$ 到 $\Delta = (y_1:\sigma_1, \dots, y_m:\sigma_m)$ 的一個態射代表 $\vec{M} = (M_1, \dots, M_i, \dots, M_n)$ 使得 $\Gamma \vdash M_i : \sigma_i$ 都成立。

那麼給定態射 $\vec{M}\colon\Gamma \to \Delta$ 跟 $\vec{L}\colon\Delta \to \Theta$ ，我們可以把 $L_j$ 當中出現變數 $y : \sigma$ 的部分取代成 $M : \sigma$，表示為 $L_j [\vec{y}/\vec{M}]$，如此以來就得到 $\Gamma \vdash L_j [\vec{y}/\vec{M}] : \rho_j$。也就得到一個態射 $$(L_1[\vec{y}/\vec{M}], \dots,L_m[\vec{y}/\vec{M}])\colon\Gamma \to\Delta\to\Theta$$ 定義為態射的合成。

對每一個 context $\Gamma$，從 $\text{(Var)}$ 我們可以得到態射 $(x_1, \dots, x_m)\colon\Gamma \to \Gamma$。我們可以很簡單地驗證此態射為單位態射：因為根據替換的操作我們有 $x_i[\vec{x}/\vec{M}] = M_i$，所以 $\vec{M} \circ \vec{x} = \vec{M}$ 。同樣地，因為 $M_i[\vec{x}/\vec{x}] = M_i$ 我們得到 $\vec{x}\circ \vec{M} = \vec{M}$ 說明 $\vec{x}\colon \Gamma\to\Gamma$ 為單位態射（identity）。

結構規則的範疇性質

接下來我們觀察範疇 $\textbf{STT}$ 上一個特殊的物件——空環境。根據定義 $\Gamma \to \emptyset$ 都有一個長度為零的序列 $\vec{M} = ()$ 使得 $\emptyset$ 內所有的 $y : \sigma$ 都可以被推導出來（！）。而長度為零的序列只有一個，也就是空序列，因此空環境 $\emptyset$在這語法範疇是 terminal object。

我們還可以再證明該範疇具有 binary product。為了簡化說明，我們只考慮環境的長度為 2 的情況，也就是 $\Gamma = x : \tau, y : \sigma$。從結構規則中，我們可以推得 $$\begin{align*} x : \tau, y : \sigma \vdash x : \tau && x : \tau, y : \sigma \vdash y : \sigma\end{align*}$$ 也就是兩個態射 $x\colon (x:\tau, y:\sigma) \to (x : \tau)$ 跟 $y\colon (x:\tau, y:\sigma)\to(y:\sigma)$；如果考慮任意兩個 judgement $\Gamma \vdash M : \tau$ 以及 $\Gamma \vdash N : \sigma$，我們得到一個從 $\Gamma$ 到 $(x : \tau, y : \sigma)$ 的態射 $(M, N)$ 並且我們知道 $x \circ (M, N) = x[x/M] = M$ 以及 $y \circ (M, N) = N$ 也就是滿足以下的交換圖：

$$\xymatrix{(x : \tau) & (x : \tau, y : \sigma) \ar[r]^-{y}\ar[l]_-{x}& (y:\sigma) \\ & \Gamma \ar[u]_{(M, N)} \ar[ru]_{N} \ar[lu]^{M}}$$ 至於 $(M, N)$ 的唯一性，用數學歸納法考慮變數替換的定義，在此略過不談。由此可知，僅用結構規則便能證明該範疇具有所有的有限 product。

在下一篇，我們將證明 $\textbf{STT}$ 為 Cartesian closed 。