计算机构造（五）

我们介绍了高阶计算模型的基本理论框架。让我们简单回忆一下：在一个类型名称集合 T 上的高阶计算模型 C 是 Setp —— 集合和部分函数构成的范畴 —— 的一个子范畴，其中 C 中的物体与 T 同构。对于任意 σ，τ∈T 我们用 C(σ) 表示类型 σ 下的数据集合，用 C[σ，τ] 表示类型 σ，τ 之间的可计算函数，它们都是 C(σ) 到 C(τ) 的部分函数。我们称 C 为一个高阶计算模型当 C 上有一个弱笛卡尔闭结构。

一个以自然数为基础，我们在这篇文章中称其为C₁ ；一个以 λ-calculus 为基础，我们称其为 C₂ 。它们都是单类型计算模型，我们为了简化就将它们的类型都记为 * 。其中我们有 C₁(*)＝ℕ， C₁[*，*] 为所有 ℕ 到 ℕ 的部分可计算函数； C₂(*) 为 ∧/∼ ，即所有 λ-term 模掉 β-equivalence；C₂[*，*] 为所有 λ-可定义的函数。

在这篇文章中，我们主要想要讨论的问题是，我们如何能够比较不同的计算模型？在之前的文章中我们提到过，如果仅仅考虑 extensional 的可计算函数，采用自然数的可计算模型和λ-calculus 的计算模型是一样的。具体的，在 λ-calculus 当中我们可以定义数字 [numerals]，其中对于任意 n∈ℕ 我们可以定义一个对应的闭项 λfλx.fⁿx ；那么在 C₂[*，*] 所定义的这些 numeral 之间的可计算函数和我们用图灵机定义的自然数之间的可计算函数是完全一致的！这在可计算理论早期是一个非常重要的结论。

但我们之前也提到过了，C₁ 和 C₂ 两个计算模型之间也有一些不同。例如， C₂[*，*] 中所有的函数都是完全的，即其所有可计算函数的定义域都是 C₂(*) 本身；这对 C₁ 来说并不成立。

计算模型之间的模拟

我们提到了计算模型之间一个自然的关系是一个计算模型在另一个计算模型中的模拟 [simulation]。直观地来说，如果我们有两个计算模型 C，D ， C 在 D 中的一个模拟指的是 (1) 首先我们能用 D 的数据模拟 C 的数据；(2) 这些模拟使得对于每一个 C 中的可计算函数都能被 D 中的可计算函数追踪 [track]。严格地来说，我们需要如下的定义：

定义：对于任意两个计算模型 C，D ，我们称 γ：C → D 为 C 在 D 中的一个模拟，当我们有：

• 对于任意 C 中的类型 σ ， γ 给出 D 中的一个模型 γσ （直观来说， γσ 是 D 中模拟 C 中 σ 的类型）；

• 在这种情形下，我们有一个二元关系 ⊩γσ⊆D(γσ) × C(σ) （直观来说， α'⊩γσα 表示我们用 D(γσ) 中的 α' 来模拟 C(σ) 中的 α ）；

同时满足如下条件：

• 对于任意 α∈C(σ) 我们存在 α'∈D(γσ) 使得 α''⊩γσα （直观来说，这个条件表示对于 C(σ) 中的每一个数据值我们都存在 D(γσ) 中的数据来表示它）；

• 对于任意 f∈C[σ，τ] ，我们存在 f'∈D[γσ，γτ] 能追踪 f ，即若 α'⊩γσα 且 f(α) 有定义，则 f'(α') 也有定义且 f'(α')⊩γτ f(α) （直观来说， f' 在我们 γ 所描述的表示的含义下模拟 f ）。

容易看出的是，对于任意计算模型C 我们有一个恒等模拟；两个模拟 γ：C → D 和 δ：D → E 之间也能够复合。这表示在模拟作为态射下，计算模型本身构成了一个范畴 Cmp。从计算模拟的定义我们可以简单地理解为，如果有一个 γ：C → D 的模拟，则从某种程度上而言 C 中的计算概念更加“抽象”，而这种抽象的计算概念通过 γ 有了一个在 D 中更加具体的实现。

但在此之上还有更进一步的结构可以考虑，在之前的文章中我们曾经提到过，Cmp 自然地构成了一个 2阶范畴 [2-category]。和函子间的自然变换类似，对于两个模拟 γ，δ：C → D ，我们有如下可计算转换 [computable transformation] 的概念：我们说可以将 γ-模拟可计算地转换为 δ-模拟，记为 γ⪯δ ，当对于任意 C 中的计算类型 σ ，存在 D 中的一个可计算函数 t∈D[γσ，δσ] 使得如下成立：

