计算机构造（三）

在正式进入主题之前，我们先规定一些这篇文章讲要使用的符号。对于两个集合间的部分函数f：A → B 和任意 A 中的元素 α，α' ，我们规定：

• ↓f(α) 表示 f(α) 有定义， ↑f(α) 表示 f(α) 无定义；

• f(α)＝f(α') 表示 f(α)，f(α') 均有定义，且两者的值相等；

• f(α)≃f(α') 表示如果 f(α)，f(α') 二者之中一个有定义，则另一个也有定义，且这种情况下二者的值相等。

计算模型

在数学和计算机领域中，计算这个概念不总是基于自然数的。因此我们需要一个能够处理多种数据类型之间的可计算函数的理论框架。很自然的，不同的数据结构可以看作是不同的类型 [type]；我们假设我们有一个集合T ，其是所有数据类型名称 [type names] 的集合。例如如果我们只想考虑自然数和真值上的计算函数，集合 T 应就只包含两个元素 T＝{nat，bool} 。

我们将T 上的一个计算模型 C 定义为包含如下信息的对象：

• 其给出了以 T 为索引的一系列集合 |C|＝{C(τ)│τ∈T} ，其中每一个集合 C(τ) 都可以看作是类型 τ 下的数据集；

• 对于任意两个类型 σ，τ∈T ，其给定一个集合 C[σ，τ] ，其中的每一个元素都是从 C(σ) 到 C(τ) 的一个部分函数 [partial function]；

• 我们要求 C 在部分函数的复合操作下构成一个范畴。

简单地说，一个T 上的计算模型 C 便是一个对象集合同构于 T 的 Setp 的子范畴 [subcategory]，其中 Setp 是集合和部分函数所构成的范畴。注意，对于我们所关心的大多数计算模型而言， C 都不是 Setp 的一个满子范畴 [full subcategory]，因为一般而言不是所有从 C(σ) 到 C(τ) 部分函数都是可计算的。

这样的定义是符合我们对于可计算性的直观的。对于不同的数据类型，其必定对应着不同的数据集合作为它的值，这便是C(σ) 这些集合所代表的含义。当然，也有可能不同的类型对应着相同的（或同构的）数据集合；我们将在后面看到这一点。在不同的数据类型之间，显然一个从 σ 到 τ 的可计算函数应该至少为一个从 C(σ) 到 C(τ) 的部分函数。直观上来说，至少所有恒等映射应该是可计算的，且两个可计算函数的复合也应该是可计算的。因此，要求 C 构成一个范畴看起来是其构成一个计算模型的必要条件。从这个定义出发，我们来看看常见的一些计算结构如何融入到我们所定义的框架中来。

例子1: 自然数的计算模型. 从现有的研究来看，自然数应该算得上是最基础的计算模型了。我们能很自然地将其纳入上面的框架当中。此时的类型名称集合 T＝{nat} 只包含一个元素，且自然地我们有 C(nat)＝ℕ 。而对于态射我们自然也有 C[nat，nat] 是所有从 ℕ 到 ℕ 地部分可计算函数所构成的集合。容易验证其构成一个范畴。

例子2: untyped λ-calculus. Church 最早对于可计算性地研究基于 λ-calculus，是一种语形（syntactical）的进路。假设我们固定了一个变元集合 [variable set] P （通常其是可数无穷的），则我们可以如下递归定义所有 untyped λ-calculus 的项 [terms]：

M：＝x∈P│MM│λx. M .(1)

我们定义∧ 为所有的项构成的集合在模掉 α-等价后所得到的集合（我们假设读者熟悉 α-等价的概念，其表示的是对于限制变元 [bounded variable] 的重命名）。在 ∧ 上我们还可以进一步定义 β-等价关系，即由下面的条件所生成的最小等价关系：

(λx.M)N ∼ M[N/x]，M ∼ N ⇒ PM ∼ PN，M ∼ N ⇒ λx.M ∼ λx.N . (2)

