编码–解码法

编码–解码法是同伦类型论中的一种证明给定一点的道路空间和其它类型同构的手法.

本文假设读者对同伦类型论相关的概念有基本的了解, 例如道路空间、相等类型及其归纳公理 J 规则、高阶归纳类型等.

1类型论相关背景

考虑到类型论目前并不属于主流数学, 这里给出一些本文用到的 (同伦) 类型论基本概念:

•	宇宙 (类型论) $\mathcal{U}$: 所有类型的类型.
•	${\mathrm{ap}}_f:\mathrm{Id}(a,b)\to \mathrm{Id}(f(a),f(b))$ 为把一个函数 $f$ 应用到一条道路上的操作, 在 J 规则中有证明.
•	$\mathrm{transport}:\mathrm{Id}(A,B)\to A\to B$ 为类型转换操作, 同样参见 J 规则.
•	无交并类型.
•	圆周 (同伦类型论) $S^1$.
•	空类型 $\varnothing$.

本词条借助较为简单的无交并类型来正式介绍编码–解码法, 然后再引入编码–解码法处理较为复杂的圆类型的例子.

方便起见, $\Pi$ 类型均使用 $(x:A)\to B$ 的语法来代替 ${\prod }_{x:A}B$.

2例子: 无交并

无交并类型是一个有两个构造函数的类型, 这两个构造函数满足如下性质:

•	单射: 由 $\mathrm{Id}(\mathrm{inl}a,\mathrm{inl}b)$ 可以得到 $\mathrm{Id}(a,b)$.
•	不交: 由 $\mathrm{Id}(\mathrm{inl}a,\mathrm{inr}b)$ 可以得到 $\varnothing$.

现在尝试证明它.

无交并的编码

给定 $a:A$, 定义:

$${\mathrm{Code}}_a:={\mathrm{rec}}_{+}(\lambda x.\mathrm{Id}(x,a),\lambda x.\varnothing )$$

读者应该能根据上面的定义推断出 ${\mathrm{Code}}_a:A+B\to \mathcal{U}$. 这就是「编码–解码法」这个名字里的「码」了. 使用模式匹配可以更直观地观察到它的行为:

$$\begin{array}{rl}{\mathrm{Code}}_a(\mathrm{inl}x)& :=\mathrm{Id}(x,a)\\ {\mathrm{Code}}_a(\mathrm{inr}x)& :=\varnothing \end{array}$$

考虑 $u:A+B$ 和 $p:{\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)$, 有:

$${\mathrm{ap}}_{{\mathrm{Code}}_a}(p):{\mathrm{Id}}_{\mathcal{U}}({\mathrm{Id}}_A(a,a),{\mathrm{Code}}_a(u))$$

注意我们得到的是一个类型之间的等值关系, 左边是 $a$ 上的环路空间, 右边是 $u$ 对应的码. 借助 $\mathrm{transport}$ 我们可以得到一个从左到右的函数, 然后再把 ${\mathrm{refl}}_a$ 喂给它:

$$\mathrm{transport}({\mathrm{ap}}_{{\mathrm{Code}}_a}(p),{\mathrm{refl}}_a):{\mathrm{Code}}_a(u)$$

上面的这个构造就是无交并类型的编码操作了. 定义:

$${\mathrm{encode}}_a(u):=\lambda p.\mathrm{transport}({\mathrm{ap}}_{{\mathrm{Code}}_a}(p),{\mathrm{refl}}_a)$$

不难看出:

$${\mathrm{encode}}_a:(u:A+B)\to {\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)\to {\mathrm{Code}}_a(u)$$

分别令 $u=\mathrm{inl}v$ 或者 $u=\mathrm{inr}v$ 就可以分别构造证明前面说的单射和不交两个性质:

•	$u=\mathrm{inl}v$ 的话, 那么 ${\mathrm{Code}}_a(\mathrm{inl}v)={\mathrm{Id}}_A(a,v)$, 所以 ${\mathrm{encode}}_a(u)$ 的类型也就是 ${\mathrm{Id}}_{A+B}(\mathrm{inl}a,\mathrm{inl}v)\to {\mathrm{Id}}_A(a,v)$.
•	$u=\mathrm{inr}v$ 的情况留给读者.

