3,094
个编辑
更改
无编辑摘要
}}
}}
= Kleene 递归定理（Kleene's Recursion Theorems） =
> '''词条性质'''：可计算性理论（computability theory，研究"什么问题原则上可以被机械地计算"的学科）的核心定理
> '''提出者'''：Stephen Cole Kleene（斯蒂芬·科尔·克林，1909–1994，美国逻辑学家，Church 的学生，可计算性理论奠基人之一）
> '''首次发表'''：Kleene (1938), ''On Notation for Ordinal Numbers'', The Journal of Symbolic Logic 3(4): 150–155
> '''面向读者'''：具有物理、人工智能等理工科背景、但未系统学习过递归函数论的读者。文中所有术语和符号在第一次出现时均给出解释。
> '''引用体例'''：文中以〔作者 年份，页码/章节〕标注出处，完整文献信息见文末"参考文献"。
---
== 导言 ==
'''递归定理（recursion theorem）'''是递归函数论——即可计算性理论（computability theory，研究"什么问题原则上可以被机械地计算"的学科）——中的一组基本定理，由 Stephen Cole Kleene 提出，合称 '''Kleene 递归定理'''，包括两条：'''第一递归定理'''说，任何用递归方式定义的函数方程都有可计算的（最小）解——机械式的递归定义永远合法、永远有解；'''第二递归定理'''说，对任何可计算的全函数 f，总存在源程序 c，使得执行 c 与执行 f(c) 效果完全相同（<math>\phi_c = \phi_{f(c)}</math>）——程序可以合法地引用自己的代码。
'''递归定理（recursion theorem）'''是递归函数论——即可计算性理论（computability theory，研究"什么问题原则上可以被机械地计算"的学科）——中的一组基本定理，由 Stephen Cole Kleene 提出，合称 '''Kleene 递归定理'''，包括两条：'''第一递归定理'''说，任何用递归方式定义的函数方程都有可计算的（最小）解——机械式的递归定义永远合法、永远有解；'''第二递归定理'''说，对任何可计算的全函数 f，总存在源程序 c，使得执行 c 与执行 f(c) 效果完全相同（<math>\phi_c = \phi_{f(c)}</math>）——程序可以合法地引用自己的代码。
---
---
== 总览：两个定理各说了什么 ==
'''Kleene 递归定理'''是关于'''自指（self-reference，即一个系统"谈论"自身）'''与'''不动点（fixed point，即变换后保持不变的点）'''的两个基本定理的合称。先用日常语言各说一遍，再给出精确表述。
'''Kleene 递归定理'''是关于'''自指（self-reference，即一个系统"谈论"自身）'''与'''不动点（fixed point，即变换后保持不变的点）'''的两个基本定理的合称。先用日常语言各说一遍，再给出精确表述。
---
---
== 预备知识：读懂本词条所需的全部概念 ==
本节用程序员熟悉的语言解释文中会反复出现的五个概念。已经熟悉的读者可以跳过。
本节用程序员熟悉的语言解释文中会反复出现的五个概念。已经熟悉的读者可以跳过。
=== "可计算"与"部分函数" ===
'''可计算的（computable / effective / recursive）'''：一个函数是"可计算的"，意思是存在一套'''固定的、有穷的指令'''（程序），使得对任何输入，只要机械地按指令执行有穷多步，就能得到输出。"可计算的"（computable）、"有效的"（effective）、"递归的"（recursive）在本文中是同义词——这是历史造成的术语冗余，三个词来自 Church、Turing、Gödel–Kleene 三条等价的技术路线<ref name="kleene1938" />。
'''可计算的（computable / effective / recursive）'''：一个函数是"可计算的"，意思是存在一套'''固定的、有穷的指令'''（程序），使得对任何输入，只要机械地按指令执行有穷多步，就能得到输出。"可计算的"（computable）、"有效的"（effective）、"递归的"（recursive）在本文中是同义词——这是历史造成的术语冗余，三个词来自 Church、Turing、Gödel–Kleene 三条等价的技术路线<ref name="kleene1938" />。
'''记号 <math>\phi_e</math>'''：把全体程序（的所有可计算部分函数）排成一个序列，用自然数 0, 1, 2, <math>\ldots</math> 编号，'''<math>\phi_e</math> 表示"编号为 e 的程序所计算的那个部分函数"'''。这个编号也叫'''哥德尔数（Gödel number）'''：关键思想是"程序本身也是一个有限符号串，可以编码成一个自然数"，于是'''程序即数据'''——程序可以作为另一个程序的输入被处理。<math>\phi_e(x)</math> 表示"编号 e 的程序在输入 x 上的输出"（可能无定义）。本文中 p <math>\downarrow</math> 表示"程序 p 停机（有输出）"，p <math>\uparrow</math> 表示"不停机（无输出）"。
'''记号 <math>\phi_e</math>'''：把全体程序（的所有可计算部分函数）排成一个序列，用自然数 0, 1, 2, <math>\ldots</math> 编号，'''<math>\phi_e</math> 表示"编号为 e 的程序所计算的那个部分函数"'''。这个编号也叫'''哥德尔数（Gödel number）'''：关键思想是"程序本身也是一个有限符号串，可以编码成一个自然数"，于是'''程序即数据'''——程序可以作为另一个程序的输入被处理。<math>\phi_e(x)</math> 表示"编号 e 的程序在输入 x 上的输出"（可能无定义）。本文中 p <math>\downarrow</math> 表示"程序 p 停机（有输出）"，p <math>\uparrow</math> 表示"不停机（无输出）"。
=== 通用程序（解释器） ===
存在一台"通用机器"：给它输入 (e, x)，它就'''模拟'''编号 e 的程序在输入 x 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的通用图灵机是它的首个化身。用记号写就是：存在程序 i 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" />
存在一台"通用机器"：给它输入 (e, x)，它就'''模拟'''编号 e 的程序在输入 x 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的通用图灵机是它的首个化身。用记号写就是：存在程序 i 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" />
=== S-m-n 定理（柯里化 / 参数特化） ===
'''S-m-n 定理'''说：给定一个双输入程序和它的'''第一个输入'''，可以机械地生成一个"把第一个输入写死在程序里"的新单输入程序。用程序员的话说，就是'''柯里化（currying）或部分应用（partial application）总是可以机械完成的'''：存在可计算的全函数 S，使得
'''S-m-n 定理'''说：给定一个双输入程序和它的'''第一个输入'''，可以机械地生成一个"把第一个输入写死在程序里"的新单输入程序。用程序员的话说，就是'''柯里化（currying）或部分应用（partial application）总是可以机械完成的'''：存在可计算的全函数 S，使得
即"程序 S(e,y)"在输入 x 上的行为 = "程序 e"在输入 (y, x) 上的行为。Kleene 1938 年论文中的 S 函数就是这个工具<ref name="kleene1938" />。'''第二递归定理的证明只需要这一个工具'''，此外什么都不需要——这是它惊人简单的原因。
即"程序 S(e,y)"在输入 x 上的行为 = "程序 e"在输入 (y, x) 上的行为。Kleene 1938 年论文中的 S 函数就是这个工具<ref name="kleene1938" />。'''第二递归定理的证明只需要这一个工具'''，此外什么都不需要——这是它惊人简单的原因。
=== 递归可枚举集（r.e. set） ===
一个自然数集合称为'''递归可枚举的（recursively enumerable, r.e.）'''，如果存在一台机器能把它的元素'''一个一个地全部列出来'''（允许重复、允许乱序；不在集合里的元素永远不会被列出）。等价地，r.e. 集就是某个程序'''有定义的输入的集合'''（即 <math>\phi_e</math> 的定义域），记作 <math>W_e</math>。典型例子："所有会停机的 (程序,输入) 对"构成的集合（停机问题集合 K）是 r.e. 的，但它的补集不是——这正是"停机问题不可判定"的现代表述。
一个自然数集合称为'''递归可枚举的（recursively enumerable, r.e.）'''，如果存在一台机器能把它的元素'''一个一个地全部列出来'''（允许重复、允许乱序；不在集合里的元素永远不会被列出）。等价地，r.e. 集就是某个程序'''有定义的输入的集合'''（即 <math>\phi_e</math> 的定义域），记作 <math>W_e</math>。典型例子："所有会停机的 (程序,输入) 对"构成的集合（停机问题集合 K）是 r.e. 的，但它的补集不是——这正是"停机问题不可判定"的现代表述。
=== "不动点"的两种含义（重要！） ===
"不动点"在本文中出现于两个截然不同的层面，混淆它们是最常见的理解障碍：
"不动点"在本文中出现于两个截然不同的层面，混淆它们是最常见的理解障碍：
---
---
== 历史背景 ==
=== 起源：一篇研究"序数记号"的 6 页短文 ===
第二递归定理诞生于 Kleene 1938 年发表于《符号逻辑杂志》（''The Journal of Symbolic Logic''）的一篇仅 6 页的短文《论序数的记号》（''On Notation for Ordinal Numbers''）<ref name="kleene1938" />。这篇论文的主题表面上与"递归定理"毫不相干：
第二递归定理诞生于 Kleene 1938 年发表于《符号逻辑杂志》（''The Journal of Symbolic Logic''）的一篇仅 6 页的短文《论序数的记号》（''On Notation for Ordinal Numbers''）<ref name="kleene1938" />。这篇论文的主题表面上与"递归定理"毫不相干：
这个"小宝石"随即在论文 §3 被用于证明该文的主要结果：'''存在一个"通用"序数记号系统 <math>S_1</math>'''——任何其他合法记号系统能命名的序数，<math>S_1</math> 都能命名，且翻译过程本身是可计算的<ref name="kleene1938" />。这是"沿着序数逐层向上做递归定义"（后来称为'''有效超限递归'''，effective transfinite recursion）这一方法的首次应用。Kleene 由此构造出著名的'''记号系统 O（Kleene's O）'''，并证明存在最小的一个"不可命名"的序数——'''Church–Kleene 序数 <math>\omega_1^CK</math>'''，即可数序数中第一个无法被任何机械记号系统触及的序数<ref name="kleene1938" /><ref name="rogers1967" />。
这个"小宝石"随即在论文 §3 被用于证明该文的主要结果：'''存在一个"通用"序数记号系统 <math>S_1</math>'''——任何其他合法记号系统能命名的序数，<math>S_1</math> 都能命名，且翻译过程本身是可计算的<ref name="kleene1938" />。这是"沿着序数逐层向上做递归定义"（后来称为'''有效超限递归'''，effective transfinite recursion）这一方法的首次应用。Kleene 由此构造出著名的'''记号系统 O（Kleene's O）'''，并证明存在最小的一个"不可命名"的序数——'''Church–Kleene 序数 <math>\omega_1^CK</math>'''，即可数序数中第一个无法被任何机械记号系统触及的序数<ref name="kleene1938" /><ref name="rogers1967" />。
=== 命名史 ===
- '''Kleene 本人'''始终只叫它 '''"the recursion theorem"（递归定理）'''——即使在他 1952 年的《元数学导论》（''Introduction to Metamathematics''）中两个定理同时出现时，也未加区分<ref name="moschovakis2010" />。
- '''Kleene 本人'''始终只叫它 '''"the recursion theorem"（递归定理）'''——即使在他 1952 年的《元数学导论》（''Introduction to Metamathematics''）中两个定理同时出现时，也未加区分<ref name="moschovakis2010" />。
- 关于证明是怎么想到的：有学生曾问 Kleene，这个"短得可疑、巧得离谱"的两行证明从何而来，Kleene（也许是开玩笑地）回答说他只是'''"拿着 S-m-n 性质瞎鼓捣"'''（"fiddled around with (b)"）<ref name="moschovakis2010" />。Moschovakis 评论说，这种"鼓捣"很可能受到 <math>\lambda</math> 演算（Church 与 Kleene 此前共同发展的形式系统）中类似对角线构造的启发〔同上〕。
- 关于证明是怎么想到的：有学生曾问 Kleene，这个"短得可疑、巧得离谱"的两行证明从何而来，Kleene（也许是开玩笑地）回答说他只是'''"拿着 S-m-n 性质瞎鼓捣"'''（"fiddled around with (b)"）<ref name="moschovakis2010" />。Moschovakis 评论说，这种"鼓捣"很可能受到 <math>\lambda</math> 演算（Church 与 Kleene 此前共同发展的形式系统）中类似对角线构造的启发〔同上〕。
=== 一个值得铭记的教训 ===
1944 年，Kleene 曾'''错误地'''宣称他构造的记号集 O 具有较低的逻辑复杂度（属于 <math>\Pi^0_2</math> 类），因为他把第二递归定理给出的'''某一个'''不动点，误当作了归纳定义所要求的'''最小'''不动点。事实上 O 的复杂度要高得多（<math>\Pi^1_1</math>-完备），Kleene 直到 1955 年才纠正<ref name="moschovakis2010" />。这个故事最生动地说明了：'''第二递归定理只保证"给你一个不动点"，不保证给你"最小/最特殊的那个"'''——这正是它区别于第一递归定理的关键（见 4.4 与 6.6）。
1944 年，Kleene 曾'''错误地'''宣称他构造的记号集 O 具有较低的逻辑复杂度（属于 <math>\Pi^0_2</math> 类），因为他把第二递归定理给出的'''某一个'''不动点，误当作了归纳定义所要求的'''最小'''不动点。事实上 O 的复杂度要高得多（<math>\Pi^1_1</math>-完备），Kleene 直到 1955 年才纠正<ref name="moschovakis2010" />。这个故事最生动地说明了：'''第二递归定理只保证"给你一个不动点"，不保证给你"最小/最特殊的那个"'''——这正是它区别于第一递归定理的关键（见 4.4 与 6.6）。
---
---
== 第一递归定理（FRT） ==
=== 从"递归定义的函数"说起 ===
编程中最自然的定义方式是'''递归'''：定义阶乘时写 `fac(n) = n * fac(n-1)`，等号右边出现了正在定义的函数自己。抽象地看，这类定义都在解一个"函数方程"：
编程中最自然的定义方式是'''递归'''：定义阶乘时写 `fac(n) = n * fac(n-1)`，等号右边出现了正在定义的函数自己。抽象地看，这类定义都在解一个"函数方程"：
第一递归定理问的是：'''什么样的 <math>\Psi</math> 能保证方程 <math>\phi = \Psi(\phi)</math> 有解，而且解是可计算的？'''
第一递归定理问的是：'''什么样的 <math>\Psi</math> 能保证方程 <math>\phi = \Psi(\phi)</math> 有解，而且解是可计算的？'''
=== 定理表述 ===
'''定义（可计算的变换规则）'''：如果变换 <math>\Psi</math> 满足下面两条，就称它是'''递归算子（recursive operator）'''：
'''定义（可计算的变换规则）'''：如果变换 <math>\Psi</math> 满足下面两条，就称它是'''递归算子（recursive operator）'''：
'''例子'''：方程组 <math>\phi(1) = 2</math>，<math>\phi(2x) = 2</math><math>\phi(x)</math> 对应一个递归算子，其最小不动点是：<math>\phi(x) = x</math>（当 x 是 2 的幂），其余输入无定义。注意"最小性"自动处理了定义不完整的分支——机器在"非 2 的幂"上自然发散。<ref name="rogers1967" />
'''例子'''：方程组 <math>\phi(1) = 2</math>，<math>\phi(2x) = 2</math><math>\phi(x)</math> 对应一个递归算子，其最小不动点是：<math>\phi(x) = x</math>（当 x 是 2 的幂），其余输入无定义。注意"最小性"自动处理了定义不完整的分支——机器在"非 2 的幂"上自然发散。<ref name="rogers1967" />
=== 意义：递归定义的"存在性定理" ===
第一递归定理的角色，类似于分析学中用不动点定理（如 Banach 压缩映像原理）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定义递归函数时无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比集合论中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''Church–Turing 论题'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。
第一递归定理的角色，类似于分析学中用不动点定理（如 Banach 压缩映像原理）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定义递归函数时无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比集合论中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''Church–Turing 论题'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。
数学血统上，它是 '''Knaster–Tarski 不动点定理'''（序理论中"完备格上的单调映射必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。
数学血统上，它是 '''Knaster–Tarski 不动点定理'''（序理论中"完备格上的单调映射必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。
=== 与第二递归定理的关系 ===
Rogers 证明了：'''第二递归定理（强）蕴含第一递归定理（弱）'''——存在统一的机械方法，把"函数层面的不动点问题"翻译成"代码层面的不动点问题"，并且翻译后得到的不动点恰好是'''最小'''的<ref name="rogers1967" />。反过来不成立：第五、六节中第二递归定理的应用几乎都无法由第一递归定理得到。因此两者中'''第二递归定理更基本、更强大'''<ref name="rogers1967" />。
Rogers 证明了：'''第二递归定理（强）蕴含第一递归定理（弱）'''——存在统一的机械方法，把"函数层面的不动点问题"翻译成"代码层面的不动点问题"，并且翻译后得到的不动点恰好是'''最小'''的<ref name="rogers1967" />。反过来不成立：第五、六节中第二递归定理的应用几乎都无法由第一递归定理得到。因此两者中'''第二递归定理更基本、更强大'''<ref name="rogers1967" />。
---
---
== 第二递归定理（SRT）——本文重点 ==
=== 三种等价表述 ===
'''表述 A（Kleene 原始形式，1938）'''：对任意可计算的部分函数 <math>\psi(z, x)</math>，存在编号 f 使得对所有 x：
'''表述 A（Kleene 原始形式，1938）'''：对任意可计算的部分函数 <math>\psi(z, x)</math>，存在编号 f 使得对所有 x：
'''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 y——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 e 的程序在参数 y 下的行为"。那么存在一个可计算的全函数 z：你输入 y，它就输出针对这个参数的不动点编号 z(y)，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 x 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 y 给出不同的编号（z 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />
'''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 y——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 e 的程序在参数 y 下的行为"。那么存在一个可计算的全函数 z：你输入 y，它就输出针对这个参数的不动点编号 z(y)，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 x 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 y 给出不同的编号（z 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />
=== 推论：SRT 衍生出的若干重要结果 ===
> SRT 不是孤岛，但也不能把整片大陆都记在它名下。本节收录三条'''真正以 SRT 为证明枢纽'''的结果——它们的证明都必经 SRT，称"推论"名副其实：
> SRT 不是孤岛，但也不能把整片大陆都记在它名下。本节收录三条'''真正以 SRT 为证明枢纽'''的结果——它们的证明都必经 SRT，称"推论"名副其实：
> 常被误归为 SRT 推论的 '''Rice 定理'''与 '''Rice-Shapiro 定理'''不在此列：Rice 的教科书证明是停机归约（对角线矛盾），Rice-Shapiro 是"有限可生成"的结构定理，两者都不依赖 SRT（SRT 至多为 Rice 提供一条事后捷径）。它们属于 r.e. '''索引集理论'''，与 SRT 的关系是"同源，但独立"——因此移至 §6.5，与真正依赖 SRT 的 Myhill 定理并置，以对照这两种不同关系。
> 常被误归为 SRT 推论的 '''Rice 定理'''与 '''Rice-Shapiro 定理'''不在此列：Rice 的教科书证明是停机归约（对角线矛盾），Rice-Shapiro 是"有限可生成"的结构定理，两者都不依赖 SRT（SRT 至多为 Rice 提供一条事后捷径）。它们属于 r.e. '''索引集理论'''，与 SRT 的关系是"同源，但独立"——因此移至 §6.5，与真正依赖 SRT 的 Myhill 定理并置，以对照这两种不同关系。
==== Smullyan 双递归定理（1959, 1961） ====
'''SRT 的联立推广'''：对任意两个全可计算函数 g, h（不一定全），存在两个程序 m, n 使得
'''SRT 的联立推广'''：对任意两个全可计算函数 g, h（不一定全），存在两个程序 m, n 使得
双递归定理是后续许多重要构造的核心：① §6.3 介绍的"两层超算术构造"里，Spector 定理需要同时构造两个互相缠绕的函数；②Myhill-Shepherdson 定理（§6.6 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③某些停机问题的"相对化"证明也走双递归路线。<ref name="smullyan1961" /><ref name="rogers1967" />
双递归定理是后续许多重要构造的核心：① §6.3 介绍的"两层超算术构造"里，Spector 定理需要同时构造两个互相缠绕的函数；②Myhill-Shepherdson 定理（§6.6 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③某些停机问题的"相对化"证明也走双递归路线。<ref name="smullyan1961" /><ref name="rogers1967" />
==== Rogers 同构定理（1958） ====
任意两个'''通用程序枚举'''（即枚举出所有可计算函数的程序编号系统，详见 §2.2；下称 <math>\phi</math> 系统与 <math>\psi</math> 系统）之间，必然存在一个'''可计算同构''' <math>\rho</math>：<math>\mathbb{N} \to \mathbb{N}</math>——一部双向都可计算的"翻译词典"，把 <math>\phi</math> 系统里的每个程序号 e 送到 <math>\psi</math> 系统里的程序号 <math>\rho(e)</math>，并且 '''保 <math>\phi</math> 等价'''、'''保 W 等价'''。这两个"保…等价"头回见到有点吓人，其实只是说：这部词典'''不改变任何行为事实'''。逐个拆开看：
任意两个'''通用程序枚举'''（即枚举出所有可计算函数的程序编号系统，详见 §2.2；下称 <math>\phi</math> 系统与 <math>\psi</math> 系统）之间，必然存在一个'''可计算同构''' <math>\rho</math>：<math>\mathbb{N} \to \mathbb{N}</math>——一部双向都可计算的"翻译词典"，把 <math>\phi</math> 系统里的每个程序号 e 送到 <math>\psi</math> 系统里的程序号 <math>\rho(e)</math>，并且 '''保 <math>\phi</math> 等价'''、'''保 W 等价'''。这两个"保…等价"头回见到有点吓人，其实只是说：这部词典'''不改变任何行为事实'''。逐个拆开看：
证明思路：把"取 f(c) = 在另一编号系统下对应于 c 的程序编号"作为变换规则，对它套 SRT 得到不动点 c——c 就是翻译词典的种子；之后逐条验证它保 <math>\phi</math>、W 等价性。Rogers 同构定理常被引用作"程序编号系统的选择不影响可计算性理论"的根据——你可以挑任何合理的编号方式，得出的可计算性结论都一样。<ref name="rogers1967" />
证明思路：把"取 f(c) = 在另一编号系统下对应于 c 的程序编号"作为变换规则，对它套 SRT 得到不动点 c——c 就是翻译词典的种子；之后逐条验证它保 <math>\phi</math>、W 等价性。Rogers 同构定理常被引用作"程序编号系统的选择不影响可计算性理论"的根据——你可以挑任何合理的编号方式，得出的可计算性结论都一样。<ref name="rogers1967" />
==== Arslanov 完全性判据（1981） ====
'''SRT 的相对化版本所给出的等价刻画'''：r.e. 集合 C 称为 r.e.-'''完全'''，当且仅当满足下面这一性质：
'''SRT 的相对化版本所给出的等价刻画'''：r.e. 集合 C 称为 r.e.-'''完全'''，当且仅当满足下面这一性质：
Arslanov 判据在递归论里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"PA 不一致"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"。<ref name="arslanov1981" /><ref name="soare1987" />
Arslanov 判据在递归论里是教科书级工具：①用于证明 Gödel 不完备定理的算术陈述（"PA 不一致"这种陈述）的相对可计算性与停机问题同构；② 用于证明某些 r.e. 集"不可能被简化"。<ref name="arslanov1981" /><ref name="soare1987" />
=== 证明：一行对角线 ===
以表述 A 为例，全部证明如下。函数 <math>\psi(S(y, y), x)</math> 是可计算的（它只是把 §2.3 的柯里化操作 S 和 <math>\psi</math> 复合起来），所以它有编号，设为 e。令 '''f = S(e, e)'''，则对任何输入 x：
以表述 A 为例，全部证明如下。函数 <math>\psi(S(y, y), x)</math> 是可计算的（它只是把 §2.3 的柯里化操作 S 和 <math>\psi</math> 复合起来），所以它有编号，设为 e。令 '''f = S(e, e)'''，则对任何输入 x：
'''图3'''：第二递归定理证明的三步拆解与对角线自应用的视觉化——核心动作就是让程序 e 在 S(e,e) 里"看见自己"，从而闭合循环。
'''图3'''：第二递归定理证明的三步拆解与对角线自应用的视觉化——核心动作就是让程序 e 在 S(e,e) 里"看见自己"，从而闭合循环。
==== 列表法（Cutland 1980）：把"对角线"画成一张表 ====
上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。Cutland 在《Computability》§2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。
上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。Cutland 在《Computability》§2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。
'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>E_k</math>，每格填 <math>\phi_\phi_i(j)</math>；主对角线（红圈）上的格子构成对角枚举 D。'''黄底 D 行'''：把对角线上的格子抽出，得到 D = (<math>\phi_\phi_0(0)</math>, <math>\phi_\phi_1(1)</math>, <math>\phi_\phi_2(2)</math>, <math>\ldots</math>)。*''D'' 行*''：把 f 套到 D 上得到 D'' = (<math>\phi_{f(\phi_0(0))}</math>, <math>\phi_{f(\phi_1(1))}</math>, <math>\ldots</math>)——可计算 <math>\Rightarrow </math>必是某行 <math>E_m</math>。'''绿框'''：取 k = m 撞上 <math>E_m</math>，得 <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>，再设 n = <math>\phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——f 的不动点。
'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>E_k</math>，每格填 <math>\phi_\phi_i(j)</math>；主对角线（红圈）上的格子构成对角枚举 D。'''黄底 D 行'''：把对角线上的格子抽出，得到 D = (<math>\phi_\phi_0(0)</math>, <math>\phi_\phi_1(1)</math>, <math>\phi_\phi_2(2)</math>, <math>\ldots</math>)。*''D'' 行*''：把 f 套到 D 上得到 D'' = (<math>\phi_{f(\phi_0(0))}</math>, <math>\phi_{f(\phi_1(1))}</math>, <math>\ldots</math>)——可计算 <math>\Rightarrow </math>必是某行 <math>E_m</math>。'''绿框'''：取 k = m 撞上 <math>E_m</math>，得 <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>，再设 n = <math>\phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——f 的不动点。
=== 直观图景：程序如何"谈论"自己的代码 ===
'''例 1（Quine，Python 版）'''〔示例取自 Wikipedia "Quine (computing)"；与 SRT 的关系见 Kiselyov, §2〕：所谓 '''quine''' 就是"打印出自己源代码的程序"。第二递归定理断言：这样的程序必然存在。下面这个 Python 程序就是教科书级的 quine——运行它，会原样打印出它自己的源码：
'''例 1（Quine，Python 版）'''〔示例取自 Wikipedia "Quine (computing)"；与 SRT 的关系见 Kiselyov, §2〕：所谓 '''quine''' 就是"打印出自己源代码的程序"。第二递归定理断言：这样的程序必然存在。下面这个 Python 程序就是教科书级的 quine——运行它，会原样打印出它自己的源码：
——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。
——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。
=== \lambda 演算视角：与 Y 组合子的关系 ===
<math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 F，YF = F(YF)，即 Y 直接生产出 F 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。
<math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 F，YF = F(YF)，即 Y 直接生产出 F 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。
这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。
这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。
=== 与其它不动点定理的关系 ===
SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的范畴论概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的不动点引理与 Lawvere 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的范畴论概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的不动点引理与 Lawvere 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
==== Gödel 不动点引理（对角引理） ====
对任何包含足够算术的递归可公理化理论 T，对 T 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 T 证 <math>\psi</math> ↔ <math>\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不可判定性三层）见 §5.7.4 的详述。
对任何包含足够算术的递归可公理化理论 T，对 T 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 T 证 <math>\psi</math> ↔ <math>\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（一致性、<math>\omega</math>-一致性、不可判定性三层）见 §5.7.4 的详述。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
==== Lawvere 不动点定理（1969） ====
这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''范畴论统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。
这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''范畴论统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。
'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容。<ref name="lawvere1969" />
'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容。<ref name="lawvere1969" />
=== 自指现象：SRT 的"自指"一面 ===
第二递归定理最直接、也最让人着迷的威力，是它'''一劳永逸地解释了"自指"现象为什么合法'''。但要先澄清一个容易混淆的关键点：这些里程碑可以从'''两个正交的维度'''来理解——
第二递归定理最直接、也最让人着迷的威力，是它'''一劳永逸地解释了"自指"现象为什么合法'''。但要先澄清一个容易混淆的关键点：这些里程碑可以从'''两个正交的维度'''来理解——
由此看清每个现象的双重身份：'''Turing 停机、Gödel 不完备'''在"风格"上是否定性自指（与 Cantor、Russell 同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；Cantor、Russell 活在纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
由此看清每个现象的双重身份：'''Turing 停机、Gödel 不完备'''在"风格"上是否定性自指（与 Cantor、Russell 同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；Cantor、Russell 活在纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
==== Cantor 对角线论证（1891） ====
'''现象'''：实数集不可数。假设每个实数都被编号 0, 1, 2, <math>\ldots</math>；定义一个新实数，令它的第 n 位小数与"编号 n 的实数"的第 n 位小数都不同。这个新实数不在原表里——矛盾。<ref name="cantor1891" />
'''现象'''：实数集不可数。假设每个实数都被编号 0, 1, 2, <math>\ldots</math>；定义一个新实数，令它的第 n 位小数与"编号 n 的实数"的第 n 位小数都不同。这个新实数不在原表里——矛盾。<ref name="cantor1891" />
'''与 SRT 的关系：同源，但独立'''。两者做了同一件事——取"第 i 个对象在第 i 个位置上的值"（对角线）：Cantor 取"第 i 个实数的第 i 位小数"，SRT 取"第 e 个程序在输入 e 上的值"<math>\phi_e(e)</math>（即证明里的 S(e, e)）。但'''方向相反'''：Cantor 取对角线后'''改动'''它，制造一个"不在表里"的对象，从而证明实数'''不可数'''；SRT 取对角线后'''固定'''它，得到一个"引用自己编号"的程序，从而证明自指程序'''存在'''。注意，SRT '''推不出''' Cantor 定理——SRT 的结论都活在"程序 / 可计算"的世界里，给不出"实数不可数"这种纯集合论命题；两者只是共享了同一个技巧。<ref name="cantor1891" /><ref name="moschovakis2010" />
'''与 SRT 的关系：同源，但独立'''。两者做了同一件事——取"第 i 个对象在第 i 个位置上的值"（对角线）：Cantor 取"第 i 个实数的第 i 位小数"，SRT 取"第 e 个程序在输入 e 上的值"<math>\phi_e(e)</math>（即证明里的 S(e, e)）。但'''方向相反'''：Cantor 取对角线后'''改动'''它，制造一个"不在表里"的对象，从而证明实数'''不可数'''；SRT 取对角线后'''固定'''它，得到一个"引用自己编号"的程序，从而证明自指程序'''存在'''。注意，SRT '''推不出''' Cantor 定理——SRT 的结论都活在"程序 / 可计算"的世界里，给不出"实数不可数"这种纯集合论命题；两者只是共享了同一个技巧。<ref name="cantor1891" /><ref name="moschovakis2010" />
==== Russell 悖论（1901） ====
'''现象'''：考虑 R = {x : x <math>\notin x</math>}（所有"不属于自己"的集合组成的集合）。问 R <math>\in R</math> 是否成立？若 R <math>\in R</math>，则按定义 R <math>\notin R</math>；若 R <math>\notin R</math>，则按定义 R <math>\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论。<ref name="russell1908" />
'''现象'''：考虑 R = {x : x <math>\notin x</math>}（所有"不属于自己"的集合组成的集合）。问 R <math>\in R</math> 是否成立？若 R <math>\in R</math>，则按定义 R <math>\notin R</math>；若 R <math>\notin R</math>，则按定义 R <math>\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论。<ref name="russell1908" />
'''与 SRT 的关系：同源，但独立'''。Russell 悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"e <math>\in W_e</math>"，就得到 K = {e : e <math>\notin W_e</math>}——K 可枚举、其补集不可枚举。而"K 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的 Russell 悖论"，但 Russell 悖论本身与 SRT 只是同源关系。<ref name="russell1908" /><ref name="rogers1967" />
'''与 SRT 的关系：同源，但独立'''。Russell 悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"e <math>\in W_e</math>"，就得到 K = {e : e <math>\notin W_e</math>}——K 可枚举、其补集不可枚举。而"K 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的 Russell 悖论"，但 Russell 悖论本身与 SRT 只是同源关系。<ref name="russell1908" /><ref name="rogers1967" />
==== Turing 停机问题（1936） ====
'''现象'''：不存在算法 H 能判定"任意程序 e 在任意输入 x 上是否会停机"。这是可计算性理论第一个、也是最著名的"不可判定"结果。<ref name="turing1936" />
'''现象'''：不存在算法 H 能判定"任意程序 e 在任意输入 x 上是否会停机"。这是可计算性理论第一个、也是最著名的"不可判定"结果。<ref name="turing1936" />
关键就在第 3 步：<math>\psi</math> 里用的是参数 z（可以正常定义），SRT 把它换成 f 自己——'''没有 SRT，"<math>\phi_f</math> 的行为取决于 H 对 f 的判决"就是非法循环定义，写不出来'''。SRT 的全部威力，就是把这种循环合法化：你只管把"自己"写成参数，存在性交给定理。<ref name="moschovakis2010" /><ref name="rogers1967" />
关键就在第 3 步：<math>\psi</math> 里用的是参数 z（可以正常定义），SRT 把它换成 f 自己——'''没有 SRT，"<math>\phi_f</math> 的行为取决于 H 对 f 的判决"就是非法循环定义，写不出来'''。SRT 的全部威力，就是把这种循环合法化：你只管把"自己"写成参数，存在性交给定理。<ref name="moschovakis2010" /><ref name="rogers1967" />
==== Gödel 第一不完备定理（1931） ====
'''现象'''：任何"足够强"的一致可公理化理论 T（例如 Peano 算术 PA）都不完备：存在一个句子 <math>\sigma</math>，使 T 既证不出 <math>\sigma</math>、也证不出 <math>\neg</math><math>\sigma</math>。<ref name="godel1931" />
'''现象'''：任何"足够强"的一致可公理化理论 T（例如 Peano 算术 PA）都不完备：存在一个句子 <math>\sigma</math>，使 T 既证不出 <math>\sigma</math>、也证不出 <math>\neg</math><math>\sigma</math>。<ref name="godel1931" />
Rogers 还讨论过一个反向的自指：可以构造一个公理系统，其中包含'''断言自身一致性'''的句子（对任何公理集 <math>W_p</math>，存在 n 使 <math>W_n = W_p</math> <math>\cup </math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含 PA，这个"自信"的系统反而不可能一致。<ref name="rogers1967" />
Rogers 还讨论过一个反向的自指：可以构造一个公理系统，其中包含'''断言自身一致性'''的句子（对任何公理集 <math>W_p</math>，存在 n 使 <math>W_n = W_p</math> <math>\cup </math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含 PA，这个"自信"的系统反而不可能一致。<ref name="rogers1967" />
==== von Neumann 自复制自动机（1948） ====
'''现象'''：存在能在物理上自我复制的自动机。von Neumann 在 Los Alamos 设计的方案含四部分：'''通用构造器 A'''（读入一段指令，构造出该指令描述的任何机器）、'''通用拷贝器 B'''（复制指令）、'''控制器 C'''（指挥 A 与 B 协同运作、并把指令传给新机器）、以及一段描述 A、B、C 三者如何组合的'''蓝图'''（即指令带）；机器 M = <math>\langle</math> A, B, C, 蓝图<math>\rangle</math> 启动后能造出 M 自己的副本。<ref name="vonneumann1966" /><ref name="lee1963" />
'''现象'''：存在能在物理上自我复制的自动机。von Neumann 在 Los Alamos 设计的方案含四部分：'''通用构造器 A'''（读入一段指令，构造出该指令描述的任何机器）、'''通用拷贝器 B'''（复制指令）、'''控制器 C'''（指挥 A 与 B 协同运作、并把指令传给新机器）、以及一段描述 A、B、C 三者如何组合的'''蓝图'''（即指令带）；机器 M = <math>\langle</math> A, B, C, 蓝图<math>\rangle</math> 启动后能造出 M 自己的副本。<ref name="vonneumann1966" /><ref name="lee1963" />
'''图4'''：自复制机的闭合回路——机器 M 的蓝图描述了 M 的全部部件（构造器 A、拷贝器 B、控制器 C）；启动后 A 读蓝图 <math>\to </math>造出 M 的新副本、B 复制蓝图、C 把它们组装起来。SRT 保证存在这样的蓝图，让有限指令即可闭合循环（驳斥了"蓝图之蓝图无穷倒退"的谬误）。
'''图4'''：自复制机的闭合回路——机器 M 的蓝图描述了 M 的全部部件（构造器 A、拷贝器 B、控制器 C）；启动后 A 读蓝图 <math>\to </math>造出 M 的新副本、B 复制蓝图、C 把它们组装起来。SRT 保证存在这样的蓝图，让有限指令即可闭合循环（驳斥了"蓝图之蓝图无穷倒退"的谬误）。
==== Quine（自打印程序） ====
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序。<ref name="wikipedia_quine_computing" />。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 Hofstadter 在《哥德尔、艾舍尔、巴赫》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979" />。
'''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序。<ref name="wikipedia_quine_computing" />。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 Hofstadter 在《哥德尔、艾舍尔、巴赫》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979" />。
也就是说，程序 c 的行为 = 打印出 c 自己——这正是 quine。所以 quine 就是"取 f = Print 程序、再套 SRT"的一行产物。Kiselyov 在分阶段 <math>\lambda</math> 演算里形式化地证明，quine、twine（两个程序互相打印对方）、trade 谜题都是 SRT 的不动点。<ref name="kiselyov" />
也就是说，程序 c 的行为 = 打印出 c 自己——这正是 quine。所以 quine 就是"取 f = Print 程序、再套 SRT"的一行产物。Kiselyov 在分阶段 <math>\lambda</math> 演算里形式化地证明，quine、twine（两个程序互相打印对方）、trade 谜题都是 SRT 的不动点。<ref name="kiselyov" />
==== 自省程序与自省式自改进程序 ====
'''自省程序（introspective program）'''：比 quine 强得多的自指——它能在运行时'''"看到"自身（或自身的有界近似），并据此修改、调整自己的行为'''。Lisp 的 `eval`、Python 的 `inspect`/反射、调试器、动态语言的元对象协议都是它的化身。
'''自省程序（introspective program）'''：比 quine 强得多的自指——它能在运行时'''"看到"自身（或自身的有界近似），并据此修改、调整自己的行为'''。Lisp 的 `eval`、Python 的 `inspect`/反射、调试器、动态语言的元对象协议都是它的化身。
---
---
== 其它应用：非自指构造 ==
上一节（§5.7）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造'''不涉及自指'''的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（有效超限递归）——把递归定义从自然数推广到序数，从而定义出越来越复杂的对象。本节即以它开篇（6.1–6.4）；此后转入其余主题（6.5–6.7）——注意 6.5 板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：
上一节（§5.7）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造'''不涉及自指'''的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（有效超限递归）——把递归定义从自然数推广到序数，从而定义出越来越复杂的对象。本节即以它开篇（6.1–6.4）；此后转入其余主题（6.5–6.7）——注意 6.5 板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：
> '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
> '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
=== 沿序数逐层构造之一：通用序数记号系统与 \omega_1^CK ===
这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：序数记号系统给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：序数记号系统给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。
Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。
=== 沿序数逐层构造之二：构造序数 = 递归序数 ===
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽。<ref name="moschovakis2010" />
这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽。<ref name="moschovakis2010" />
=== 沿序数逐层构造之三：超算术层级与 Spector 唯一性定理 ===
'''背景'''：这一段需要先铺垫三个概念。
'''背景'''：这一段需要先铺垫三个概念。
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 §5.2 的 Smullyan 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />
证明需要同时构造'''两个互相缠绕的函数'''（互相引用对方编号），由双递归定理（见 §5.2 的 Smullyan 版本）合法化——这是有效超限递归技术的高峰之一。Kleene 对这个学生的工作推崇备至，他常讲自己如何"行为不端"地接受它作为博士论文、又作为期刊编辑指定自己为审稿人并立即录用——"非常不合规矩，但我认为最终有利于逻辑！"<ref name="moschovakis2010" />
=== 沿序数逐层构造之四：HYP = \Delta^1_1 与有效描述集合论 ===
'''背景'''：在自然数的集合（数学分析的对象）上，可以用"二阶量化"分层：<math>\Sigma^1_1</math> 集是"存在一个实数使得某个可计算性质成立"的集合（存在投影），<math>\Pi^1_1</math> 是其对偶（全称），<math>\Delta^1_1 = \Sigma^1_1 \cap \Pi^1_1</math> 是"两面都可定义"的集合——可类比为分析学中"既可开逼近又可闭逼近"的集合。
'''背景'''：在自然数的集合（数学分析的对象）上，可以用"二阶量化"分层：<math>\Sigma^1_1</math> 集是"存在一个实数使得某个可计算性质成立"的集合（存在投影），<math>\Pi^1_1</math> 是其对偶（全称），<math>\Delta^1_1 = \Sigma^1_1 \cap \Pi^1_1</math> 是"两面都可定义"的集合——可类比为分析学中"既可开逼近又可闭逼近"的集合。
此外，Kleene 1940 年代为直觉主义数学（拒绝排中律的构造性数学）构造的'''可实现性（realizability）'''解释中，bar 递归定义、bar 归纳与连续性原理的验证也本质地使用 SRT 的各种形式<ref name="moschovakis2010" />。
此外，Kleene 1940 年代为直觉主义数学（拒绝排中律的构造性数学）构造的'''可实现性（realizability）'''解释中，bar 递归定义、bar 归纳与连续性原理的验证也本质地使用 SRT 的各种形式<ref name="moschovakis2010" />。
=== r.e. 索引集理论：Rice、Rice-Shapiro 与 Myhill ===
本板块把"程序行为性质"当作一个独立的研究对象。核心概念是'''索引集（index set）'''：给定某类程序行为，把"行为落在这类里"的全部程序编号收集起来，就得到 <math>\mathbb{N}</math> 的一个子集。若用程序 e 的定义域 <math>W_e</math>（§2.4）来编码行为、用 <math>\mathcal{A}</math> 表示某类 r.e. 集，则写法是
本板块把"程序行为性质"当作一个独立的研究对象。核心概念是'''索引集（index set）'''：给定某类程序行为，把"行为落在这类里"的全部程序编号收集起来，就得到 <math>\mathbb{N}</math> 的一个子集。若用程序 e 的定义域 <math>W_e</math>（§2.4）来编码行为、用 <math>\mathcal{A}</math> 表示某类 r.e. 集，则写法是
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 6.5.3）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 §5.2 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。
与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 6.5.3）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 §5.2 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。
==== Rice 定理（1951） ====
'''陈述'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 A = { e : <math>\phi_e \in \mathcal{A}</math> } 不是可计算集（更不是递归集）。
'''陈述'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 A = { e : <math>\phi_e \in \mathcal{A}</math> } 不是可计算集（更不是递归集）。
> '''注（SRT 捷径，非本质）'''：Rice 定理也可用 SRT 三行证完：设 A 可计算，取变换规则 f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 m 使 <math>\phi_m = \phi_{f(m)}</math>。若 m <math>\in A</math>，则 f(m) <math>\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；m <math>\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制。<ref name="rogers1967" />
> '''注（SRT 捷径，非本质）'''：Rice 定理也可用 SRT 三行证完：设 A 可计算，取变换规则 f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 m 使 <math>\phi_m = \phi_{f(m)}</math>。若 m <math>\in A</math>，则 f(m) <math>\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；m <math>\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制。<ref name="rogers1967" />
==== Rice-Shapiro 定理（1956） ====
Rice 定理回答"'''能否'''判定"；Rice-Shapiro 定理进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
Rice 定理回答"'''能否'''判定"；Rice-Shapiro 定理进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
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" />
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 定理：创造集 = 完备集 ====
'''背景'''：停机问题集合 K = {e : 程序 e 在输入 e 上停机} 是 r.e. 集中"最不可判定"的——任何 r.e. 集都能通过可计算的翻译归约到它（称为 '''r.e.-完备'''，complete）。另有一个看似完全不同的概念：一个 r.e. 集 A 称为'''创造集（creative set）'''，如果它的补集是"能系统地生产反例"的——存在一个可计算程序，你给它任何与 A 不交的 r.e. 集，它都能吐出一个既不在 A 里也不在那个集合里的元素。创造性是 Post 1944 年为刻画"不可判定的源泉"而引入的概念。
'''背景'''：停机问题集合 K = {e : 程序 e 在输入 e 上停机} 是 r.e. 集中"最不可判定"的——任何 r.e. 集都能通过可计算的翻译归约到它（称为 '''r.e.-完备'''，complete）。另有一个看似完全不同的概念：一个 r.e. 集 A 称为'''创造集（creative set）'''，如果它的补集是"能系统地生产反例"的——存在一个可计算程序，你给它任何与 A 不交的 r.e. 集，它都能吐出一个既不在 A 里也不在那个集合里的元素。创造性是 Post 1944 年为刻画"不可判定的源泉"而引入的概念。
'''证明中 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" />。
'''证明中 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" />。
=== 有效运算的连续性：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> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：
'''背景'''：一个"程序变换"<math>\Phi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Phi(\phi)</math>。有两种实现方式：'''按代码操作'''（给 <math>\Phi</math> 输入 <math>\phi</math> 的程序编号，让它随便分析代码——类似"按名调用"）与'''按值操作'''（<math>\Phi</math> 只能查询 <math>\phi</math> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：
此外，Rogers 用 SRT 证明了 '''Blum 定理'''：任意两个"通用部分函数"（即解释器）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一。<ref name="rogers1967" />
此外，Rogers 用 SRT 证明了 '''Blum 定理'''：任意两个"通用部分函数"（即解释器）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一。<ref name="rogers1967" />
=== Solovay 可证性逻辑 ===
'''背景'''：'''可证性逻辑（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。模态逻辑系统 '''GL'''（Gödel–Löb 逻辑）是候选公理系统。
'''背景'''：'''可证性逻辑（provability logic）'''研究"可证"这个概念的抽象规律，把 "⌜<math>\phi</math>⌝ 在 PA 中可证" 抽象为模态算子 □<math>\phi</math>。模态逻辑系统 '''GL'''（Gödel–Löb 逻辑）是候选公理系统。
Solovay 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。
Solovay 的证明漫长精巧，其关键引理需要构造一个'''自指的'''函数 h——h 的定义中引用 h 自己的编号。Solovay 本人用一句话带过："表面上的循环用递归定理以通常方式处理"<ref name="moschovakis2010" />。Moschovakis 评论：无法想象不借助 SRT 如何凭空想出这个构造——在此意义上 SRT 是可证性逻辑这块基石中不可或缺的成分<ref name="moschovakis2010" />。
=== 应用地图一览 ===
|领域|代表性结果|SRT 的角色|
|领域|代表性结果|SRT 的角色|
---
---
== 评注与影响 ==
1. '''简单性与普适性的反差'''。SRT 的全部证明只有一行对角线，应用却横跨逻辑学几乎所有分支。Moschovakis 指出：其广泛适用性恰恰'''源于'''这种简单——它极易被翻译到自然数以外的语境（实数空间、任意 Polish 空间、高类型对象、模态逻辑），在每个语境中重新化身<ref name="moschovakis2010" />。
1. '''简单性与普适性的反差'''。SRT 的全部证明只有一行对角线，应用却横跨逻辑学几乎所有分支。Moschovakis 指出：其广泛适用性恰恰'''源于'''这种简单——它极易被翻译到自然数以外的语境（实数空间、任意 Polish 空间、高类型对象、模态逻辑），在每个语境中重新化身<ref name="moschovakis2010" />。