其中M[N/x] 表示将 M 中的自由变元 [free variable] x 替换为 N 后所得到的项（为了避免 N 中的自由变元在替换到 M 后被限制我们可能需要先替换 M 中限制变元，但这是良定义的，因为在 ∧ 中 α-等价的项代表同一个元素）。我们用 [M] 表示项 M 在 ∼-等价关系下所对应的等价类，将 ∧/∼ 记为 ∧ 在这个等价关系下的商。则我们同样有一个只有一个类型 ℓ 的计算模型，其中 C(ℓ)＝∧/∼ 。对于任意 P∈∧ ，其都对应着一个良定义的映射函数 P：∧/∼ → ∧/∼ ，其定义为 [M] ↦ [PM]。这样的映射称为 λ-可定义函数，在我们的计算模型中，我们也令 C[ℓ，ℓ] 为所有 λ-可定义函数所构成的集合。值得注意的是，所有这样的函数都是完全函数而不是部分函数。感兴趣的读者应自行验证 C 构成一个范畴，即 ∧/∼ 上的恒等映射是 λ-可定义的，且若两个映射均为 λ-可定义，则其复合映射同样为 λ-可定义。

在 Higher-Order Computability 一书中还给出了许许多多的可计算模型的例子，有基于图灵机的，有基于编程语言的，还有和传统递归论和可计算理论中所研究的计算模型更贴近的，限于篇幅我们就不一一介绍了。我们后面的理论介绍将都基于上面给出的这两个最基本的计算模型的例子。

计算模型上的弱笛卡尔闭 [Weakly Cartesian Closed] 结构

我们提到了，我们有许许多多地理由关心高阶的可计算性，但高阶可计算性的具体数学结构只有在今天介绍了详细的计算模型的定义后才能展开说明。对应到我们前面提到的计算模型的范畴结构，高阶计算性表示这个范畴是弱笛卡尔闭的。这一节我们便详细地谈谈这一点。

给定一个T 上的可计算模型 C ，我们说 C 上有一个弱笛卡尔结构 [weak Cartesian structure] 当满足条件：对于 T 中的任意两个类型 σ，τ 我们有一个对应的类型 σ × τ∈T 和两个投影映射 [projection map] πσ∈C[σ × τ，σ] ， πτ∈C[σ × τ，τ] ，使得对于任意 η∈T 和任意 f∈C[η，σ] g∈C[η，τ]，存在一个函数 h∈C[η，σ × τ] 使得对于任意 c∈C[η] 我们有：

• ↓h(c) 当且仅当 ↓f(c) 且 ↓g(c) ；

• 在这种情况下， πσ(h(c))＝f(c) ，πτ(h(c))＝g(c) 。

值得注意的是，在上面的定义中我们仅仅要求函数h 的存在性而不要求其唯一性，这是我们说它构成一个“弱”笛卡尔结构的原因。同时一般地，我们并不一定有 πσ◦h＝f ，因为可能对于某些 c，↓f(c) 但 ↑g(c) ，因此根据定义我们必定有 ↑h(c) ，这表示 ↑πσ◦h(c) 。当某个 d∈C(σ × τ) 满足 πσ(d)＝α ， πτ(d)＝b 时，其中 α∈C(σ) ， b∈C(τ) ，我们称 d 表示了 (α，b) 这个有序对。对于一般计算模型上的弱笛卡尔机构，不一定任意 C(σ) × C(τ) 中的有序对都由一个 C(σ × τ) 中的元素表示，但对于许多常见的计算模型，如我们下面会提到的两个例子，这是成立的。

完全类似的，我们可以定义什么是C 中的一个弱终对象 [weak terminal object]：它由一个类型 ι∈T 和一个元素 i∈C[ι] 构成，使得对于任意的类型 σ∈T ，将所有 C[σ] 中的元素都映射到 i 的常函数是 C[σ，ι] 中的一个可计算函数。

感兴趣的读者可以尝试思考，在什么意义下弱笛卡尔积结构和弱终对象是不依赖于我们具体选择的，即当对于两个类型σ，τ 我们有多个类型和多个投影映射都满足是 σ，τ 的弱笛卡尔积时它们之间有什么关系；或者当我们有多个弱终对象时，它们之间是什么关系。这些问题的答案应该是与范畴论中在同构的意义上定义笛卡尔积和终对象类似。有了如上定义，我们可以来看看之前提到的两个计算模型的例子。事实上，它们上面都有弱笛卡尔结构以及弱终对象。

例子1: 自然数的计算模型. 在这个例子中我们的类型结合 T 中只有一个类型 nat ，因此我们别无选择只能有 nat 和 nat 的弱笛卡尔积就是其本身！这样定义的确能够构成一个弱笛卡尔积结构是由于我们有许多从 ℕ × ℕ 到 ℕ 的可计算函数构成它们之间的双射，比如下面定义的这个可计算函数 B ：(m，n)↦m＋(m＋n)(m＋n＋1)/2. (3)

