用户: Trebor/多项式模型

本文介绍 Martin-Löf 类型论多项式模型的直观、动机, 以及其如何构成函数外延性的反模型.

1温习: 集合模型

首先来温习集合如何构成类型论的模型. 直观上, 我们把类型解释成集合, 类型的元素解释成集合的元素. 类型的 Descartes 积解释成集合的乘积, 类型的不交并解释成集合的不交并, 函数类型解释成函数集合, 等等.

但是, 依值类型是可以包含变量的, 因此我们需要定义 “依赖于一个 $x:A$ 的类型 $B$” 如何解释. 如果 $A$ 已经被解释为一个集合 $\alpha$, 就可以把 $B$ 解释为一族集合 ${\beta }_i$, 指标是 $i\in \alpha$.

要正确地把上面的讨论推广到任意变量的情况. 一列变量 $x:A,y:B(x),z:C(x,y),\dots$ 构成一组语境 $\Gamma$. 我们将语境 $\Gamma$ 解释成集合 $\gamma$, 语境 $\Gamma$ 中的类型解释成集合族 $\{{\alpha }_i\}$, $i\in \gamma$. 而类型的元素则是集合族中的元素族, 即 $\{x_i\}$, $i\in \gamma$.

这样, 我们对模型的直观, 总是先经历 “类型是 X” $⟹$ “需要定义 ‘依值 X’ 来对应依值类型” $⟹$ “其实语境才是 X, 而类型是依值 X” 这三步. 下面的介绍也会类比这个过程.

对于 Martin-Löf 类型论这样, 类型的直观很接近集合的情况, 往往有一种办法可以帮助了解某个模型的性质: 通过函子 $\mathrm{hom}(1,-)$ 获得对象的 “底集合”. 例如拓扑空间 $X$ 的底集合就是点集 $\mathrm{hom}(1,X)$. 带群 $G$ 作用的集合的底集合是其不动点集, 等等. 注意群范畴不能这样操作, 因为群范畴与集合范畴的直观并不类似.

2两步博弈

组合博弈论中, 常常直接规定若一方无法行动, 则判负 (困毙). 这样就无需额外规定胜负, 只需规定一方没有行动即可.

考虑一类非常简单的两人完全信息博弈. 我们固定将其中一方叫做 “我”, 另一方叫做 “对面”. 我总是先走.

定义 2.1. 两步博弈包含两个要素: 一个集合 $Q$ 表示我能选择的行动, 一族集合 $R_i$, $i\in Q$ 表示对面能做出的应对.

更复杂的博弈则可以包含多步, 不过我们不需要这些. 后面会解释为何.

例 2.2. 博弈 $0$ 中我没有任何选择, 即死. 博弈 $1$ 中我只有唯一的选择, 而对手没有应对, 即死. 博弈 $x$ 中我只有唯一的选择, 而对手有唯一的应对.

一个博弈 $⅁$ 对应的底集合是我的赢法, 即 $|⅁|=\{i\in Q\mid R_i=\varnothing \}$. 正如 $G$-集合的情况一样, 这丢失了很多信息, 但仍不失为直观认识它的办法.

由这个直观可以看出, 博弈的态射应该将困难 (我难以赢) 的博弈映射到简单的博弈. 具体来说, 博弈的态射是对手策略的某种翻译器.

定义 2.3. 给定两博弈 ${⅁}^{\prime }$, $⅁$, 其态射 ${⅁}^{\prime }\to ⅁$ 包含以下资料:

•	将我的策略从前者对应到后者: $\phi :Q^{\prime }\to Q$,
•	将对手的策略从后者对应到前者: ${\psi }_i:R_{\phi (i)}\to R_i^{\prime }$.

注意两个映射方向相反: 这样如果对手能在 $⅁$ 中打赢我, 利用这个翻译办法, 就能在 ${⅁}^{\prime }$ 中打赢我.

定理 2.4. 全体博弈构成范畴.

$\square$

博弈的组合

我们可以轻松地把两个博弈组合起来形成新的博弈.

定义 2.5. 给定两个博弈 $⅁$, ${⅁}^{\prime }$, 其和 $⅁+{⅁}^{\prime }$ 中我可以选择二者之一并且做出行动, 对手做相应的回应. 换言之, 我的行动是不交并 $Q+Q^{\prime }$; 对手的行动则是两族集合 $R_i$, $R_{i^{\prime }}^{\prime }$ 的不交并. 有显然的态射 $⅁\to ⅁+{⅁}^{\prime }$.

请读者证明 $⅁+{⅁}^{\prime }$ 是范畴中的余积. 博弈 $0$ 则是范畴中的始对象.

