语言背后的代数学（九）：笛卡尔闭范畴

发表于 | 分类于


回顾

上文我们简单的介绍了一些范畴论相关的内容，

范畴由一些对象和箭头组成，范畴之间的箭头称为函子，

函子之间的一族箭头称为自然变换。


范畴的对象不一定是集合，所有的箭头也不一定构成一个集合。

如果一个范畴CC，它的对象都是集合，所有的箭头也构成了一个集合，

就称该范畴是一个小范畴（small categories）。


1. 定义域和值域



在集合论中，函数自变量所有可取值的集合，称为函数的定义域，

给定函数f:A→Bf:A\to B，其中AA就是ff的定义域，记为DfD_f，

集合f(A)={f(x)∣x∈A}f(A)=\{f(x)|x\in A\}，称为ff的值域，记为RfR_f。


在范畴论中，箭头也有定义域和值域的概念。

箭头f:a→bf:a\to b，表示了对象aa和bb之间的关系，

我们称aa为箭头ff的定义域（domain），记为dom fdom~f，

bb为箭头ff的值域（codomain），记为cod fcod~f。


由此，我们还可以定义范畴CC中，从对象aa到对象bb所有箭头的集合，

hom(a,b)={f∣f∈C,dom f=a,cod f=b}hom(a,b)=\{f|f\in C,dom~f=a,cod~f=b\}，常被称为hom-set。


2. 笛卡尔闭范畴



笛卡尔闭范畴是一种带有附加结构的范畴，这个名字虽然不是那么熟悉，

而实际上，我们经常遇到它。


2.1 笛卡尔积

两个集合XX和YY的笛卡尔积，是以下所有可能有序对构成的集合，

X×Y={(x,y)∣x∈X,y∈Y}X\times Y=\{(x,y)|x\in X,y\in Y\}。


2.2 笛卡尔积上的函数

f:X×Y→Zf:X\times Y\to Z，是从笛卡尔积X×YX\times Y到ZZ的函数，

我们可以用两种不同的视角来看待它，

（1）它是一个一元函数，参数取遍X×YX\times Y中的所有元素。

（2）它是一个二元函数，一个参数来自于XX，另一个来自于YY。

原则上，这两种理解应该是不同的，然而它们却是等价的。


2.3 柯里化



笛卡尔闭范畴就是反映这一类性质的数学结构，

一个范畴中，定义在乘积对象a×ba\times b上的箭头ff，

总是可以“自然的”由定义在某一个对象aa或bb上的箭头来决定。


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

将一个二元函数柯里化指的是，将它看成一个一元函数，

这个函数返回另一个一元函数。


假设f:X×Y→Zf:X\times Y\to Z是一个函数，

令ZY={f∣f(y)∈Z,y∈Y}Z^Y=\{f|f(y)\in Z,y\in Y\}是所有YY到ZZ的函数，

则存在唯一的g=X→ZYg=X\to Z^Y，使得g(x)(y)=f(x,y)g(x)(y)=f(x,y)，∀x∈X,y∈Y\forall x\in X,y\in Y。

函数gg称为ff的柯里化。


用hom-set的术语来表述就是，存在一个一一映射，使得，

hom(X×Y,Z)≅hom(X,ZY)hom(X\times Y,Z)\cong hom(X,Z^Y)


2.4 Cartesian Closed

将以上柯里化的概念推广到范畴论中，我们就有，

一个笛卡尔闭范畴（cartesian closed category）CC，是满足以下几个额外条件的范畴。


（1）CC中存在一个对象11，使得对于任意对象A∈CA\in C，有唯一的箭头A→1A\to 1，

这样的对象11，称为终对象（terminal object）。


（2）对于任意两个对象XX和YY，范畴CC中存在一个对象X×YX\times Y，

以及两个箭头p1p_1和p2p_2，使得，p1:X×Y→Xp_1:X\times Y\to X，p2:X×Y→Yp_2:X\times Y\to Y。


（3）对于任意两个对象YY和ZZ，

