编码–解码法

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

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

1类型论相关背景

我们使用如下辅助定义:

•	${\mathrm{ap}}_f:\mathrm{Id}(a,b)\to \mathrm{Id}(f(a),f(b))$ 为把一个函数 $f$ 应用到一条道路上的操作, 在 J 规则中有证明.

•	$\mathrm{传送}:\mathrm{Id}(A,B)\to A\to B$, 也是通过 J 规则证明.

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

2例子: 无交并

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

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

现在尝试证明它.

无交并的编码

给定 $a:A$, 定义:

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

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

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

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

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

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

$$\mathrm{传送}({\mathrm{ap}}_{{码}_a}(p),{\mathrm{refl}}_a):{码}_a(u)$$

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

$${\mathrm{编码}}_a(u):=\lambda p.\mathrm{传送}({\mathrm{ap}}_{{码}_a}(p),{\mathrm{refl}}_a)$$

不难看出:

$${\mathrm{编码}}_a:\prod _{u:A+B}{\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)\to {码}_a(u)$$

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

•	$u=\mathrm{inl}v$ 的话, 那么 ${码}_a(\mathrm{inl}v)={\mathrm{Id}}_A(a,v)$, 所以 ${\mathrm{编码}}_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)$ 到 ${码}_a(u)$. 这个函数的输入是从定点 $\mathrm{inl}a$ 出发的道路空间, 输出是这个定点周围的「码」. 接下来我们将会定义它的逆, 以证明这个函数是一个同构.

无交并的解码

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

$${\mathrm{解码}}_a:\prod _{u:A+B}{码}_a(u)\to {\mathrm{Id}}_{A+B}(\mathrm{inl}a,u)$$

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

•	如果 $u=\mathrm{inl}v$, 那么参数类型 ${码}_a(u)={码}_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$, 那么 ${码}_a(u)={码}_a(\mathrm{inr}v)=\varnothing$, 此时返回类型是什么已经不再重要.

因此:

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

编码和解码互逆

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

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

3例子: 圆

圆类型类似的性质如下:

命题 3.1. 任何 $p:{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})$ 都生成自形如 $p_1\cdot p_2\cdot \cdots \cdot 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{传送}(\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{rec}}_{S^1}(\mathbb{Z},s)$$

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

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

$${\mathrm{编码}}_x:=\lambda p.\mathrm{传送}({\mathrm{ap}}_{码}(p),0)$$

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

$${\mathrm{编码}}_x:\mathrm{Id}(\mathrm{base},x)\to 码(x)$$

圆周的解码

从编码操作的类型可以看出解码操作应该有如下类型:

$${\mathrm{解码}}_x:码(x)\to \mathrm{Id}(\mathrm{base},x)$$

解码操作需要处理如下两种情况 (第二个情况的类型过于复杂, 第一次阅读推荐跳过):

$$\begin{array}{rl}& {\mathrm{解码}}_{\mathrm{base}}:\mathbb{Z}\to {\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})\\ & {\mathrm{ap}}_{\mathrm{解码}}(\mathrm{loop}):{\mathrm{Id}}_{\mathbb{Z}\to {\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})}({\mathrm{解码}}_{\mathrm{base}},\mathrm{传送}({\mathrm{ap}}_{\lambda x.码(x)\to \mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}}))\end{array}$$

对于第一个情况, 对于输入的整数 $n$, 我们需要返回「转了 $n$ 圈」的环路, 因此可以感性地定义如下:

$$\begin{array}{rl}& {\mathrm{解码}}_{\mathrm{base}}(0)={\mathrm{refl}}_{\mathrm{base}}\\ & {\mathrm{解码}}_{\mathrm{base}}(正n)=\underset{n次}{\underbrace{\mathrm{loop}\cdot \mathrm{loop}\cdot \cdots \cdot \mathrm{loop}}}\\ & {\mathrm{解码}}_{\mathrm{base}}(负n)=\neg (\underset{n次}{\underbrace{\mathrm{loop}\cdot \mathrm{loop}\cdot \cdots \cdot \mathrm{loop}}})\end{array}$$

负数的情况也可以使用如下等价的定义:

$${\mathrm{解码}}_{\mathrm{base}}(负n)=\underset{n次}{\underbrace{(\neg \mathrm{loop})\cdot (\neg \mathrm{loop})\cdot \cdots \cdot (\neg \mathrm{loop})}}$$

接下来还需要证明这个操作被「绕着 $\mathrm{loop}$ 转一圈」保持. 注意到 $\mathrm{传送}({\mathrm{ap}}_{\lambda x.码(x)\to \mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}})$ 的类型为:

$$码(\mathrm{base})\to \mathrm{Id}(\mathrm{base},\mathrm{base})$$

按照定义这等于

$$\mathbb{Z}\to {\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})$$

一番整理后我们可以得到如下等价的命题:

$$\prod _{n:\mathbb{Z}}{\mathrm{Id}}_{{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})}({\mathrm{解码}}_{\mathrm{base}}(n),\mathrm{传送}({\mathrm{ap}}_{\lambda x.码(x)\to \mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}})(n))$$

证明思路大致如下:

$$\begin{array}{rlrl}& \mathrm{传送}({\mathrm{ap}}_{\lambda x.码(x)\to \mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}})(n)& & 根据\mathrm{传送}对函数类型的性质\\ =& \mathrm{传送}({\mathrm{ap}}_{\lambda x.\mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}}(\mathrm{传送}({\mathrm{ap}}_{码}(\neg \mathrm{loop}),n)))& & 展开第二个\mathrm{传送}\\ =& \mathrm{传送}({\mathrm{ap}}_{\lambda x.\mathrm{Id}(\mathrm{base},x)}(\mathrm{loop}),{\mathrm{解码}}_{\mathrm{base}}(n-1))& & 展开第一个\mathrm{传送}\\ =& \mathrm{loop}\cdot {\mathrm{解码}}_{\mathrm{base}}(n-1)& & 展开解码\\ =& \mathrm{loop}\cdot {\mathrm{解码}}_{\mathrm{base}}(n)\cdot \neg \mathrm{loop}& & 整理\\ =& {\mathrm{解码}}_{\mathrm{base}}(n)& & \end{array}$$

编解码互逆

思路类似, 但涉及大量技术细节, 因此略过, 但编解码的互逆会给出如下等价:

$$\prod _{x:S^1}\mathrm{Id}(\mathrm{Id}(\mathrm{base},x),码(x))$$

令 $x:=\mathrm{base}$ 可以得到

$$\mathrm{Id}(\mathrm{Id}(\mathrm{base},\mathrm{base}),\mathbb{Z})$$

换言之, $S^1$ 的环路空间等价于整数.

4参考文献

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