定义 2.6. 给定两个博弈 $⅁$, ${⅁}^{\prime }$, 其积 $⅁\times {⅁}^{\prime }$ 中我需要同时进行两场博弈. 对手只要选择一场进行回应即可获胜. 换言之, 我的行动是 $(i,j)\in Q\times Q^{\prime }$; 对手的行动则是 $(i,j)\mapsto R_i+R_j^{\prime }$. 有显然的态射 $⅁\times {⅁}^{\prime }\to ⅁$.

请读者证明 $⅁\times {⅁}^{\prime }$ 是范畴中的积. 博弈 $1$ 则是范畴中的终对象.

例 2.7. $x^n$ 中我只有唯一一种选择, 而对此对手有 $n$ 种回应方法. 特别地, $x^0=1$.

不难看出积和余积都可以推广到无穷元, 无需限制在二元情况.

为了简化叙述, 我们可以允许我连续做出几步选择: 例如可以先选择 $1\le n\le 8$ 的整数, 再选择 $1\le m\le n$ 的整数. 因为这等价于直接令我从 $36$ 种走法种择一. 类似地, 对手也可以连续做选择.

事实上, 我们也可以交错地做选择. 假如我们进行四步博弈, 这实则等价于我先走第一步, 然后声明一个映射, 将对手的第二步映射到我将要走的第三步应对. 然后对手走第二步, 再走第四步. 由于这是完全信息博弈, 这样做不会导致对手获得任何优势. 读者可以试着将这个过程写成公式. 需要注意的是, 上面的不少构造都是针对两步博弈的. 例如 $\mathrm{hom}(1,-)$ 是我的走法中对方无法回应的部分. 对于四步博弈, 必须先翻译成两步博弈才能应用这些描述.

两步博弈范畴是积闭范畴. 要构造指数对象, 直观上需要考虑 $\mathrm{hom}({⅁}^{\prime },⅁)$ 并将其内化为一个博弈. 态射的定义中需要给出 $\phi :Q^{\prime }\to Q$ 的翻译, 在选择了 $i\in Q^{\prime }$ 后, 对手经过翻译选择一个元素 $r\in R_{\phi (i)}$ 作为回应, 我们的态射再将其翻译回 $R_i^{\prime }$. 因此构造 $\mathrm{hom}({⅁}^{\prime },⅁)$ 的元素的过程可以转换为一次博弈:

定义 2.8. 给定两个博弈 $⅁$, ${⅁}^{\prime }$, 其幂 ${⅁}^{{⅁}^{\prime }}$ 中我需要同时进行 $Q^{\prime }$ 场 $⅁$ 博弈. 在对手回应了 $j\in Q^{\prime }$ 对应的博弈后, 我再从 $\{\star \}+R_j^{\prime }$ 中选择一个元素. 如果选择 $r\in R_j^{\prime }$, 则构造成功, 对手即死; 如果选择 $\star$, 则对手有唯一的回应方式, 我即死.

考虑点集 (即我的走法中对手无法回应的部分) $\mathrm{hom}(1,{⅁}^{{⅁}^{\prime }})=\mathrm{hom}({⅁}^{\prime },⅁)$ 只能解释这个构造的一部分. 关于为何需要额外有一步令我即死的选择 $\star$, 我们还可以利用 $\mathrm{hom}(x,-)$ 做更精细的考量. 这个函子取出了我的所有走法, 不只是我的赢法. 而 $\mathrm{hom}(x,{⅁}^{{⅁}^{\prime }})=\mathrm{hom}(x\times {⅁}^{\prime },⅁)$, 由一个映射 $\phi :Q^{\prime }\to Q$ 与 $\psi :R_{\phi (i)}\to 1+R_i^{\prime }$ 构成. 因此幂的定义中也需要包含 $1+R^{\prime }$ 这个构造才能匹配.

还有别的思考方式可以解释此构造, 将在第 5 节考虑.

定理 2.9. 博弈的幂是范畴中的指数对象.

证明.