显然，当我们有了这个双射B ，在弱笛卡尔积结构中我们所需要的两个投影映射可以分别定义为

πₙₐₜ，₁＝π₁◦B⁻¹，πₙₐₜ，₂＝π₂◦B⁻¹. (4)

容易验证，对于任意两个部分可计算函数f，g：ℕ⇀ℕ ，我们可令 h 为 B◦〈f，g〉 ，显然其满足我们上面陈述的两个条件。由此可见，对于我们第一个非常基础的自然数的计算模型，其有一个弱笛卡尔积结构。同时由于 B 是一个双射且 πₙₐₜ，₁ ， πₙₐₜ，₂ 都为完全函数，对于任意自然数的有序对 (m，n) 它都由某一个自然数表示。我们选取不同的 ℕ × ℕ 和 ℕ 之间的双射能够得到不同的弱笛卡尔积结构。这个计算模型具有一个弱终对象是显然的，因为任意 ℕ 到 ℕ 的常映射都是可计算的。

例子2：untyped λ-calculus. 对于第二个 λ-calculus 所对应的计算模型的例子，熟悉一些基本的 untyped λ-calculus 理论的读者应该都应该能够猜想到其也必定具有弱笛卡尔积结构。和例子1完全类似，在这个计算模型中我们也只有一个类型，因此其笛卡尔积必定只能是其自身。我们同样需要找到一个 pairing 函数使得 ∧/∼ 本身就能够表达 ∧/∼ × ∧/∼ 的信息。由我们的定义可知，在此计算模型中所有的可计算函数都由一个项生成。特别地，我们如下可以定义 ∧ 中的一个项：

pair：＝λxyz.zxy. (5)

其中λxyz 是 λx.λy.λz. 的缩写；还有如下的两个项：

fst：＝λp.p(λxy.x)，snd：＝λp.p(λxy.y).(6)

此时，对于任意两个C 中的可计算函数，即两个项 M，N ，我们这个有序对所对应的可计算函数可以选为 pair M N （注意，在 λ-calculus 的语境下项都默认为是左侧结合的）。由于 C 中全是完全函数，因此我们可以直接结算 fst 和这个函数的复合；在项的层面这就是将这两个项相作用：

fst(pair M N)＝[λp.p(λxy.x)](λxyz.zxy M N)

＝[λp.p(λxy.x)](λz.zM N)

＝(λz.zMN)(λxy.x)

＝(λxy.x)M N

＝M

(7)

上面的计算完全遵从于 (2) 中提到的β-等价关系。完全类似地，大家可以计算 snd(pair M N) ，其结果也必定和 N 相等。由此可见， λ-calculus 所对应的计算模型也具有弱笛卡尔积的结构，且同样地对于任意一个有序对都有一个表示项与其对应。和例子1类似，任意 ∧/∼ 到其自身的常映射都是 λ-可定义的，因此其上也具有弱终对象。

由此可见，对于前面提到的两个基本的计算模型的例子，尽管它们都只有一个数据类型，但它们都具有弱笛卡尔积结构，其原因也符合我们的直观：利用它们本身的数据集合就能够编码它们自身成对的信息。

目前为止，我们还不涉及高阶计算的内容，因为弱笛卡尔积结构从直观上只是说明在我们的计算模型中能够表达成对的数据值。与高阶计算内容密切相关的是弱笛卡尔积闭的结构。换句话说，我们要求可计算函数本身作为数据也能够在我们的计算模型中进行表达。这也就是我们接下来要阐述的。

我们称一个T 上的具有弱笛卡尔积和弱终对象的可计算模型 C 上具有一个弱笛卡尔积闭 [weakly Cartesian closed] 结构，当我们给出如下信息：

• 对于任意两个类型 σ，τ∈T，我们指定一个类型 σ → τ∈T ；

• 一个部分函数 ·στ：C(σ → τ) × C(σ) ⇀ C(τ) ；

使得对于任意η∈T 和任意部分函数 f：C(η) × C(σ) ⇀ C(τ) ，下面两个条件是等价的：

