更改

递归定理 (查看源代码)

2026年9月10日 (四) 12:41的版本

添加24字节、 2026年9月10日 (星期四)

第544行：第544行：

其中图灵停机问题、哥德尔不完备定理拥有'''双重身份'''：结论是否定性的（与康托尔、罗素问题同类），历史原证也走否定性对角线老路、不依赖 SRT；但因活在程序世界，又能被 SRT 事后更简洁地推出（[[#图灵停机问题（1936）|§5.7.3]] 展示了停机问题的完整套用过程）。它们共同构成 SRT 的"自指"一面；SRT 还有另一面——"沿序数逐层构造"——见[[#SRT的其它应用|第六节]]。

−

== SRT的其它应用 ==

+

=== SRT的其它应用 ===

上一节（[[#SRT与自指|§5.7]]）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造不直接涉及自指的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（[[有效超限递归]]）——把递归定义从自然数推广到[[序数]]，从而定义出越来越复杂的对象。本节即以它开篇（前4个例子）；此后转入其余主题——注意第5个板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：

第550行：第550行：

'''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />

−

=== 通用序数记号系统与<math>\omega_1^{CK}</math> ===

+

==== 通用序数记号系统与<math>\omega_1^{CK}</math> ====

第594行：第594行：

Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。

−

=== 构造序数 = 递归序数 ===

+

==== 构造序数 = 递归序数 ====

可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 [[#6.1|6.1]]）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。

第602行：第602行：

这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽<ref name="moschovakis2010" />。

−

=== 超算术层级与 Spector 唯一性定理 ===

+

==== 超算术层级与 Spector 唯一性定理 ====

需要先铺垫三个概念。

第623行：第623行：

证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 [[#推论：SRT 衍生出的若干重要结果|§5.2]] 的 [[雷蒙德·斯穆里安|Smullyan]] 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />。

−

=== <math>HYP = \Delta^1_1</math> 与有效描述集合论 ===

+

==== <math>HYP = \Delta^1_1</math> 与有效描述集合论 ====

第640行：第640行：

此外，Kleene 1940 年代为直觉主义数学（拒绝排中律的构造性数学）构造的'''可实现性（realizability）'''中，[[bar递归定义]]、[[bar归纳]]与[[连续性原理]]的验证也本质地使用 SRT 的各种形式<ref name="moschovakis2010" />。

−

=== r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill ===

+

==== r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill ====

本板块把"程序行为性质"当作一个独立的研究对象。核心概念是'''索引集（index set）'''：给定某类程序行为，把"行为落在这类里"的全部程序编号收集起来，就得到 <math>\mathbb{N}</math> 的一个子集。若用程序 e 的定义域 <math>W_e</math>（[[#递归可枚举集（r.e. set）|§2.4]]）来编码行为、用 <math>\mathcal{A}</math> 表示某类 r.e. 集，则写法是

第652行：第652行：

与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|6.5.3]]）。

−

==== [[Rice定理]]（1951） ====

+

===== [[Rice定理]]（1951） =====

'''[[Rice定理|莱斯定理]]'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。

第665行：第665行：

'''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。

−

==== Rice-Shapiro 定理（1956） ====

+

===== Rice-Shapiro 定理（1956） =====

Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：

第675行：第675行：

Rice-Shapiro 不是 SRT 的推论，而是索引集理论中独立的结构定理，并且它比 Rice 定理更强——由它可以推出 Rice 定理：若非平凡索引集 A 可计算，则 A 与补集都是 r.e. 索引集，Rice-Shapiro 给 <math>\mathcal{A}</math> 与其补类都套上"有限可生成"；而有限可生成自动蕴含"超集仍在类中"，把两个类里各自的成员并起来，就得到同时属于两类的一个 r.e. 集，矛盾。可见在"识别程序性质"的问题上，真正的母定理是 Rice-Shapiro 而非 SRT<ref name="rogers1967" /><ref name="soare1987" />。

−

==== [[Myhill定理]]：[[创造集]] = [[完备集]] ====

+

===== [[Myhill定理]]：[[创造集]] = [[完备集]] =====

'''背景'''：停机问题集合 <math>K = \{e : \text{程序} e \text{在输入} e \text{上停机}\}</math> 是 r.e. 集中"最不可判定"的——任何 r.e. 集都能通过可计算的翻译归约到它（称为 [[r.e.-完备|递归可枚举完备]]）。另有一个看似完全不同的概念：一个 r.e. 集 A 称为'''[[创造集]]（creative set）'''，如果它的补集是"能系统地生产反例"的——存在一个可计算程序，你给它任何与 A 不交的 r.e. 集，它都能吐出一个既不在 A 里也不在那个集合里的元素。创造性是 Post在1944 年为刻画"不可判定的源泉"而引入的概念。

第683行：第683行：

'''证明中 SRT 的关键一步'''：想把任意 r.e. 集 B 归约到创造集 A，需要构造一个程序 <math>z</math>，使得"若 <math>x\in B</math>，则 <math>z</math> 枚举出<math>\{u(z)\}</math>；否则 <math>z</math> 枚举空集"——'''<math>z</math> 的定义里用到了 <math>z</math> 自己的编号'''（<math>u(z)</math> 是生产反例的程序作用于 <math>z</math>）。这正是 SRT 合法化的自指；没有这个自指，证明无法闭合。由此 Rogers 还得到推论：'''所有创造集在"可计算的重新命名"意义下完全相同（两两递归同构）'''——从可计算性角度看它们"长得一模一样"<ref name="rogers1967" />。

−

=== 有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理 ===

+

==== 有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理 ====

'''背景'''：一个"程序变换"<math>\Phi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Phi(\phi)</math>。有两种实现方式：'''按代码操作'''（给 <math>\Phi</math> 输入 <math>\phi</math> 的程序编号，让它随便分析代码——类似"按名调用"）与'''按值操作'''（<math>\Phi</math> 只能查询 <math>\phi</math> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：

第697行：第697行：

此外，Rogers 用 SRT 证明了 '''[[Blum定理]]'''：任意两个"[[通用部分函数]]"（即[[解释器]]）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一<ref name="rogers1967" />.

−

=== Solovay 可证性逻辑 ===

+

==== Solovay 可证性逻辑 ====

'''背景'''：'''[[可证性逻辑]]（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在皮亚诺公理体系中可证" 抽象为模态算子 □<math>\phi</math>。[[模态逻辑]]系统 '''GL'''（[[Gödel-Löb 逻辑|Gödel-Löb 逻辑]]）是候选公理系统。

第705行：第705行：

[[罗伯特·索洛韦|Solovay]] 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h，其中 h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论到：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。

−

=== 应用地图一览 ===

+

==== 应用地图一览 ====

{| class="wikitable"

Jake

行政员、界面管理员、管理员

3,094

个编辑