证明. 我们直接验证泛性质. 假设有第三个博弈 ${⅁}^{\prime \prime }$. $\mathrm{hom}({⅁}^{\prime \prime },{⅁}^{{⅁}^{\prime }})$ 中的元素是两个映射 $(\phi ,\psi )$. $\phi$ 将 $i\in Q^{\prime \prime }$ 翻译到二元组 $\phi (i)=(f,F)$ 表示我方在 ${⅁}^{{⅁}^{\prime }}$ 中的行动, 其中 $f:Q^{\prime }\to Q$,$$F:\prod _{j\in Q^{\prime }}{R}_{f(j)}\to (\{\star \}+R_j^{\prime }).$$反过来, $\psi$ 的输入是对手在 ${⅁}^{{⅁}^{\prime }}$ 中的走法, 即 ${\sum }_{j\in Q^{\prime }}\{k\in R_{f(j)}\mid F(j,k)=\star \}$. 输出是 ${⅁}^{\prime \prime }$ 中的走法 $\psi (k)\in R_i^{\prime \prime }$. 我们可以将整体写成一个巨大的依值类型$$\begin{array}{rl}& \left(f:Q^{\prime \prime }\to Q^{\prime }\to Q\right)\\ & \times \left(F:\prod _{i:Q^{\prime \prime }}\prod _{j:Q^{\prime }}{R}_{f(i,j)}\to 1+R_j^{\prime }\right)\\ & \times \left[\prod _{i:Q^{\prime \prime }}\left(\sum _{j:Q^{\prime }}\sum _{k:R_{f(i,j)}}F(i,j,k)=\star \right)\to R_i^{\prime \prime }\right].\end{array}$$

另一方面, $\mathrm{hom}({⅁}^{\prime \prime }\times {⅁}^{\prime },⅁)$ 中的元素也是两个映射 $(\phi ,\psi )$. $\phi :Q^{\prime \prime }\times Q^{\prime }\to Q$. $\psi$ 则将 $R_{\phi (i,j)}$ 翻译到 $R_i^{\prime \prime }+R_j^{\prime }$. 换句话说是如下的依值类型$$(\phi :Q^{\prime \prime }\times Q^{\prime }\to Q)\times \left(\prod _{i:Q^{\prime \prime }}\prod _{j:Q^{\prime }}{R}_{\phi (i,j)}\to R_i^{\prime \prime }+R_j^{\prime }\right).$$请读者盯着这两个依值类型看, 不久就能看出其显然等价.

$\square$

3依值类型

我们接下来考虑依值类型.

定义 3.1. 给定博弈 $⅁$, 定义关于 $⅁$ 的依值博弈 $\mathbb{G}$ 由如下要素构成. 有一族依赖于 $i\in Q$ 的集合 ${\mathcal{Q}}_i$, 还有一族依赖于 $i\in Q$ 与 $j\in {\mathcal{Q}}_i$ 的集合 ${\mathcal{R}}_{i,j}$.

这也可以说成是 displayed game, 不知如何翻译. 有了依值的事物后最重要的问题就是询问其全空间为何. 对于集合族来说全空间就是其不交并. 对于不依赖 $⅁$ 的退化情况, 我们应该得到乘积 $⅁\times \mathbb{G}$.

定义 3.2. 依值博弈 $\mathbb{G}$ 的全空间 $\int \mathbb{G}$ 是一场博弈, 其中我需要选择 $i\in Q$ 与 $j\in {\mathcal{Q}}_i$. 对手要么给出回应 $R_i$, 要么给出回应 ${\mathcal{R}}_{i,j}$. 有显然的态射 $\int \mathbb{G}\to ⅁$.

在集合的情况下, 集合族 $A\to \mathsf{Set}$ 与一个映射 $B\to A$ 包含的信息是等价的. 但是博弈则不是如此, 例如 $x\to x^2$ 的对角映射 (这由抽象废话可以直接定义, 但请读者写出映射的具体内容) 不能写成 $\int \mathbb{G}\to ⅁$ 的形式. 读者需要想清楚为什么才可继续往下阅读.

正如全空间是乘积的依值情况, 截面就是映射的依值情况.

定义 3.3. 依值博弈 $\mathbb{G}$ 的截面由如下要素定义. 有依值函数 $\phi :(i:Q)\to {\mathcal{Q}}_i$, 与依值函数 $\psi :{\prod }_{i:Q}{\mathcal{R}}_{i,\phi (i)}\to R_i$.

Sigma 类型不难类推定义. 假设有博弈 $⅁$, 关于 $⅁$ 的依值博弈 $\mathbb{G}$, 与关于 $\int \mathbb{G}$ 的依值博弈 ${\mathbb{G}}^{\prime }$, 我们可以定义其 $\Sigma$ 类型 ${\Sigma }_{\mathbb{G}}{\mathbb{G}}^{\prime }$, 是关于 $⅁$ 的依值博弈. 给定 $i\in Q$, 我的走法是 $(i^{\prime },i^{\prime \prime }):{\sum }_{i^{\prime }:{\mathcal{Q}}_i}{\mathcal{Q}}_{i,i^{\prime }}^{\prime }$, 而对方的回应是 ${\mathcal{R}}_{i,j}+{\mathcal{R}}_{(i,i^{\prime }),i^{\prime \prime }}^{\prime }$ 的元素. 这就是把全空间的定义升级了.

