有效意象

有效意象或可计算意象是一个初等意象. 它刻画了 (包括高阶函数的) 可计算性的概念.

1定义

以防混淆, 提前说明本文均假定排中律成立. 直觉主义中的可计算性非常复杂.

具现

在逻辑中 (不一定是直觉主义), 常常可以把证明看作是某种可计算函数. 如 $\psi \to \chi$ 的证明可以看出一个函数, 输入一个 $\psi$ 的证明, 输出一个 $\chi$ 的证明. 具现就是将这种可计算性解释形式化的一种方法. 这里只列举 Kleene 具现的规则.

取定递归的双射 $⟨-,-⟩:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$ 作为配对函数, 使得它对应的投影 ${\pi }_1,{\pi }_2$ 也是递归函数. 再取 ${\iota }_1,{\iota }_2:\mathbb{N}\to \mathbb{N}$, 使得二者都是单射, 值域构成自然数集合的划分, 并且其逆 $\mathbb{N}\to \{\mathsf{left},\mathsf{right}\}\times \mathbb{N}$ 也是可计算的. 最后取定所有 (部分) 递归函数的 Gödel 编码, 则有一个部分递归函数 $\mathrm{eval}:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$, 使得 $\mathrm{eval}(e,n)$ 是 $e$ 编码的部分递归函数在 $n$ 处的值. 无歧义时, 我们直接写作 $e(n)$.

定义 1.1. 我们递归定义 “自然数 $n$ 具现了命题 $\phi$” 这个关系:

•	如果 $\phi$ 是真的原子命题, 则 $0$ 具现了 $\phi$.
•	$⟨m,n⟩$ 具现了 $\psi \wedge \chi$, 当且仅当 $m$ 具现了 $\psi$ 且 $n$ 具现了 $\chi$.
•	${\iota }_1(m)$ 具现了 $\psi \vee \chi$, 当且仅当 $m$ 具现了 $\psi$. 对 ${\iota }_2$ 同理.
•	$e$ 具现了 $\psi \to \chi$, 当且仅当对于任何具现了 $\psi$ 的 $n$, $e(n)$ 都具现了 $\chi$.
•	$⟨m,n⟩$ 具现了 $\exists x.\psi (x)$, 当且仅当 $n$ 具现了 $\psi (\lceil m\rceil )$. 其中 $\lceil m\rceil$ 表示 $m$ 在形式语言中对应的表达式, 即$$\underset{m\text{个}}{\underbrace{\mathtt{SS}\dots \mathtt{S}}}0.$$
•	$e$ 具现了 $\forall x.\psi (x)$, 当且仅当对于所有的 $n$, $e(n)$ 都具现了 $\psi (\lceil n\rceil )$.

其中原子命题以及其真值, 在不同的理论中各有规定. 在这里, 原子命题是 $M=N$, 其中 $M,N$ 是由一些全递归函数构成的表达式. $\perp$ 是某个固定的原子假命题, 如 $0=1$. $\neg \psi$ 是 $\psi \to \perp$ 的缩写.

定理 1.2. 如果某个句子在 Heyting 算数系统中可证, 那么这个句子可具现.

但是请读者注意下面这个例子:

例 1.3. 令 $\psi$ 是一个句子. 那么 $\psi \vee \neg \psi$ 总是可具现.

这是因为如果 $\psi$ 被某个 $n$ 具现, 那么 ${\iota }_1(n)$ 就具现了 $\psi \vee \neg \psi$. 不然的话, 任何自然数 $e$ 都具现了 $\neg \psi$, 因为按照定义, 对于任何具现 $\psi$ 的自然数 $n$, $e(n)$ 都具现了 $0=1$. 由于不存在这样的自然数, 这是空真的.

有效范畴

仅仅有自然数上的可计算性, 在研究其他对象时就需要反复提到到自然数的编码细节. 而有效范畴则打包了这些信息, 使得可以更自由地使用可计算性的概念.

Kleene 具现相当于给每个句子赋了一个 $\mathbb{N}$ 的子集作为其 “广义真值”. 因此我们说这是给每个句子赋予了 $2^{\mathbb{N}}$-真值. 同理, 我们可以定义一个 $2^{\mathbb{N}}$–谓词为一个函数 (不一定可计算) $f:X\to 2^{\mathbb{N}}$. 这些谓词之间也有命题逻辑的连词, 只需要逐点使用上面命题的逻辑运算即可.

定义 1.4. 对于两个 $X$ 上的 $2^{\mathbb{N}}$–谓词 $\psi ,\varphi$, 定义蕴涵关系 $\psi {⊢}_X\varphi$: 它为真当且仅当集合$$\bigcap _{x\in X}(\psi \to \varphi )(x)$$非空.

这与 $\psi \to \varphi$ 的定义不同: 后者对于每个 $x\in X$ 可以用不同的自然数具现对应的命题; 前者需要找到一个统一的自然数具现.