∀α∈C(σ)，∀α'⊩γσ α.t(α')⊩δγα.(1)

熟悉自然变换概念的读者可以看出，其与可计算转换的概念有着相似性。但在考虑可计算转换时，我们只考虑这些可计算函数t∈D[γσ，δσ] 的存在性，而 t 本身不是可计算转换这个结构的一部分。这使得 C 到 D 的计算模拟这个集合构成了一个预序 [preorder]，而不是像两个范畴之间的函子和自然变换那样是一个更为一般的范畴。我们之所以这样定义，是因为和之前定义弱笛卡尔积闭结构时类似，在计算模型中这样的可计算函数 t 通常并不具有唯一性， 在 D 中我们可以有很多不同的函数使得 γ 可以可计算地转换到 δ ，而在实际应用中我们只关心这样转换的可能性，而似乎并不关心具体转换实现的方式。因此，Cmp 是一个 preorder-enriched category，或者说一个任意两个 1-cell 之间的 2-cell 都同构的 2-category。

对于任意一个 2阶-范畴，我们都有一个自然的弱于同构的对等价的定义。以范畴为例，我们通常说两个范畴C，D 是等价的 [equivalent] 当我们有如下两个函子 F：C → D ， G：D → C ，使得两边的复合并不直接等于 C，D 上的恒等函子，但和它们之间自然同构：

idᴄ≃GF，idᴅ≃FG (2)

同样的，在计算模型的语境下，我们说两个计算模型C，D 之间是等价的，当我们有两个计算模拟 γ：C → D ， δ：D → C 使得它们满足

idᴄ≃δγ，idᴅ≃γδ (3)

其中，idᴄ≃δγ 表示 idᴄ ⪯ δγ 且 δγ ⪯ idᴄ 。因此，基于这个 2阶-范畴 Cmp 我们对计算模型之间的模拟和等价便有了一个完整地描述了。

现在让我们回到我们之前的例子C₁，C₂ ，分别为自然数的可计算模型和 λ-calculus 的可计算模型。基于我们之前的讨论，我们知道它们之间存在双向的计算模拟。具体地，我们可以通过一个哥德尔编码 [Gödel numbering] 构造一个从 λ-calculus 到自然数模型的模拟 γ：C₂ → C₁ 。我们可以对任意的 λ-term 进行编码，对任意 λ-term M ，我们用 ⌜M⌝ 表示 M 的哥德尔编码，我们要求这个编码是有效的 [effective]。在这个编码下，我们说一个自然数 n 表示了一个 ∧/∼ 中的一个元素 [M] （ [M] 为一个 λ-term 的 β-等价类），即 n ⊩ [M] ，当且仅当存在 M' ∼ M 使得 ⌜M'⌝＝n 。因此在这个顶一下，对于一个 λ-term 的等价类，我们有多个自然数是其表示。显然，对于任意 C₂ 中的可计算函数 [M] ↦ [PM]，在我们的有效编码下其会转换为一个 ℕ 上的一个可计算函数。因此，我们得到了一个计算模拟 γ：C₂ → C₁ 。

另一方面，由于在λ-calculus 中有 Church 数字 [Church numeral]，我们将 n 的 Church 数字 λfλx.fⁿx 记为 ˆn 。对于任意自然数 n 我们可以定义 ˆn ⊩ n 。在此基础上，递归论经典的结论告诉我们对于任意自然数上的可计算函数，都存在一个 λ-term P 使得 P 对应的 ∧/∼ 上的函数与这个可计算函数对应。因此，这也定义了另一个方向的计算模拟 δ：C₁ → C₂ 。

显然，这两个计算模拟复合后并不直接等于C₁ 或 C₂ 上的恒等模拟，但我们有恒等模拟和这两个复合之间的计算转换。首先考虑 γδ ：一方面，从任意自然数 n 我们能够有效地计算出其 Church 数字所对应的哥德尔编码，因此 n↦⌜ˆn⌝ 是可计算的，这表明我们有 idᴄ₁ ⪯ γδ 。另一方面，对于任意 M ∼ ˆn ，从 M 的哥德尔编码 ⌜M⌝ 我们也能够有效地计算出 n ，这显示 γδ ⪯ idᴄ₁ 。于是在 C₁ 的方面我们的确有 idᴄ₁≃γδ 。

我们再来考虑C₂ 的方向。首先，Kleene 有一个非常经典的递归论结论表明，对于一个确定的哥德尔编码，存在一个 λ-term E ，称为一个计数项 [enumerator]，使得

︿

