类型论–范畴论–逻辑学类比

类型论–范畴论–逻辑学类比指三种理论间构造的对应关系.

类型论与范畴论的对应是通过将类型视为范畴中的对象来实现的, 称为类型论的范畴语义. 简单类型 $\lambda$ 演算对应于积闭范畴, 依值类型论对应于概括范畴, 同伦类型论则对应某种 $\infty$-范畴.

本文中的逻辑学指命题逻辑和谓词逻辑. 类型论和逻辑学的对应大致是将类型视为命题的 “所有证明构成的空间”. 这一对应关系也称为 Curry–Howard 对应, 而加上范畴论的版本又叫 Curry–Howard–Lambek 对应 (见 简单类型与积闭范畴).

1例子

下表列出了三种理论的对应关系, 由于拓扑空间范畴 (确切地说是紧生成空间范畴) 是积闭范畴, 且有高阶结构, 下面以拓扑空间范畴为范畴论的例子.

	类型论	范畴论	拓扑学	逻辑学
简单类型论	类型	对象	拓扑空间	命题
	单位类型	终对象	单点空间	真
	空类型	始对象	空空间	假
	实例	从终对象出发的态射	点	证明
	函数类型	幂对象	映射空间	蕴含
	积类型	积	积空间	与
	无交并	余积	无交并空间	或
依值类型论	$\Sigma$ 类型	纤维化	纤维化	存在
	$\Pi$ 类型	截面范畴	截面空间	全称
同伦类型论	相等类型	$2$-态射的空间	环路空间
	截断类型	截断	截断

除此之外, 线性逻辑和通信类型之间也有类似的联系, 半公理化逻辑和异步通信类型之间也是一样.

简单类型与积闭范畴

简单类型 $\lambda$ 演算 ${\lambda }_{\to }$ 和积闭范畴的公理有对应关系, 这也是范畴语义最简单的例子. 仿照代数理论的定义, 定义一个 $\lambda$-理论为三元组 $(\text{Ty},\text{Tm},\text{Eq})$. 其中 $\text{Ty}$ 表示类型符号的集合, 由这些类型符号, 在函数类型, 乘积类型等操作下生成全体类型的集合 $\text{Ty}$. 对于每个类型 $A\in \text{Ty}$, $\text{Tm}(A)$ 表示此类型下添加的元素. 最后 $\text{Eq}$ 是元素对的集合, 表示元素之间要满足的等式.

例 1.1. 群理论可以写成 $\lambda$-理论. 令 $\text{Ty}=\{G\}$, 其中 $G$ 是一个符号.$$\begin{array}{rl}\mathsf{Tm}(G)& =\{e\}\\ \mathsf{Tm}(G\to G)& =\{i\}\\ \mathsf{Tm}(G\to G\to G)& =\{m\}\end{array}$$这里 $e,i,m$ 都是符号, 分别代表单位元, 逆, 乘法. 需要满足的等式有$$\begin{array}{rl}\lambda x.mex& =\lambda x.x\\ \lambda x.m(ix)x& =\lambda x.e\\ \lambda xyz.m(mxy)z& =\lambda xyz.mx(myz)\\ & \dots \end{array}$$其余等式不再写出.

对于两个 $\lambda$-理论, 如果有某个对应关系将类型映射到类型 ${\phi }_{\mathsf{Ty}}:{\mathsf{Ty}}_1\to {\mathrm{Ty}}_2$, 将元素映射到元素 ${\phi }_{\mathsf{Tm}}:{\mathsf{Tm}}_1(A)\to {\mathrm{Tm}}_2(\cdot )$, 使得等式都对应成立, 就称 $\phi$ 是两个 $\lambda$-理论之间的态射. 这样 $\lambda$-理论构成一个范畴 $\text{Theory}$. 所有的积闭范畴与积闭函子也构成一个范畴 $\text{CCC}$. 我们有伴随$$\text{Theory}\perp \text{CCC}\text{Syn}\text{Lang}$$其中 $\text{Syn}$ 构造句法范畴, 而 $\text{Lang}$ 构造内语言. 在简单类型论的情况下此伴随恰好是伴随等价, 但是在一般的情况中可能只有伴随.