Pi 类型略显复杂, 但实则是上面的讨论的简单外推. 直接将定义 2.8 改成依值的情况即可. 自然语言表达显繁琐, 读者可以观察此形式化. 不过需要注意的是, 博弈范畴不是局部积闭的. 之前所提到的 $x\to x^2$ 的映射就无法取前推 (即依值函数).

我们将所闻整理成模型: 这构成具族范畴 (category with family). 底范畴即博弈构成的范畴 $\mathcal{C}$. 给定博弈, 取其对应的全体依值博弈集合, 则构成函子 ${\mathcal{C}}^{\text{op}}\to \text{Set}$, 是具族范畴中类型的解释. 元素的解释就是依值博弈的截面, 语境延伸就是取依值博弈的全空间. Sigma, Pi 类型都满足对应的定义.

上述操作都可以内化到合适的范畴中, 不一定是 $\text{Set}$.

4函数外延

这个模型的重要作用之一是证明函数外延在 Martin-Löf 类型论中不可证. 为此, 我们来看相等类型的语义.

相等类型的语义实际上非常取决于哪些映射形如 $\int \mathbb{G}\to ⅁$. 这些映射称作形式丛. 例如对于积闭范畴而言, 我们可以直接规定类型均不可依值, 则形式丛只有乘积的投影映射. 那么这个模型中就可以取相等类型为恒真类型. 相反地, 如果某范畴局部积闭, 可以取所有映射都是形式丛. 那么这个模型中相等类型就必须是对角线 $X\to X\times X$ 对应的类型, 也就是外延相等.

对于博弈范畴而言, 我们不希望相等类型平凡, 也不能取外延相等 (因为这个范畴并不局部积闭). 因此可以取一个折中的构造.

相等类型的定义中, 需要语境 $⅁$ 以及其中的类型 $\mathbb{G}$. 相等类型依赖于两个 $\mathbb{G}$ 变量. 我们耍些小聪明, 把它说成是依赖一个 $\mathbb{G}\times \mathbb{G}$ 变量. 这个乘号就是博弈乘积对依值情况的推广: 我的走法是 $(s,t)\in {\mathcal{Q}}_i^2$ ($i\in Q$), 对手的应对是 ${\mathcal{R}}_{i,s}+{\mathcal{R}}_{i,t}$.

定义 4.1. 相等类型对应的博弈中, 如果 $s=t$, 则我恰有一种走法, 对手即死. 反之, 我没有走法, 我即死. 关于 $\text{refl}$ 和 $J$ 的构造, 请参考上面的形式化. 此模型中 UIP 也成立.

注意到依值博弈中 $\mathcal{Q}$ 和 $\mathcal{R}$ 都只可依赖 $Q$. 因此尽管类型的元素由两个要素组成 (一个 $Q$, 一个 $R$), 相等类型中我们只能保证 $Q$ 分量相等, 而不能保证 $R$ 分量. 这也是不能取外延相等的实操原因.

正因如此, 函数外延不能成立. 函数逐点相等的解释中抛弃了元素的 $R$ 分量. 我们有两个投影映射 $x^2\to x$, 唯一的区别在 $R$ 分量. 这样代入一切定义后, 会得到两个投影映射逐点相等, 但不相等.

5博弈与多项式

尽管标题是多项式模型, 本文似乎尚未提到多项式. 接下来我们就来揭秘.

引理 5.1. 任何博弈都可以唯一地写成 $x$ 的多项式, 即 $x$ 的 (可以无限次) 幂的余积.

证明. 若 $⅁$ 由 $Q$ 与 $R_i$ 定义, 则 $⅁={\sum }_{i\in Q}{x}^{R_i}$.

$\square$

考虑两个多项式 $P(x)$ 与 $Q(x)$. 可以看成含有一个类型变量 $x$ 的代数数据类型. 这也被编程社区称作容器 (container). 它们之间的态射 —— 注意到 $x$ 的参数性 —— 可以完全刻画出来, 请读者亲自思考一下. 其结果恰好就是博弈之间的映射. 从另一个角度, 也可以用自然性来替代参数性. 将多项式视为 $\text{Set}\to \text{Set}$ 的函子, 则自然变换就恰好和博弈之间的映射有对应. 这可以靠米田引理说明. 多项式模型更细致的讨论可以参考此文.

类型论的预层模型非常有用. 此文中利用预层的构造为商-归纳-归纳类型 (QIIT) 给出了严谨的语义. 不过这只能在 QIIT 存在的情况下给出语义, 不能保证其存在. (例如 $X=\mathcal{P}(\mathcal{P}(X))$ 的不动点不可能存在.) 因此我们可以试图将预层限制到多项式函子. 这是诸如 A container model for type theory 等工作的动机.

(懒得看如何写成参考文献格式, 就都搞成链接了.)