用户: Ice1000/神谕模态

考虑 Gödel 编码的那一套理论 (见 Kleene 第一代数) 里面的 ${\phi }_e$,

记 $2$ 为两个元素的集合.

1基本定义

定义 1.1 (可计算). 称 $f:\mathbb{N}\to 2$ 可计算, 若存在 Turing 机能计算它.

定义 1.2 (相对可计算). 称 $f:\mathbb{N}\to 2$ 相对 $\chi :\mathbb{N}\to 2$ 可计算, 若以 $\chi$ 为神谕下 $f$ 可计算. 记作 $f{\le }_T\chi$, 又称 $f$ Turing 可规约到 $\chi$.

命题 1.3. 在 Turing 可规约下, $\mathbb{N}\to 2$ 的函数构成拟序.

2抽象废话

命题 1.3 里面的拟序的 “poset reflection” 可以嵌入有效意象 Eff 的子意象格.

集合范畴 Set 是 Eff 的子意象. 记子意象层化单子为 $\nabla$, 那么它是以下图表中的左伴随:

$$\mathsf{Set}\mathsf{Eff}\nabla \perp$$

可以将 $\nabla$ 看作 “抹除计算信息” 的函子. 例如, $X\to Y$ 为以可计算函数的集合, 而 $\nabla X\to \nabla Y$ 就是对应的不一定可计算的函数的集合.

命题 2.1. 考虑 $f:\nabla X\to \nabla Y$, 考虑包含它的最小的 Eff 的子意象, 这里面的态射就是相对于 $\mathbf{f}$ 可计算的函数.

这里出现了一张我还没看清就跳过的交换图.

3模态

定义 3.1. 神谕模态 $◯:\mathcal{U}\to \mathcal{U}$ 为将函数拓展为可计算函数的最小模态.

类型论层面上, 除了标准的模态公理, 神谕模态还对于任意类型 $X$, 有函数 ${\mu }_X:X\to ◯X$.

定义 3.2. 称类型 $X$ 为:

•	$◯$-模态, 若 ${\mu }_X$ 是等价 (类型论).
•	$◯$-分离, 若 (没看清).
•	$◯$-联通, 若 (也没看清).

后面因为没看清这些就全部不懂了.

总之这个讲座已经开始将高阶归纳类型这个术语扩展到任意模态了. 对于模态 $M:\mathcal{U}\to \mathcal{U}$, 类型 $D$ 的高阶构造子就是返回 $MD$ 或者 $M(MD)$ 等类型的构造子. 我第一次见这个用法是 Astra Kolomatskaia 的半单类型论, 现在似乎像爆豪胜己受欢迎这件事一样已经被大众接受了.