数学联邦政治世界观
超小超大

计算机构造(五) (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),接着再看更方便。

相关小说

寒花吟 连载中
寒花吟
玫艾
寒月缘
0.4万字9个月前
爆裂飞车之迎着海风,走过夕阳,人生浪荡,无人能降 连载中
爆裂飞车之迎着海风,走过夕阳,人生浪荡,无人能降
摆渡翎殉ROSE
逐峰他有姐姐?逐峰隐藏了什么秘密?十二星座,能向他致敬吗?【本书原名《爆裂飞车之逐峰与他的姐姐》】
0.5万字9个月前
蔽月危局之宿命轮回 连载中
蔽月危局之宿命轮回
努力码字的凤倾歌
〖已签约〗CP:外冷内热“学神”(风琼宇)X温柔自卑“学渣”(楚月泠)关键词:前世今生/轮回诅咒/糖里带刀核心梗:命运残酷,如何把死局盘活?......
38.4万字9个月前
沧海桑田,我们回不去了 连载中
沧海桑田,我们回不去了
墨雨殇情
【已签约,禁止转载】她叫雪儿,倾国倾城她叫以沫,富可敌国她为了朋友隐瞒了身世她为了队友离开了家族他陪她走过了沧海桑田他陪她玩转了沧海桑田不论......
6.9万字9个月前
嘎了几次手握女主剧本了! 连载中
嘎了几次手握女主剧本了!
杨总会成裁
多男主,现在先保证每个男主有基本的20章!芝麻馅汤圆,温柔似水,风骚的……尽量给你们凑齐全部性格的男主准备高考,随缘更新几世纠缠,她与他是斩......
11.6万字9个月前
舞桐堕落,雨浩挽回 连载中
舞桐堕落,雨浩挽回
橙子渣女.
简介正在更新
1.0万字9个月前