1. f 存在一个 C[η × σ，τ] 中的部分函数 ˉf 为其表示，即对于任意 d∈C(η × σ) ，若其是 (α，c)∈C(η) × C(σ) 的表示，则 f(c，α)≃ˉf(d) ；

2. 在 C[η，σ → τ] 中有一个完全函数 ˆf 满足对于任意 c∈C(η) ， α ∈ C(σ) ， ˆf(c) · στ α≃f(c，α) 。

直观上来说，高阶计算性或者弱笛卡尔闭结构是想说明C(σ) ⇀ C(τ) 这样的部分函数可以由 σ → τ 这个类型的值，即 C(σ → τ) 中的元素表示。这个定义和一般范畴论中的笛卡尔积闭结构最大的不同在于，对于任意的一个函数 f 若其表示存在，我们并不要求其表示函数 ˆf 是唯一的。换句话说， C(σ → τ) 中的元素是内涵性物体 [intensional objects]，如一段程序或者是一个算法，我们可以有多个内涵性物体对应着同一个可计算函数的外延。从如上的定义中我们也可以看出， ·στ 这个部分函数也必定由某个 C[(σ → τ) × σ，τ] 中的函数表示，因为在 C[σ → τ，σ → τ] 中我们有 C(σ → τ) 上的恒等映射；我们把这个函数记为 αppστ 。我们再次来看看前面提到的两个计算模型的例子上的高阶计算结构。

例子1：自然数的计算模型. 和之前类似，由于我们只有一个类型 nat ，因此如果其上有高阶计算结构我们也必定有 nat → nat＝nat 。在考虑高阶计算结构的时候我们需要对可计算函数的具体实现方式作出更多的说明，因为如前所述，高阶计算模型不仅要考虑可计算函数的外延，还要考虑其内涵。因此此时，可计算函数的具体实现方式变得相关了。假设我们采用了图灵机的表述（换用其他常见的可计算函数表述，如传统递归论的或是其他类型的也是可以的，只是我们得到的高阶模型会有些细微的差别），则高阶计算结构（把自然数本身看作是某个程序，因为我们此处有 nat → nat 和 nat 是同一个类型）具体实现方式是通过对所有的图灵机进行编码。假设我们选取了一个合适的编码，并用 Tₙ 表示第 n 号图灵机（由于有不同的图灵机计算相同的可计算函数，这显示了当我们把自然数本身看作是可计算函数的编码时其所表示的是内涵的结构，而不单纯是可计算函数的外延）。可计算理论中一个很重要的结果便是存在一个通用图灵机 U 使得当我们输入一个有序对 (e，α) 时，我们有 U(e，α)≃Tₑ(α) 。显然，我们可以把 U 对应的可计算函数作为我们的部分函数 ·：ℕ × ℕ → ℕ 。在自然数的计算模型中由于我们的函数 B 是一个双射，因此任意可计算的 f：ℕ × ℕ → ℕ 都有一个对应的函数 ˉf：ℕ → ℕ 为其表示，其可以自然地选为如下的函数：

ˉf＝f◦B⁻¹ (8)

此时我们也有另一个完全可计算函数ˆf 满足 ˆf(c) · α≃f(c，α)。这来自于基本递归论中的 Kleene s-m-n 定理：对于任意一个图灵机 T ，存在另一个完全图灵机 T' 使得对于任意 c，α∈ℕ， Tᴛ'₍ᴄ₎(α)≃T(c，α) 。由此可见，我们基于自然数的计算模型是一个完整地高阶计算模型；在计算理论的文献中，这个模型一般被称为第一 Kleene 模型 [Kleene's first model]，记为 K₁ 。

例子2: untyped λ-calculus. untyped λ-calculus 的高阶可计算性某种意义上要比自然数模型的高阶性要更自然也显然一些。显然同样的，在这个模型中我们也必定有 ℓ → ℓ＝ℓ 。其上的函数 M 非常自然的就是项之间的作用函数。假设我们有一个项 M 表示了某个函数 f：∧/∼ ×∧/∼ → ∧/∼，使得对于任意两个项 N，N' 我们有 M(pair N N')＝f(N，N') ，则此时我们可以令 λxy.M(pair x y) 为表示 ˆf 的项。此时我们有，

[λxy.M(pair x y)] N N'＝M(pair N N')＝f(N，N') (9)

这同样说明了 untypedλ-calculus 的计算模型是弱笛卡尔积闭的，其上很自然的有高阶计算结构。

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