偏等关系语义

偏等关系语义是一种基于偏等关系的构造类型论的模型的手法. 它基于一个语法合法的表达式的集合 $\mathrm{Val}$, 并借助偏等关系在这之上定义什么样的表达式是 “合法” 的, 然后把类型定义为 $\mathrm{Val}$ 的子集. 这种基于集合的语义可以解释一些不常规的类型, 比如对应集合论中交集的类型、子类型、并集类型 (注意不是无交并类型) 等.

语法合法与合法的区分, 用不严谨的数学语言来说, 可以这样类比:

•	$\mathbb{N}(2.33)$ 属于语法合法的表达式, 它括号成对匹配、符号使用规范, 但它类型不合法, 因为 $\mathbb{N}$ 作为自然数的集合不能被当作函数应用.

•	$\frac{\forall }{233(}$ 属于语法不合法的表达式.

这有别于范畴语义的思路, 后者一般直接定义合法的值, 不会有语法合法但类型不合法的值. 当然, 这并不意味着偏等关系语义就必须要存在 “语法合法” 的概念, 直接给所有合法的值取并集得到语法合法的值也是可行的.

偏等关系之所以被用来解释类型论是因为它在讨论相等关系的能力之外还给出了一种定义子集的方式: 考虑集合 $X$ 上的偏等关系$$R\subset X\times X,$$$X$ 中所有满足自反性的元素构成子集:$$\{x\in X\mid R(x,x)\}$$在这个子集上, $R$ 升级为一个等价关系. 同理, 也可以用 $X$ 的子集 $A\subset X$ 来诱导出一个偏等关系, 记作 $R_A$.

而偏等关系的传递性和对称性则可以用来在不确定 $X$ 的子集时论证这个子集里的等价关系. 这对应了某些类型论 (尤其是外延类型论) 中对于在 “不确定两个表达式的类型是否相等” 时讨论这些表达式的相等性的需求, 无类型的情况下论证得出的相等关系在加上类型之后也是有意义的.

1语义构造

偏等关系语义的思路大致如下: 对于每个合法的类型 $A$, 定义 $R_A$ 为 $\mathrm{Val}$ 中由 “合法的 $A$ 的实例构成的子集” 对应的偏等关系, 类似于一个 $\mathrm{Val}$ 上的过滤器.

简单类型论

如果类型的定义和值无关, 那么直接用该思路定义类型即可. 换言之:

$$\underset{R_A(M,M)成立}{\overset{M:A}{=}}$$

依值类型论

在依值类型论中, 类型和实例都在 $\mathrm{Val}$ 里面, 且类型的定义是依赖于值的, 所以需要嵌套的偏等关系:

•	对于类型, 定义对应的偏等关系.

•	对于每个类型, 给它的值定义偏等关系.

形式化定义如下.

定义 1.1. 令 $P(X)$ 表示 $X$ 的幂集, 考虑三元关系:$$\tau \subset \mathrm{Val}\times \mathrm{Val}\times P(\mathrm{Val}\times \mathrm{Val})$$如果它满足如下条件, 那么 $\tau$ 是类型论的偏等关系语义:

•	唯一性: 若 $\tau (A,B,\phi )$ 和 $\tau (A,B,{\phi }^{\prime })$ 同时成立, 则 $\phi ={\phi }^{\prime }$.

•	值偏等关系: 若 $\tau (A,B,\phi )$ 则 $\phi \subset \mathsf{Val}\times \mathsf{Val}$ 是一个偏等关系.

•	类型偏等关系: 固定值偏等关系 $\phi \subset \mathsf{Val}\times \mathsf{Val}$, 那么 $\tau (A,B,\phi )$ 退化为针对 $A,B$ 的二元关系. 该关系是偏等关系.

直觉上, $\tau (A,B,\phi )$ 表示的是 “对于相等的类型 $A$ 和 $B$, 有简单类型论的偏等关系 $\phi$”.

在实际用来解释具体的类型论时, 基本思路是将每个类型定义成一个三元关系上的、关于蕴涵关系单调的函数$$T(\tau )\subset \mathrm{Val}\times \mathrm{Val}\times P(\mathrm{Val}\times \mathrm{Val}),$$然后使用 Knaster-Tarski 不动点定理给出同时拥有所有这些类型的三元关系, 再加上偏等关系语义所需要的性质 (1.1) 就得到了具有所有这些类型的类型论的偏等关系语义.

处理宇宙

为了解释依值类型论中的宇宙, 这里给出一种结合了 Tarski 宇宙和宇宙层级的手法. 首先假设 $\mathrm{Val}$ 中没有宇宙, 只有普通的依值类型.

1.	定义 $V_0\subset \mathrm{Val}$ 为合法的类型构成的子集. 一种可选的定义方式是 $V_0=\{A\in \mathrm{Val}\mid \tau (A,A,\phi )\}$, 当然这不是唯一的定义方式.
2.	针对每个类型 $A\in V_0$, 定义它合法的实例的集合 $\mathrm{El}(A)=\{x\in \mathrm{Val}\mid \tau (A,A,\phi )且\phi (x,x)\}$.
3.	定义新集合 $V_1=V_0\cup \{{\mathcal{U}}_0\}$ 其中 $\mathrm{El}({\mathcal{U}}_0)=V_0$.
4.	以此类推, 定义 $V_2,V_3,\cdots$ 且有包含关系 $V_0\subset V_1\subset V_2\cdots$.

术语翻译

偏等关系 • 英文 partial equivalence relation