E⌜M⌝ ∼ M。这表明我们有 δγ ⪯ idᴄ₂ 。但重点在于， idᴄ₂ ⪯ δγ 并不成立。这是因为在 λ-calculus 自己当中，我们不可能有一个 λ-term P 使得它把任意 λ-term M 转换到自己哥德尔编码所对应的 Church 数字；直观上来讲，这是因为 λ-calculus 自身并不能检视自己的语法（编码的具体实现和 λ-term 的语法息息相关）。

从这个例子来看，显然γ，δ 并不构成两个计算模型 C₁，C₂ 之间的等价。事实上，这两个模型之间不存在任何等价。这个初步的结论和我们之前的直观是相吻合的。这个结论也深刻体现了高阶计算模型的有点：它能够反映之前仅仅考虑计算函数外延，即从 ℕ 到 ℕ 的部分可计算函数，所不能反应的计算模型之间更加细微的差异。这种差异对我们研究一般的计算模型和它们之间的关系是非常重要的。

计算模型的集群范畴

我们提到了定义计算模型之间的模拟和转换后，也即定义了 Cmp 这个 2阶-范畴后，更进一步的问题。在我们现在的定义中，几乎所有出现的都是弱结构，在其他数学分支中较少见到，检验各个定义也比较繁琐。这也使得直接研究 Cmp 的结构变得比较困难。性质更好的数学结构，使得我们有从 Cmp 到这个结构的函子，能够反应计算模型的基本性质。这和我们在拓扑中寻找代数不变量的基本想法是非常类似的：一个拓扑空间可能是通过各种粘接和分割的操作构造而成的，其自身可能比较复杂；但当我们考虑这个空间上的代数不变量时，我们可以对这个空间的基本性质有非常好的描述。

在计算模型的语境下，这样的构造叫集群范畴 [category of assemblies]。对于任意一个计算模型 C ，我们可以构造它对应的集群范畴 Ass(C) 。限于篇幅，我们并不再详细地介绍集群范畴的具体定义了，只是在这里指出这个构造满足如下一些非常良好的性质：

• Ass(一) 的构造构成了一个从 Cmp 到 CAT 的 2阶-函子 [2-functor]（事实上，这个构造是从 Cmp 到 CAT/Set 的 2阶-函子）；

• Ass(C) 和 Ass(D) 之间的函子是从 C → D 之间的模拟生成的当且仅当其保持 Ass(C) 中一定的范畴结构；特别地， C 和 D 作为计算模型是等价的当且仅当 Ass(C) 和 Ass(D) 这两个范畴是等价的；

• Ass(C) 反映了计算模型 C 的结构： C 具有弱笛卡尔积结构、弱笛卡尔积闭结构、当且仅当 Ass(C) 是具有笛卡尔乘积、是一个笛卡尔闭范畴；

• 若 C 只有一个计算类型，即 T 是一个单点集 [singleton]，且其具有是弱笛卡尔积闭结构，则 Ass(C) 是一个伪拓扑斯 [quasi-topos]，且其能够进一步生成实现拓扑斯 [realisability topos]，这和直觉主义逻辑以及可计算理论之间有着十分深刻的关联；

直观上来说，Ass(C) 可以看作是由那些可以用 C 这个具体的计算模型表示的抽象数据结构 X 所构成的范畴。换而言之，它在某种意义上是所有那些可以通过计算模型 C 具体实现的抽象数据类型。这样构造的存在性和它具有的良好的数学性质从侧面印证了我们对于计算模型之间模拟和计算转换的定义是有实际数学意义的。通过研究范畴性质更好的集群范畴，我们可以对计算模型的性质有更好地把握。例如，我们可以通过集群范畴的性质判断之前提到的 C₁，C₂ 两个计算模型之间不是等价的。

集群范畴在其他方面还有更多的应用，此处我们也不过多展开了，感兴趣的读者可以去阅读原著 Higher-Computability Theory，或者是 Realizability: An Introduction to its Categorical Side.

结语

这篇文章我们延续之前的介绍，定义了计算模型之间的模拟和计算转换，得到了一个 2阶-范畴Cmp，通过这个 2阶-范畴定义了计算模型之间的等价，并且初步地说明了，在高阶计算模型的框架下自然数的计算模型和基于 λ-calculus 的计算模型之间不是等价的。我们也简单地讨论了从计算模型到集群范畴的构造，表明了这之后有着更加优美和深刻的数学结构。我们有许许多多其他关于计算模型的技术和应用没有涉及；事实上，高阶计算模型在计算机语言语义、可计算结构、（高阶）直觉主义逻辑等等领域有着更加深刻广泛地应用。感兴趣的读者可以翻阅 Higher-Computability Theory 一书的相关章节，两位作者对于高阶计算理论发展的历史和应有有着非常好的阐述。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。