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

型別理論

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

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 兩者。

稠密範疇（一）

一般拓樸學內說稠密子集合，指的是一個空間 $X$ 內的子集 $D$，凡是 $X$ 內的元素要嘛在 $D$ 裡頭，要嘛是由 $D$ 的 limit point。而給定兩個連續函數 $f, g\colon X \to Y$ 從 $X$ 到一個 Hausdorff 空間 $Y$，若 $f$ 跟 $g$ 在任一個稠密集合相等，則 $f$ 與 $g$ 必定也在 $X$ 相等。類似的概念延伸到範疇上，我們可以定義稠密函子，使得子範疇的 inclusion functor 成為其特例。

首先記得所謂的 comma category：給定兩個函子 $K, S\colon \mathscr{A} \to \mathscr{C}$ ，定義一範疇的物件為所有從 $Ka$ 到 $Sa'$ 的態設，而物件間的態設為一對 $\mathscr{A}$ 上的態設 $f\colon a \to b, g\colon a' \to b'$ 滿足以下的交換圖
\[
\xymatrix{
  Ka \ar[d]_{Kf} \ar[r] & Sa' \ar[d]^{Sg} \\
  Kb \ar[r] & Sb'
}
\]
而且自然地，我們有兩個 forgetful functor
其中若 $S$ 為常數函子，以上的交換圖則退化成以下的三角交換圖：
\[
\xymatrix{
Ka \ar[d]_{Kf} \ar[r] & c \\
Kb \ar[ru]
}
\]
其中 $f\colon a \to b$。而且自然有一個 forgetful 函子 $P^c$ 將 $Ka \to c$ 對應到 $a$。回到稠密的定義如下：

範疇論的學習進程

對於理論電腦科學的研究生來說，範疇論書籍的選擇跟數學系的稍微不同，以下是給自己的建議：

入門書的部分

• Mac Lane 的 Categories for Working Mathematician 對數學背景的學生是非常好的起點，尤其是修過研究所代數，大概對於 colimits, limits, universal property 以及 adjunction 已經有粗略的概念。對數理邏輯沒興趣的，跳過 topos 跟 foundation 跟 metacategory。跳過七八兩章，直到 Kan extension 之前大概都需要熟悉。第八章如果需要要學 homology 或是學過再回來看就好。跳過的部分之後再補都好。
• Goldblatt 的 Topoi: The Categorial Analysis of Logic 其實是基礎的範疇論介紹，加上 topos 理論的基礎。細節寫得很詳細，非數學基礎的人應該也能看得懂。topos 跟邏輯間的關係寫得不錯，而且本書是作者的畢業論文，網路上就能下載。
• B. Lawvere 寫的 Conceptual Mathematics: A First Introduction to Categories 據說不錯，但我沒仔細看過。

範疇論有了基礎概念 (CWM) 後，接下來才是挑戰的開始，有幾本書可以參考：

用 MathJax 顯示數學符號－以 Blogger 為例

前言

MathJax 是近年來網頁技術中，用來顯示數學符號最熱門的方法之一。以往的解決方法如 MathML 需要瀏覽器的支援，可能因為數學排版複雜又不熱門，主流瀏覽器中只有 Firefox 支援的最完整，其它如  Chrome、Safari 或是 IE 排版結果遠遜於 $\TeX$ 或是 $\LaTeX$ 的品質；另一種方式則是直接顯示成圖片，缺點是與內文難以相配，能夠顯示但不夠優美。而如今 MathJax 的優點，在於只需要支援 JavaScript 的瀏覽器幾乎都可以正確而且漂亮地顯示（詳情見 MathJax 網頁），支援 $\LaTeX$ 的語法，幾乎就像是直接使用 $\LaTeX$ 一樣。

但因為 MathJax 是一支 JavaScript 程式，必須在網頁讀取完成後再解讀。使用上不如 MathML 只要輸入 MathML 的語法就能顯示，需要在網頁中「安裝」MathJax，並不能直接使用。目前網站支援 MathJax 大多為數學相關的網站，像是討論研究所等級的數學問題的 MathOverflow 或是維基百科 Wikipedia （需個人賬號登入設定）。而各主流網誌平台中，多數仍需要稍微修改範本（template）的原始檔才能使用，有些平台如 Wordpress.com 雖然提供各種不同範本的，但不能修改原始檔就沒辦法了。

幸好，Google 旗下的 Blogger 提供了範本的原始檔修改，幾個簡單的步驟就能讓 Blogger 使用 MathJax。其他的平台也類似如法炮製即可：

函子範疇與 Yoneda Lemma（二）

前面一口氣介紹了函子，自然轉換，函子範疇跟 Yoneda 引理。接下來，我們要談談有關 Yoneda 引理代表了什麼意義。

物件其實就像是集合，只不過⋯⋯

首先，從 Yoneda 引理我們可以推得，考慮的函子 $latex K : C^{\mathrm{op}} \rightarrow \mathbf{Set}$ 換成 $latex hom(-, d)$ 得到：
\[
\hom(c, d)\cong[C^{\mathrm{op}}, \mathbf{Set}](hom(-, c), hom(-, d))
\]其中用 $latex [C^\mathrm{op}, \mathbf{Set}]$ 代表從 $latex C^\mathrm{op}$ 到 $latex \mathbf{Set}$ 的函子範疇，而 $latex [C^\mathrm{op}, \mathbf{Set}](hom(-, c), hom(-, d))$  代表這個函子範疇所有從 $latex hom(-, c)$ 到 $latex hom(-, d)$ 的自然轉換。

函子範疇與 Yoneda Lemma（一）

談完範疇的基礎後，可以理解到數學基礎亂七八糟放心地討論範疇論實用的部分：函子（functor）、自然轉換（natural transformation），函子範疇（functor category）以及 Yoneda 引理。

Grothendieck universe - 談範疇的定義跟大小分類

歷史回顧

首先回顧發展公設集合論的動機，羅素悖論（Russell's Paradox）：

令 $V = \{ S : S \not\in S \}$ 為所有不屬於自己的集合，試考慮 $V$ 是否屬於 $V$ 自己？

一般口語的說法是，假若 $V \in V$，則根據 $ V$ 的構造性質，$V \not\in V$；若 $V \not\in V$，則同理得到 $V \in V$，而不論哪一種，都會得到與前提違悖的結果。我們正式地說，考慮 Naive Set Theory，也就是一個帶有 $\in$ 關係以及底下公設模式（Axiom Schema）：對任意用 $x$ 符號為 free variable 的邏輯述句 $P(x)$ 都有
\[\exists y . \forall x . (x \in y \iff P(x))\]

的一階邏輯理論(first-order theory)。 那麼我們考慮 $P(x) = x \not\in x$，以上公設配合一階邏輯會推出\[y \in y \iff y \not\in y\]說明 Naive Set Theory 本身不一致，甚至根據爆炸原理（Principle of Explosion）從而可以證明任何描述，也就是即便 $1\neq 1$這樣的描述都可以成真。很顯然地，這樣的集合論我們沒辦法接受，促使了羅素（B. Russell）發展了型別理論（Type Theory）以及 Zermelo 跟 Fraenkel 發展目前標準的公設集合論——Zermelo–Fraenkel set theory （ZF）。