这样一来, ${⊢}_X$ 就构成了谓词的偏序. 并且这个偏序中 $\psi \wedge \varphi$ 是交运算, $\psi \vee \varphi$ 是并运算. 并且有 $\chi {⊢}_X\psi \to \varphi$ 等价于 $\chi \wedge \psi {⊢}_X\varphi$, 从而有指数对象.

接下来, 我们也可以定义量词 $\forall ,\exists$. 注意上面定义的量词取值范围是自然数. 而下面要定义的则有更一般的取值集合.

设 $f:X\to Y$ 是一个函数. 那么由函数复合, 任何一个 $Y$ 上的 $2^{\mathbb{N}}$–谓词 $\varphi$ 都自然导出一个 $X$ 上的 $2^{\mathbb{N}}$–谓词 $f^{\ast }\varphi$: 我们定义 $(f^{\ast }\varphi )(x)=\varphi (f(x))$ 即可. 这对于 $⊢$ 来说是单调的. 对于熟悉范畴论的读者, 可以直接用伴随函子的概念定义 $\forall ,\exists$.$$\exists f⊣f^{\ast }⊣\forall f.$$但是对于不那么熟悉这些定义的读者, 也可以用下面这个更浅显的定义:

定义 1.5. 定义 $\forall f,\exists f$ 为从 $X$ 的 $2^{\mathbb{N}}$–谓词到 $Y$ 的 $2^{\mathbb{N}}$–谓词的函数.$$\exists f(\varphi )=y\mapsto \bigcup _{x\in f^{-1}\{y\}}\varphi (x)$$$$\forall f(\varphi )=y\mapsto \{e\in \mathbb{N}\mid \forall x\in f^{-1}\{y\},e(0)\in \varphi (x)\}$$

如果 $f:X\to \{\star \}$, 那么这两个量词就退化成我们熟悉的量词. 而如果 $f:X\times Y\to X$ 为投影函数, 则量词就是对 $y\in Y$ 做量化. (...)

有了必要的工具, 我们可以开始定义有效范畴 $\mathsf{Eff}$ 了.

定义 1.6. $\mathsf{Eff}$ 中的对象是一个集合 $X$ 与 $X\times X$ 上的一个 $2^{\mathbb{N}}$–谓词 (即二元关系) $\approx$, 满足$$\begin{array}{rl}x\approx y& ⊢y\approx x\\ x\approx y\wedge y\approx z& ⊢x\approx z.\end{array}$$注意并没有自反性. 我们记 $x\approx x$ 为 $E(x)$. 范畴里的态射 $(X,\approx )\to (Y,\approx )$ 为 $X\times Y$ 上满足一些条件的 $2^{\mathbb{N}}$–谓词的等价类: $$\begin{array}{rl}F(x,y)\wedge x\approx x^{\prime }\wedge y\approx y^{\prime }& ⊢F(x^{\prime },y^{\prime })\\ F(x,y)& ⊢E(x)\wedge E(y)\\ F(x,y)\wedge F(x,y^{\prime })& ⊢y\approx y^{\prime }\\ E(x)& ⊢\exists y.F(x,y)\end{array}$$如果 $F(x,y)⊢G(x,y)$ 且 $G(x,y)⊢F(x,y)$, 则认为 $F$ 和 $G$ 等价.

(...)

定理 1.7. $\mathsf{Eff}$ 是意象.

2性质

我们有函子 $\Gamma (X)=\mathrm{hom}(1,X)$ 取出某个对象的点集. 此函子有右伴随 $\nabla (X)$, 它给此集合配备余离散的有效结构, 即令 $X\times X$ 上配备的 $2^{\mathbb{N}}$–谓词为$$\varphi (x,y)=\{\begin{array}{ll}\mathbb{N}& (x=y)\\ \varnothing & (x\ne y)\end{array}$$那么常函数 $r(n)=1$ 即可为此谓词的对称性与传递性提供证据. 此函子 $\nabla$ 是全忠实函子, 并且这给出了子意象 $\mathsf{Set}\hookrightarrow \mathsf{Eff}$.

此意象中有自然数对象, 记作 $\mathbb{N}$. 其集合为 $\mathbb{N}$, 而其上配备的二元谓词为 $\varphi (m,n)=\{m\}\cap \{n\}$.

定理 2.1. $\mathrm{hom}({\mathbb{N}}^n,\mathbb{N})$ 是传统意义上的 $n$ 元全可计算函数集合.

这证明了有效意象确实刻画了原本的可计算函数. 而不难验证 $\mathrm{hom}(\nabla \mathbb{N},\nabla \mathbb{N})$ 这个集合就是集合论中的 (不一定可计算的) 全体函数的集合.

术语翻译

有效意象 • 英文 effective topos