2014年2月12日 星期三

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

介紹

範疇論對理論電腦科學影響重大,其中一個應用提供各種型別理論(複數以上 type theories)的模型語意。為了解釋這兩者之間的關係,我們以 simply-typed lambda calculus $\lambda_\to$(或簡稱 simple type theory、STT)為例,討論其範疇上的詮釋。在 STT 中只討論最基本的函數型別(function type)以及變數型別,具體來看是非常簡單的函數式語言,型別系統只負責處理 function application 是否合適。

這題材預計分做兩篇,首先解釋 Cartesian closed category (簡稱 CCC)跟 simply typed lambda calculus 的定義跟基本性質,接著談論如何聯繫 CCC 與 simply typed lambda calculus 兩者。

背景知識

一個範疇 $\mathscr{C}$ 是 Cartesian closed
  1. 所有有限的 product 都存在以及
  2. 對任意的物件 $y, z \in \mathscr{C}$ 都有 exponential object $z^y$。
更明確地說,第一個條件相當於 $\mathscr{C}$ 有 terminal object $1$ 以及對任意物件 $x, y$ 其 binary product $x \times y$ 都存在。第二個條件的 exponential object 定義為一個 object $z^y$ 以及一個「取值」態射 $\epsilon\colon z^y \times y \to z$ 滿足
對任意的物件 $x \in \mathscr{C}$ 以及任意的態射 $g\colon x \times y \to z$ 存在一個唯一的態射 $\lambda g \colon x \to z^y$ 使得 $g = \epsilon \circ (\lambda g \times \mathit{id}_y)$
基本的範例有集合範疇 $\mathbf{Set}$:在此範疇下,只包含一個元素的集合 $\{*\}$ 為 terminal object,對任意集合 $X, Y$ 都可以組成其卡式積 $X \times Y = \{\, (x, y) \mid x \in X, y \in Y\,\}$ 為此範疇的 binary product。而對 exponential object 則為所有從 $Y$ 到 $Z$ 構成的函數集合 $Y \to Z = \{\, f \colon Y \to Z \,\}$ 以及取值函數 $\mathrm{eval}\colon Z^Y \times Y \to Z$ 定義為 $\mathrm{eval}(f, y) = f(y)$。

我們可以再整理一下 exponential object 的定義:任意 exponential object $z^y$ 都存在若對所有的 $y$ 都具有以下對 $x$ 以及 $z$ 自然的一一對應
\begin{align*}
\hom(x, z^y) & \cong \hom(x \times y, z) \\
\lambda g\colon x \to z^y & \mapsto g = \epsilon \circ (\lambda g \times \mathit{id}_y) = \epsilon \circ (\lambda g \times y)
\end{align*}
(an isomorphism natural in $x$ and $z$),也就是說將 $(-)\times y$ 看成一個函子的話,具有一個 right adjoint $(-)^y$。

另外一個例子是給定一個 Boolean algebra $A$,用 $A$ 上的 poset 結構當作一個範疇,也會得到一個 Cartesian closed category,留給讀者分辨對應的 product 跟 exponential object 是什麼。

基本性質

在 $\mathbf{Set}$ 上的 $Z^Y$ 恰好是函數空間,也就是 $\mathbf{Set}(Y, Z)$。一般來說,exponential object $z^y$ 可以看作是將 $\hom(y, z)$ 內化成範疇內的物件,考慮以上 adjunction 的刻畫,因為 $y \cong 1 \times y$,我們可以推出:
\[ \hom(y, z) \cong \hom(1 \times y, z) \cong \hom(1, z^y) \]
對於所有態射 $f\colon y \to z$ 都可以對應到態射 $\lambda f\colon 1 \to z^y$。

這個態射 $\lambda f \colon 1\to z^y$ 代表什麼意思呢?從 $\mathbf{Set}$ 來看,任意 $x\colon 1 \to X$ 的函數,唯一決定 $X$ 上的一點 $x(*) \in X$。我們可以將 $1 \to X$ 當作是 $X$ 上的一個點。還可以從 exponential object 的「取值」態設來驗證這個想法:
引理:在 CCC 中,任意態設 $f\colon x \to y$ 以及任一點 $a\colon 1 \to x$,我們有 \[1 \xrightarrow{\langle \lambda f, a \rangle} y^x \times x \xrightarrow{\epsilon} y = 1 \xrightarrow{a} x \xrightarrow{f}y\] 
證明:給定任意 $f\colon x \to y$,考慮 $f' = f\circ \pi \colon 1 \times x \to x \to y$ 我們有\[\xymatrix{1\times x\ar[d]_{\lambda f' \times x}\ar[rd]^{f'}\\ y^x \times x\ar[r]_{\epsilon} & y}\] 也就是 $f' = \epsilon \circ (\lambda f' \times \mathit{id}_x)$。從此不難推出 $fa = \epsilon \circ \langle \lambda f, a \rangle$。
除此之外,exponential object 跟 products 有著常見的指數運算,例如

  1. $(x^y)^z \cong x^{y \times z}$:從 adjunction 可輕易推得
  2. $x¹\cong x$(同上)
  3. $1^x \cong 1$ 從 $1$ 是 terminal 跟 adjunction 推得
  4. $(x \times y)^z \cong x^z \times y^z$ 因為 $(-)^y$ 是 right adjoint。

 Cartesian closed 函子

我們對於保持 CCC 結構的函子特別有興趣,相當於代數上 homomorphism 保持代數結構操作的觀念:給定兩個 Cartesian closed 範疇 $\mathscr{C}, \mathscr{D}$,我們稱函子 $F\colon\mathscr{C}\to\mathscr{D}$ 為 Cartesian closed 的若 $F$ 保持 finite products 以及 exponential objects。具體來說,這代表
  1. $F(1_\mathscr{C}) \cong 1_\mathscr{D}$
  2. $F(x \times y) \cong Fx \times Fy$ 
  3. $F(z^y) \cong F(z)^{F(y)}$ 
要特別注意的是,這邊的 $\cong$ 不單指同構而是將諸如投影態射 $\pi_x \colon x \times y \to x$ 同樣對應到 $Fx \times Fy \xrightarrow{F\pi} Fx$ 投影態射。

舉例來說,給定兩個 Boolean algebra $A, B$,所有從 $A$ 到 $B$ 的 Boolean algebra homomorphism $f$ 都可以視作 Cartesian closed 函子,因為任意的 Boolean algebra homomorphism 都滿足 $f(\top_A) = \top_B$、$f(a \wedge_A b) = fa \wedge_B fb$ 且 $f(a \to_A b) = fa \to_B fb$。

下一篇將介紹 simply-typed lambda calculus $\lambda_\to$ 並且討論如何將 $\lambda_\to$ 當作 Cartesian closed 範疇。

沒有留言:

張貼留言

留言也可用 \$...\$ 輸入 $\LaTeX$ 語法(注意:預覽畫面無法顯示)