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

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

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