计算机构造（五） (5-1)

我们介绍了高阶计算模型的基本理论框架。让我们简单回忆一下：在一个类型名称集合 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(γσ) 中的数据来表示它）；

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。