观察编码操作的类型, 它可以看作是一个参数化的函数, 从 ${\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)$ 到 ${\mathrm{Code}}_a(u)$. 这个函数的输入是从定点 $\mathrm{inl}a$ 出发的道路空间, 输出是这个定点周围的「码」. 接下来我们将会定义它的逆, 以证明这个函数是一个同构.

无交并的解码

从编码操作的类型可以很轻易地看出解码操作应有的类型:

$${\mathrm{decode}}_a:(u:A+B)\to {\mathrm{Code}}_a(u)\to {\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)$$

我们借助 ${\mathrm{rec}}_{+}$ 来定义解码操作.

•	如果 $u=\mathrm{inl}v$, 那么参数类型 ${\mathrm{Code}}_a(u)={\mathrm{Code}}_a(\mathrm{inl}v)={\mathrm{Id}}_A(v,a)$, 此时返回类型也随之变为 ${\mathrm{Id}}_{A+B}(\mathrm{inl}a,\mathrm{inl}v)$, 通过 ${\mathrm{ap}}_{\mathrm{inl}}$ 即可简单实现这个转换.
•	如果 $u=\mathrm{inr}v$, 那么 ${\mathrm{Code}}_a(u)={\mathrm{Code}}_a(\mathrm{inr}v)=\varnothing$, 此时返回类型是什么已经不再重要.

因此:

$${\mathrm{decode}}_a(u):={\mathrm{rec}}_{+}({\mathrm{ap}}_{\mathrm{inl}},{\mathrm{rec}}_{\varnothing })$$

编码和解码互逆

接下来我们需要证明编码和解码两个函数互逆. 证明很直接, 其中一个方向是使用 J 公理直接得到结果, 另一个方向是使用模式匹配, 留作习题.

注 2.1. 在立方类型论中, 由于 Swan 问题导致 $\mathrm{transport}$ 计算性质较差, 比起同伦类型论还需要额外多出一些步骤.

3例子: 圆

圆类型类似的性质如下:

•	闭环: 由 $u:\mathbb{Z}$ 可以得到 ${\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})$ (一条圆上的环路) .
•	基本群: 任何 $p:{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})$ 都生成自形如 $p_1\circ p_2\circ \cdots \circ p_m$ 的表达式, 其中 $p_i$ 为 $\mathrm{loop}$ 或者 $\neg \mathrm{loop}$. 用构造主义逻辑的话来讲, 就是存在一个整数 $n$ 使得 $\mathrm{loop}$ 和自己相连 $n$ 次得到的道路等价于 $p$, 其中负数代表反向相连.

我们尝试证明它们. 这个证明用到了泛等公理的性质 ($\beta$ 规则):

$${\mathrm{ua}}_{\beta }:\prod _{e:A\simeq B}\mathrm{Id}(\mathrm{transport}(\mathrm{ua}e),e.1)$$其中 $e.1$ 是指取出 $A\simeq B$ 中对应的函数. 在立方类型论中, 如上性质是类型论中的计算性质.

除此之外, 我们还需要用到整数上由 $+1$ 操作形成的自同构:

$$\begin{array}{rl}& s:\mathbb{Z}\simeq \mathbb{Z}\\ & s.1(x)=x+1\end{array}$$

圆周的编码

由于圆周的构造子不需要参数, 因此定义「码」如下:

$$\mathrm{Code}:={\mathrm{rec}}_{S^1}(\mathbb{Z},s)$$

读者应该能推断出 $\mathrm{Code}:S^1\to \mathcal{U}$. 不难看出:$$\mathrm{Id}(\mathrm{transport}(\mathrm{Code}(\mathrm{loop})),\lambda x.x+1)$$同样的, 在立方类型论中如上性质由计算即可得到.

用类似的思路可以定义编码操作:

$${\mathrm{encode}}_x:=\lambda p.\mathrm{transport}({\mathrm{ap}}_{\mathrm{Code}}(p),0)$$

其中 $0:\mathbb{Z}$ 是整数. 不难看出,

$${\mathrm{encode}}_x:(p:\mathrm{Id}(\mathrm{base},x))\to \mathrm{Code}(x)$$

(未完待续)

4参考文献

•	Daniel R. Licata, Michael Shulman (2013). “Calculating the Fundamental Group of the Circle in Homotopy Type Theory”. arXiv: 1301.3443. (doi) (web)