更改

递归定理 (查看源代码)

2026年9月9日 (三) 17:18的版本

添加1,397字节、 2026年9月9日 (星期三)

无编辑摘要

第202行：第202行：

推广到 <math>k</math> 元：对任意 <math>k</math> 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 <math>k</math> 个程序 <math>m_1</math>, <math>\ldots</math>, <math>m_k</math> 使得 <math>\phi_{m_i}(x) = g_i(\langle m_1, \ldots, m_k\rangle, x)</math>。

−

[[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① §6.3 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（§6.6 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"~~证明也走双递归路线。~~<ref name="smullyan1961" /><ref name="rogers1967" />

+

[[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① §6.3 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（§6.6 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"证明也走双递归路线<ref name="smullyan1961">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§5.2.1】</ref><ref name="rogers1967" />.

==== Rogers 同构定理（1958） ====

第230行：第230行：

直觉上：[[R. R. Arslanov|Arslanov]] 判据说"装得下所有 r.e. 集合"等价于"对每个 r.e. 集合都有机械的相对化方式"——这和 SRT 中"对每个全可计算 <math>f</math> 都给出一个不动点"的相对化版本（relativized SRT）说的是同一件事：SRT 的相对化是说"对每个以 <math>C</math> 为'''神谕'''（oracle）可计算的 <math>f</math>，存在不动点 <math>c</math>"；Arslanov 判据说"对每个 <math>W</math>，存在以 <math>C</math> 为[[谕示机|神谕]]可计算的归约"。

−

[[Arslanov 判据]]在[[递归论]]里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"[[PA不一致]]"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"<ref name="arslanov1981" /><ref name="soare1987" />。

+

[[Arslanov 判据]]在[[递归论]]里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"[[PA不一致]]"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"<ref name="arslanov1981">'''Arslanov, R. R. (1981).''' On a class of recursively enumerable sets. ''Algebra and Logic'', 20, 324–328.【Arslanov 完全性判据】【§5.2.3】</ref><ref name="soare1987" />。

=== 证明：一行对角线 ===

第418行：第418行：

* 因此应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。

−

'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969" />。

+

'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。

=== SRT与自指===

第450行：第450行：

'''现象'''：实数集不可数。假设每个实数都被编号 <math>0, 1, 2, \ldots</math>；定义一个新实数，令它的第 <math>n</math> 位小数与"编号 <math>n</math> 的实数"的第 <math>n</math> 位小数都不同。这个新实数不在原表里——矛盾<ref name="cantor1891">'''Cantor, G. (1891).''' Über eine elementare Frage der Mannigfaltigkeitslehre. ''Jahresbericht der Deutschen Mathematiker-Vereinigung'', 1, 75–78.【对角线论证的源头】</ref>。

−

'''与 SRT 的关系：同源，但独立'''。两者做了同一件事——取"第 <math>i</math> 个对象在第 <math>i</math> 个位置上的值"（对角线）：康托尔取"第 <math>i</math> 个实数的第 <math>i</math> 位小数"，SRT 取"第 <math>e</math> 个程序在输入 <math>e</math> 上的值"<math>\phi_e(e)</math>（即证明里的 <math>S(e, e)</math>）。但'''方向相反'''：康托尔取对角线后'''改动'''它，制造一个"不在表里"的对象，从而证明实数'''不可数'''；SRT 取对角线后'''固定'''它，得到一个"引用自己编号"的程序，从而证明自指程序'''存在'''。注意，SRT '''推不出''' 康托尔定理——SRT 的结论都活在"程序 / 可计算"的世界里，给不出"实数不可数"这种纯集合论命题；两者只是共享了同一个技巧<ref name="cantor1891" /><ref name="moschovakis2010" />。

+

'''与 SRT 的关系：同源，但独立'''。两者做了同一件事——取"第 <math>i</math> 个对象在第 <math>i</math> 个位置上的值"（对角线）：康托尔取"第 <math>i</math> 个实数的第 <math>i</math> 位小数"，SRT 取"第 <math>e</math> 个程序在输入 <math>e</math> 上的值"<math>\phi_e(e)</math>（即证明里的 <math>S(e, e)</math>）。但'''方向相反'''：康托尔取对角线后'''改动'''它，制造一个"不在表里"的对象，从而证明实数'''不可数'''；SRT 取对角线后'''固定'''它，得到一个"引用自己编号"的程序，从而证明自指程序'''存在'''。注意，SRT '''推不出''' 康托尔定理——SRT 的结论都活在"程序 / 可计算"的世界里，给不出"实数不可数"这种纯集合论命题；两者只是共享了同一个技巧<ref name="cantor1891" /><ref name="moschovakis2010">'''Moschovakis, Y. N. (2010).''' Kleene's amazing second recursion theorem. ''The Bulletin of Symbolic Logic'', 16(2), 189–239.【18 个应用的权威综述；本文应用部分的章节编号均指此文】</ref>。

==== 罗素悖论（1901） ====

第615行：第615行：

问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？

−

* '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的<ref name="spector1955" /><ref name="moschovakis2010" />。

+

* '''Spector 唯一性定理（1955）'''：不会。<math>H_\alpha</math> 的可计算度只依赖序数 <math>\alpha</math> 本身，与代号选择无关；而且不同代号之间的翻译是一致可计算的<ref name="spector1955">Spector, C. (1955). Recursive wellorderings. ''The Journal of Symbolic Logic'', 20, 151–163.</ref><ref name="moschovakis2010" />。

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

第654行：第654行：

# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（§5.7.3）。

−

* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"~~，而那正是不可判定的对角线问题。~~<ref name="rice1953" />

+

* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"，而那正是不可判定的对角线问题<ref name="rice1953">'''Rice, H. G. (1953).''' Classes of recursively enumerable sets and their decision problems. ''Transactions of the AMS'', 74, 358–366.【Rice 定理原始论文】【§6.5.1】</ref>.

'''注（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" />。

第672行：第672行：

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

−

* '''定理（Myhill 1955）'''：每个创造集都是 r.e.-完备的；两个概念重合<ref name="myhill1955" /><ref name="rogers1967" /><ref name="moschovakis2010" />.

+

* '''定理（Myhill 1955）'''：每个创造集都是 r.e.-完备的；两个概念重合<ref name="myhill1955">Myhill, J., & Shepherdson, J. C. (1955). Effective operations on partial recursive functions. ''Zeitschrift für mathematische Logik und Grundlagen der Mathematik'', 1, 310–317.</ref><ref name="rogers1967" /><ref name="moschovakis2010" />.

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

第694行：第694行：

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

−

'''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 [[Gödel-Löb 逻辑|GL]] 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑<ref name="solovay1976" /><ref name="moschovakis2010" />。

+

'''Solovay 定理（1976）'''：一个模态公式在 PA 的所有解释下都可证，当且仅当它是 [[Gödel-Löb 逻辑|GL]] 的定理。即 GL '''恰好'''完全刻画了 PA 的可证性逻辑<ref name="solovay1976">Solovay, R. M. (1976). Provability interpretations of modal logic. ''Israel Journal of Mathematics'', 25, 287–304.</ref><ref name="moschovakis2010" />。

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

Jake

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

3,094

个编辑