語言背後的代數學（九）：笛卡爾閉範疇

回顧

上文我們簡單的介紹了一些範疇論相關的內容，

範疇由一些對象和箭頭組成，範疇之間的箭頭稱為函子，

函子之間的一族箭頭稱為自然變換。

範疇的對象不一定是集合，所有的箭頭也不一定構成一個集合。

如果一個範疇 ，它的對象都是集合，所有的箭頭也構成了一個集合，

就稱該範疇是一個小範疇（small categories）。

1. 定義域和值域

在集合論中，函數自變數所有可取值的集合，稱為函數的定義域，

給定函數 ，其中 就是 的定義域，記為 ，

集合 ，稱為 的值域，記為 。

在範疇論中，箭頭也有定義域和值域的概念。

箭頭 ，表示了對象 和 之間的關係，

我們稱 為箭頭 的定義域（domain），記為 ，

為箭頭 的值域（codomain），記為 。

由此，我們還可以定義範疇 中，從對象 到對象 所有箭頭的集合，

，常被稱為hom-set。

2. 笛卡爾閉範疇

笛卡爾閉範疇是一種帶有附加結構的範疇，這個名字雖然不是那麼熟悉，

而實際上，我們經常遇到它。

2.1 笛卡爾積

兩個集合 和 的笛卡爾積，是以下所有可能有序對構成的集合，

。

2.2 笛卡爾積上的函數

，是從笛卡爾積 到 的函數，

我們可以用兩種不同的視角來看待它，

（1）它是一個一元函數，參數取遍 中的所有元素。

（2）它是一個二元函數，一個參數來自於 ，另一個來自於 。

原則上，這兩種理解應該是不同的，然而它們卻是等價的。

2.3 柯里化

笛卡爾閉範疇就是反映這一類性質的數學結構，

一個範疇中，定義在乘積對象 上的箭頭 ，

總是可以「自然的」由定義在某一個對象 或 上的箭頭來決定。

這就是柯里化（curring）的概念，

將一個二元函數柯里化指的是，將它看成一個一元函數，這個函數返回另一個一元函數。

假設 是一個函數，

令 是所有 到 的函數，

則存在唯一的 ，使得 ， 。

函數 稱為 的柯里化。

用hom-set的術語來表述就是，存在一個一一映射，使得，

2.4 Cartesian Closed

將以上柯里化的概念推廣到範疇論中，我們就有，

一個笛卡爾閉範疇（cartesian closed category） ，是滿足以下幾個額外條件的範疇。

（1） 中存在一個對象 ，使得對於任意對象 ，有唯一的箭頭 ，

這樣的對象 ，稱為終對象（terminal object）。

（2）對於任意兩個對象 和 ，範疇 中存在一個對象 ，

以及兩個箭頭 和 ，使得， ， 。

（3）對於任意兩個對象 和 ，

範疇 中存在一個對象 ，以及一個箭頭 ，使得，

對於任意的箭頭 ，存在唯一的箭頭 ，

有 恆成立。

即， 。

其中 ，為對象 的恆等箭頭， 稱為指數對象（exponential object）。

3. 項的解釋

在第六篇中，為了解釋簡單類型化 演算，

我們為每一個 項，找到了一個 代數中數學對象與之對應，

簡要的說，我們用 代數的載體 來解釋基本類型 ，

用載體上的函數集 來解釋類型為 的所有函數。

現在有了笛卡爾閉範疇，我們準備為每一個基本類型選擇範疇中的一個對象，

而將項常量 解釋為範疇中的一個箭頭 （原因在下文解釋），

其中 為我們在Henkin模型中定義的含義函數。

3.1 封閉項的解釋

我們這樣定義一個含義函數 ，

（1）

（2）

（3）

（4）

3.2 帶有自由變數的項

如果 是一個含有自由變數的 項，

則在笛卡爾閉範疇中，它應該解釋為從自由變數的語義對象到 的語義對象的一個箭頭，

。

值得一提的是，這裡說明了，項常量 為什麼不能被解釋為範疇中的對象，

而是解釋成了箭頭 。

其中，類型上下文 的解釋，定義如下，

（1）

（2）

回顧

本文介紹了笛卡爾閉範疇，是一種具有特殊結構的範疇，

它補充了柯里化這一概念所需滿足的約束條件。

接著我們用笛卡爾閉範疇解釋了，

帶有單位類型，乘積類型的簡單類型化 演算 。

---

參考

你好，類型（六）：Simply typed lambda calculus

語言背後的代數學（六）：Henkin模型

Small and Large Categories

Class

Category Theory for Computing Science

Cartesian closed category

---

下一篇：語言背後的代數學（十）：Curry-Howard-Lambek correspondance

推薦閱讀：