范畴CC中存在一个对象ZYZ^Y，以及一个箭头e:ZY×Y→Ze:Z^Y\times Y\to Z，使得，

对于任意的箭头f:X×Y→Zf:X\times Y\to Z，存在唯一的箭头g:X→ZYg:X\to Z^Y，

有f=e∘(g×I)f=e\circ (g\times I)恒成立。


即，(e∘(g×I))(X×Y)=e((g×I)(X×Y))=e(ZY×Y)=Z(e\circ (g\times I))(X\times Y)=e((g\times I)(X\times Y))=e(Z^Y\times Y)=Z。

其中I:Y→YI:Y\to Y，为对象YY的恒等箭头，ZYZ^Y称为指数对象（exponential object）。



3. 项的解释

在第六篇中，为了解释简单类型化λ\lambda演算，

我们为每一个λ\lambda项，找到了一个Σ\Sigma代数中数学对象与之对应，

简要的说，我们用Σ\Sigma代数的载体AσA^\sigma来解释基本类型σ\sigma，

用载体上的函数集Aσ→τA^{\sigma\to\tau}来解释类型为σ→τ\sigma\to\tau的所有函数。


现在有了笛卡尔闭范畴，我们准备为每一个基本类型选择范畴中的一个对象，

而将项常量bb解释为范畴中的一个箭头unit→A[[b]]unit\to\mathscr{A}[\![b]\!]（原因在下文解释），

其中A[[⋅]]\mathscr{A}[\![\cdot]\!]为我们在Henkin模型中定义的含义函数。


3.1 封闭项的解释

我们这样定义一个含义函数C[[⋅]]\mathscr{C}[\![\cdot]\!]，

（1）C[[unit]]=unit\mathscr{C}[\![unit]\!]=unit

（2）C[[b]]=unit→A[[b]]\mathscr{C}[\![b]\!]=unit\to\mathscr{A}[\![b]\!]

（3）C[[σ×τ]]=C[[σ]]×C[[τ]]\mathscr{C}[\![\sigma\times\tau]\!]=\mathscr{C}[\![\sigma]\!]\times\mathscr{C}[\![\tau]\!]

（4）C[[σ→τ]]=C[[σ]]→C[[τ]]\mathscr{C}[\![\sigma\to\tau]\!]=\mathscr{C}[\![\sigma]\!]\to\mathscr{C}[\![\tau]\!]


3.2 带有自由变量的项

如果Γ⊢M:σ\Gamma\vdash M:\sigma是一个含有自由变量的λ\lambda项，

则在笛卡尔闭范畴中，它应该解释为从自由变量的语义对象到σ\sigma的语义对象的一个箭头，

C[[Γ⊢M:σ]]=C[[Γ]]→C[[σ]]\mathscr{C}[\![\Gamma\vdash M:\sigma]\!]=\mathscr{C}[\![\Gamma]\!]\to\mathscr{C}[\![\sigma]\!]。


值得一提的是，

这里说明了，项常量bb为什么不能被解释为范畴中的对象，

而是解释成了箭头unit→A[[b]]unit\to\mathscr{A}[\![b]\!]。


其中，类型上下文Γ\Gamma的解释，定义如下，

（1）C[[∅]]=unit\mathscr{C}[\![\varnothing]\!]=unit

（2）C[[Γ,x:σ]]=C[[Γ]]×C[[σ]]\mathscr{C}[\![\Gamma,x:\sigma]\!]=\mathscr{C}[\![\Gamma]\!]\times\mathscr{C}[\![\sigma]\!]


回顾

本文介绍了笛卡尔闭范畴，是一种具有特殊结构的范畴，

它补充了柯里化这一概念所需满足的约束条件。


接着我们用笛卡尔闭范畴解释了，

带有单位类型，乘积类型的简单类型化λ\lambda演算λunit,×,→\lambda^{unit,\times,\to}。


参考

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

语言背后的代数学（六）：Henkin模型

Small and Large Categories

Class

Category Theory for Computing Science

Cartesian closed category