| 第157行： |
第157行： |
| | | | |
| | Moschovakis 还给出了一个'''统一形式'''：把"变换规则"同时允许依赖于"函数的编号"和"函数的值"，所得不动点定理在两种极端情形下分别退化为第二递归定理（不依赖函数值）和第一递归定理（不依赖编号）<ref name="moschovakis2010" />。 | | Moschovakis 还给出了一个'''统一形式'''：把"变换规则"同时允许依赖于"函数的编号"和"函数的值"，所得不动点定理在两种极端情形下分别退化为第二递归定理（不依赖函数值）和第一递归定理（不依赖编号）<ref name="moschovakis2010" />。 |
| − |
| |
| − | == 第二递归定理（SRT） ==
| |
| − |
| |
| − | === 三种等价表述 ===
| |
| − |
| |
| − | '''表述 A（Kleene 原始形式，1938）'''：对任意可计算的部分函数 <math>\psi(z, x)</math>，存在编号 <math>f</math> 使得对所有 <math>x</math>：
| |
| − |
| |
| − | : <math>\phi_f(x) = \psi(f, x)</math>
| |
| − |
| |
| − | 即：'''存在一个程序 <math>f</math>，它在输入 <math>x</math> 上的行为，恰好等于"把 <math>f</math> 自己的编号当作第一个参数喂给 <math>\psi</math>"的行为。''' 程序 <math>f</math> 在某种意义上"知道自己的代码"<ref name="kleene1938" />。
| |
| − |
| |
| − |
| |
| − | '''表述 B（Rogers 不动点形式，1967）'''：对任意可计算的'''全'''函数 <math>f</math>（程序变换规则），存在编号 <math>n</math> 使得：
| |
| − |
| |
| − | : <math>\phi_n = \phi_{f(n)}</math>
| |
| − |
| |
| − | 这是 Rogers 的原话——"''Let f be any recursive function; then there exists an n such that <math>\phi_n = \phi_{f(n)}</math>.''"<ref name="rogers1967" />。意思是：<math>f</math> 拿着程序 <math>n</math> 的源代码算出一个新程序 <math>f(n)</math>，而'''新程序与旧程序计算的是同一个函数'''。<ref name="rogers1967" />
| |
| − |
| |
| − |
| |
| − | '''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 <math>y</math>——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 <math>e</math> 的程序在参数 <math>y</math> 下的行为"。那么存在一个可计算的全函数 <math>z</math>：你输入 <math>y</math>，它就输出针对这个参数的不动点编号 <math>z(y)</math>，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 <math>x</math> 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 <math>y</math> 给出不同的编号（<math>z</math> 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />
| |
| − |
| |
| − | === 推论：SRT 衍生出的若干重要结果 ===
| |
| − |
| |
| − | SRT 不是孤岛，但也不能把整片大陆都记在它名下。本节收录三条'''真正以 SRT 为证明枢纽'''的结果——它们的证明都必经 SRT，称"推论"名副其实：
| |
| − |
| |
| − | * '''[[Smullyan 双递归定理]]'''——SRT 的"联立化"推广：一次造出两个互相引用对方代码的程序（可推广到 <math>k</math> 个），是后续许多构造的通用工具；
| |
| − | * '''[[Rogers 同构定理]]'''——SRT 的"编号[[独立性 (数学)|独立性]]"推论：任意两个[[通用图灵机|通用程序]]枚举之间必有保结构的可计算同构；
| |
| − | * '''[[Arslanov 完全性判据]]'''——相对化 SRT 的"刻画性"等价定理：一个 r.e. 集何时是 [[r.e.-完备的]]。
| |
| − |
| |
| − | ==== Smullyan 双递归定理（1959, 1961） ====
| |
| − |
| |
| − | '''SRT 的联立推广'''：对任意两个全可计算函数 <math>g</math>, <math>h</math>（不一定全），存在两个程序 <math>m, n</math> 使得
| |
| − |
| |
| − | : <math>
| |
| − | \phi_m(x) = g(\langle m, n\rangle, x)\\
| |
| − | \phi_n(x) = h(\langle m, n\rangle, x)
| |
| − | </math>
| |
| − |
| |
| − | ——两个程序可以'''互相引用对方的代码'''。这是 SRT 的"二元推广"，可直接由 SRT 套用：
| |
| − |
| |
| − | # 先用 s-m-n（§2.3）构造两个可计算函数 <math>\psi_1(x) = g(S(x, x), x)</math>、<math>\psi_2(x) = h(S(x, x), x)</math>，二者均依赖自身编号；
| |
| − | # 对 <math>\psi_1</math> 套 SRT 拿到不动点 <math>m</math>；
| |
| − | # <math>m</math> 唯一确定后，<math>n</math> 由 <math>\phi_n = \psi_2(m)</math> 的不动点结构给出。
| |
| − |
| |
| − | 推广到 <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">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§5.2.1】</ref><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> 系统里的每个程序号 <math>e</math> 送到 <math>\psi</math> 系统里的程序号 <math>\rho(e)</math>，并且 '''保 <math>\phi</math> 等价'''、'''保 W 等价'''。这两个"保…等价"是说：这部词典'''不改变任何行为事实'''。逐个拆开看：
| |
| − |
| |
| − | * '''<math>\phi</math> 等价'''：同一编号系统内，若两个程序 <math>e_1</math>、<math>e_2</math> 计算的是同一个（部分）函数（<math>\phi_{e_1} = \phi_{e_2}</math>，§2.1），就说它们 '''<math>\phi</math> 等价'''——编号只是程序的外衣，算出的函数才是实质。
| |
| − | * '''保 <math>\phi</math> 等价'''：要求对每个程序号 <math>e</math> 成立 <math>\phi_e = \psi_{\rho(e)}</math>：<math>e</math> 在 <math>\phi</math> 系统里算什么函数，<math>\rho(e)</math> 在 <math>\psi</math> 系统里就算同一个函数。于是"算同一函数"的程序对，翻译后依然是"算同一函数"的对。
| |
| − | * '''W 等价 / 保 W 等价'''：<math>W_e</math> 是程序 <math>e</math> 的定义域——会让它停机的输入集合（§2.4）。两个程序 '''W 等价'''指 <math>W_{e_1} = W_{e_2}</math>（接受的输入一模一样）；'''保 W 等价'''指翻译也不破坏这层对应。由于词条约定 <math>W_e = dom(\phi_e)</math>，"保 <math>\phi</math>"已自动带出"保 W"；Rogers 原版把两层并列，是因为他的框架允许"函数枚举"与"r.e. 集枚举"彼此独立（§6.5 索引集的 <math>\mathcal{A}</math> 用的正是独立于 <math>\phi</math> 的 W 层）。
| |
| − |
| |
| − | 直觉上：两个不同的程序编号系统乍看像不同的语言（一个把 quine 编号成 42，另一个编号成 100），但实质上说的是同一类对象；Rogers 定理说它们之间必有可计算的"翻译词典"，且词典严格保结构。
| |
| − |
| |
| − | 证明思路：把"取 <math>f(c)</math> = 在另一编号系统下对应于 <math>c</math> 的程序编号"作为变换规则，对它套 SRT 得到不动点 <math>c</math>——<math>c</math> 就是翻译词典的种子；之后逐条验证它保 <math>\phi</math>、W 等价性。[[#Rogers 同构定理（1958）|Rogers 同构定理]]常被引用作"程序编号系统的选择不影响可计算性理论"的根据——你可以挑任何合理的编号方式，得出的可计算性结论都一样<ref name="rogers1967" />。
| |
| − |
| |
| − | ==== Arslanov 完全性判据（1981） ====
| |
| − |
| |
| − | '''SRT 的相对化版本所给出的等价刻画'''：r.e. 集合 C 称为 r.e.-'''完全'''，当且仅当满足下面这一性质：
| |
| − |
| |
| − | * 对每个 r.e. 集合 <math>W</math>，存在一个可计算函数 <math>f_W</math> 使得 <math>W\leq_T C</math> 通过 <math>f_W</math>
| |
| − |
| |
| − | 这里一下子出现了三个新名字，先逐个解释：
| |
| − |
| |
| − | * '''r.e. 集合'''：见 §2.4。本词条统一用缩写 r.e.（recursively enumerable，[[递归可枚举集|递归可枚举]]）。
| |
| − | * '''r.e.-完全'''：r.e. 集合这个"复杂度类别"里"最硬核"的一档——任何别的 r.e. 集合 <math>W</math> 都能机械地归约到 <math>C</math>，判定"<math>W</math> 含 <math>x</math>"等价于"问 <math>C</math>"。
| |
| − | * '''Turing 归约 / <math>W\leq_T C</math> 通过 <math>f_W</math>'''：<math>A</math> 能 '''Turing 归约'''到 <math>B</math>（记 <math>A\leq_T B</math>），意思是"只要允许把 <math>B</math> 当'''神谕机（oracle，下一条解释）'''——可以向它提任意多个 yes/no 问题并瞬时得到回答——<math>A</math> 就能被判定"。等式 <math>W\leq_T C</math> 通过 <math>f_W</math> 即"编排提问方式的过程由可计算函数 <math>f_W</math> 给出，它把 <math>x</math> 改写成若干个向 <math>C</math> 的查询并综合出答案"。
| |
| − |
| |
| − | 直觉上：[[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">'''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">'''Soare, R. I. (1987).''' ''Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets''. Berlin: Springer-Verlag.【r.e. 集与图灵度的标准教科书；Arslanov 完备性判据（§5.2.3）与 Rice–Shapiro 等索引集定理（§6.5）的教科书出处】</ref>
| |
| − | 。
| |
| − |
| |
| − | === 证明：一行对角线 ===
| |
| − |
| |
| − | 以表述 A 为例，全部证明如下。函数 <math>\psi(S(y, y), x)</math> 是可计算的（它只是把 §2.3 的[[柯里化操作]] <math>S</math> 和 <math>\psi</math> 复合起来），所以它有编号，设为 <math>e</math>。令 '''<math>f = S(e, e)</math>'''，则对任何输入 <math>x</math>：
| |
| − |
| |
| − | : <math>\phi_f(x) = \phi_{S(e,e)}(x) = \phi_e(e, x) = \psi(S(e,e), x) = \psi(f, x)</math> ∎
| |
| − |
| |
| − | 第一步是 <math>f</math> 的定义；第二步是柯里化的定义（<math>S(e,e)</math> 就是"把 <math>e</math> 的第一个输入写死为 <math>e</math>"）；第三步是 <math>e</math> 的定义；第四步再回到 <math>f</math> 的定义。'''唯一实质操作是第三步前那个自应用 <math>S(e,e)</math>：让程序 <math>e</math> 作用于自己的编号。''' 这就是[[对角线论证|对角线方法]]——与 Cantor 证明实数不可数、Gödel 构造"本句不可证"、Turing 证明停机问题不可解是同一种技术<ref name="kleene1938" /><ref name="rogers1967" />。
| |
| − | [[文件:对角线证明.png|替代=对角线证明|缩略图|图3：第二递归定理证明的三步拆解与对角线自应用的视觉化——核心动作就是让程序 e 在 S(e,e) 里"看见自己"，从而闭合循环。]]
| |
| − |
| |
| − | ==== 列表法（Cutland 1980）：把"对角线"画成一张表 ====
| |
| − |
| |
| − | 上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。[[奈杰尔·卡特兰|Cutland]] 在《Computability》<ref name="cutland1980"/> §2.3 (Theorem 2.3) 给出过一种更直观的列表法证明，用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上。三步走。
| |
| − |
| |
| − | * '''1. 把"所有可计算函数的枚举"摆成一张表'''
| |
| − |
| |
| − | 按 §2.2，每个可计算部分函数都有一个编号；所有这种编号的全体记作 <math>\{\phi_k\}</math>。对任意"枚举函数" <math>E</math>（把一列编号映射成一列可计算函数），<math>E</math> 的第 <math>n</math> 项就是 <math>\phi_{E(n)}</math>，即"编号为 <math>E(n)</math> 的程序"。现在考虑所有"可计算函数的枚举"——它们每一个都是某个可计算函数 <math>h</math>。Cutland 把它们自身也排成一张表：用编号为 <math>k</math> 的程序 <math>\phi_k</math> 自己去枚举，得到
| |
| − |
| |
| − | : <math>E_k</math> = "以 <math>\phi_k</math> 为枚举函数的那种枚举"，即 <math>E_k</math> 的第 <math>n</math> 项 = <math>\phi_{\phi_k(n)}</math>
| |
| − |
| |
| − | ——双重编号 <math>\phi_{\phi_k(n)}</math>。把 <math>E_0</math>、<math>E_1</math>、<math>E_2</math>、<math>\ldots</math> 并排写下来就是一张二维表（图 6 的上半部）：每行 <math>E_k</math> 是一个枚举、每列 <math>n</math> 是"该行第 <math>n</math> 个值"、每格是某个具体的可计算函数。这张表把"枚举可计算函数的所有方式"完整地、不重不漏地列了出来。
| |
| − |
| |
| − | * '''2. 对角线枚举<math>D</math>'''
| |
| − |
| |
| − | 把这张表沿主对角线的格子圈出来——它们正是
| |
| − |
| |
| − | : <math>D = (\phi_{\phi_0(0)}, \phi_{\phi_1(1)}, \phi_{\phi_2(2)},\ldots)</math>
| |
| − |
| |
| − | <math>D</math> 仍然是一个可计算的枚举：由 <math>h(x) = \phi_x(x)</math> 给出（图 6 黄底一行的"沿主对角线"）。它满足一个关键性质：
| |
| − |
| |
| − | : <math>D</math> 和每行 <math>E_k</math> 都共享一项：第 <math>(k+1)</math> 项都是 <math>\phi_{\phi_k(k)}</math>
| |
| − |
| |
| − | ——因为 <math>E_k</math> 的第 <math>(k+1)</math> 项 = <math>\phi_{\phi_k(k)}</math>，而 <math>D</math> 的第 <math>(k+1)</math> 项 = <math>\phi_{\phi_k(k)}</math>，两者恰好对得上（图 6 右侧红字注释）。
| |
| − |
| |
| − | * '''3. 沿 <math>D</math> 把 <math>f</math> 套进去，得到 <math>f</math> 的不动点'''
| |
| − |
| |
| − | 设 <math>f</math> 是任意全可计算函数。沿 <math>D</math> 的每一项先用 <math>f</math> 变一下号，再去取对应的可计算函数，得到另一个枚举：
| |
| − |
| |
| − | : <math>D^* = (\phi_{f(\phi_0(0))},\phi_{f(\phi_1(1))}, \phi_{f(\phi_2(2))},\ldots)</math>
| |
| − |
| |
| − | <math>D^*</math> 也可计算（由 <math>f(h(x))</math> 给出）——既然 <math>D^*</math> 本身也是"枚举可计算函数"的一种方式，它必然是表里某一行 <math>E_m</math>。这正是循环闭合的地方：套用 <math>f</math> 之后，必然撞回表内。
| |
| − |
| |
| − | 取 <math>k = m：D^* =E_m</math>，所以 <math>D^*</math> 的第 <math>(m+1)</math> 项 = <math>E_m</math> 的第 <math>(m+1)</math> 项 = <math>\phi_{\phi_m(m)}</math>。而 <math>D^*</math> 的第 <math>(m+1)</math> 项由定义也是 <math>\phi_{f(\phi_m(m))}</math>：
| |
| − |
| |
| − | * '''4. <math>\phi_{\phi_m(m)} = \phi_{f(\phi_m(m))}</math>'''
| |
| − |
| |
| − | Cutland 用 Lemma 2.1 把"第 <math>m</math> 行"调整成全的（即 <math>\phi_m</math> 是全函数），所以 <math>\phi_m(m)</math> 是一个良定的自然数 <math>n</math>。设 n = <math>\phi_m(m)</math>：
| |
| − |
| |
| − | : <math>\phi_n = \phi_{f(n)}</math>
| |
| − |
| |
| − | <math>n</math> 就是 <math>f</math> 的不动点 ∎<ref name="cutland1980">'''Cutland, N. J. (1980).''' ''Computability: An Introduction to Recursive Function Theory''. Cambridge University Press.【§1.9 定理 1.9 给出 totally <math>\psi</math>-introspective 程序的原始定义与存在性证明——"自省程序"概念的最早明确出处（§5.7.7）；§2.3 定理 2.3 给出 SRT 的"列表法"证明（§5.3.1）】</ref>.
| |
| − |
| |
| − | '''与"一行证明"的关系'''：§5.3 的证明把表上 <math>D^* = E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——<math>h(x) = \phi_x(x)</math> 对应"<math>e </math>= 编号(<math>\psi(S(y,y), x)</math>)"，<math>S(e,e)</math> 就是用自应用把表上的对角线点亮；列表法只是把这一行在表格里完整地展开。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——每行 <math>E_k</math> 都被对角线穿一格，循环天然闭合。
| |
| − | [[文件:列表法证明.png|无|'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0, E_1, E_2, \cdots, E_k</math>，每格填 <math>\phi_{\phi_i(j)}</math>；主对角线（红圈）上的格子构成对角枚举 <math>D</math>。'''黄底 <math>D</math> 行'''：把对角线上的格子抽出，得到 <math>D = (\phi_{\phi_0(0)}, \phi_{\phi_1(1)}, \phi_{\phi_2(2)}, \ldots)</math>。'''<math>D^*</math> 行'''：把 <math>f</math> 套到 <math>D</math> 上得到 <math>D^* = (\phi_{f(\phi_0(0))}, \phi_{f(\phi_1(1))}, \ldots)</math>——可计算 <math>\Rightarrow</math> 必是某行 <math>E_m</math>。'''绿框'''：取 <math>k = m</math> 撞上 <math>E_m</math>，得 <math>\phi_{\phi_m(m)} = \phi_{f(\phi_m(m))}</math>，再设 <math>n = \phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——<math>f</math> 的不动点。|缩略图|800x800像素]]
| |
| − |
| |
| − | === 直观图景：程序如何"谈论"自己的代码 ===
| |
| − |
| |
| − | '''例 1（Quine，Python 版）'''〔示例取自 Wikipedia "Quine (computing)"<ref name="wikipedia_quine_computing" />；与 SRT 的关系见 Kiselyov<ref name="kiselyov"/>, §2〕：所谓 '''quine''' 就是"打印出自己源代码的程序"。第二递归定理断言：这样的程序必然存在。下面这个 Python 程序就是教科书级的 quine——运行它，会原样打印出它自己的源码：
| |
| − |
| |
| − | <syntaxhighlight lang="python3">
| |
| − | c = 'c = %r; print(c %% c)'; print(c % c)
| |
| − | </syntaxhighlight>
| |
| − |
| |
| − | 它的机制很简洁：字符串 `c` 本身是一个"打印模板"——`%r` 会带上引号打印出 c 自己的内容，`%%` 是格式化转义符（输出为单个 `%`）。于是 `print(c % c)` 打印出的结果，恰好就是这个程序的全部源码。'''程序把自己的源码当作数据、再把它打印出来'''——这正是第二递归定理"程序合法地引用自己的代码"在程序语言里的最小实现<ref name="wikipedia_quine_computing" /><ref name="kiselyov" />。
| |
| − |
| |
| − | '''把 Print 换成任意可计算操作 f：quine 是 SRT 在 f = Print 上的特例'''。上面那个 quine 里的 `print(c % c)` 可以立刻换成'''任意可计算操作'''。看下面这个程序——它不再"打印自己"，而是"先把自己的源码施加一个变换 f、再打印结果"（这里 f = "给每一行加上行号"）：
| |
| − |
| |
| − | <syntaxhighlight lang="python3">
| |
| − | def f(s):
| |
| − | return '\n'.join(f'{i:2d}: {line}'
| |
| − | for i, line in enumerate(s.split('\n'), 1))
| |
| − |
| |
| − | c = '''def f(s):
| |
| − | return '\\n'.join(f'{i:2d}: {line}'
| |
| − | for i, line in enumerate(s.split('\\n'), 1))
| |
| − | src = %r
| |
| − | print(f(src % src))'''
| |
| − | print(f(c % c))
| |
| − | </syntaxhighlight>
| |
| − |
| |
| − | `c % c` 仍然是"自己的源码"，但最后一行不再是 `print(c % c)`，而是 `print(f(src % src))`——也就是先调用 f 处理自己的源码、再打印结果。这个程序满足：c 的行为 = "对 c 的源码施加 f、再打印"的行为。
| |
| − |
| |
| − | ——用公式写就是 <math>\phi_c = \phi_{f(c)}</math>（<math>\phi_c</math> 是程序 <math>c</math> 当作可计算函数看时的整体行为）。把上面那个 <math>f</math> 换成别的——比如"统计字符数"、"对源码求 SHA-256（一种密码学中的哈希函数）"、"把字符串大写"、"把源码上传到某服务器"、"什么都不做只返回自己"——只要 <math>f</math> 是可计算的全函数，'''满足 <math>\phi_c = \phi_{f(c)}</math> 的不动点程序 <math>c</math> 就必然存在'''。这正是 SRT 所承诺的内容：quine 是 SRT 在 <math>f =</math> "Print" 这一个特例上的推论，SRT 则是 quine 在 <math>f =</math> "任意全可计算函数"上的推广。Kiselyov 在分阶段 <math>\lambda</math> 演算里把这一观察形式化为"quine = f = id 的不动点、twine（两程序互相打印对方）= f = 另一程序编号映射的不动点、trade 谜题 = f = 投影函数对的不动点"<ref name="kiselyov" />。
| |
| − |
| |
| − | '''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 §5.3 那一行证明——给定 <math>f</math>，构造 <math>\psi(x) = \phi_{S(x,x)}</math>（其中 <math>S</math> 把 <math>f</math> 与"自应用"组合起来），取 <math>e</math> 满足 <math>\phi_e = \psi</math>，再对 <math>\psi</math> 套 SRT 取不动点——会发现它和 quine 是'''同一种构造'''，差别只在目的（执行层面 vs 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：
| |
| − |
| |
| − | {| class="wikitable"
| |
| − | |-
| |
| − | !
| |
| − | ! '''quine 的自指'''
| |
| − | ! '''SRT 证明的自指'''
| |
| − | |-
| |
| − | | '''自指的载体'''
| |
| − | | 字符串 <math>c</math>（程序的源码）
| |
| − | | 编号 <math>e</math>（程序在 <math>\phi</math> 枚举里的下标）
| |
| − | |-
| |
| − | | '''载体在哪里被引用'''
| |
| − | | `print(c % c)` 把 c 嵌入 print 的实参
| |
| − | | <math>\psi(x) = \phi_{S(x,x)}</math> 把 <math>e</math> 作为通用函数的下标
| |
| − | |-
| |
| − | | '''构造方向'''
| |
| − | | 先有具体 <math>f</math>（= Print），再造 <math>c</math>（<math>c</math> 的代码里嵌入 <math>f</math> 的引用）
| |
| − | | 先有具体 <math>f</math>（§5.3 假设中任意一个），再造 <math>c</math>（<math>c</math> 由对 <math>f</math> 套 SRT 得到）
| |
| − | |-
| |
| − | | '''目的'''
| |
| − | | 让 <math>c</math> 的输出 = <math>c</math> 的源码
| |
| − | | 让 <math>\phi_c</math> 等价于 <math>\phi_{f(c)}</math>
| |
| − | |-
| |
| − | | '''得到什么'''
| |
| − | | 一个具体程序（<math>f =</math> Print 时的不动点）
| |
| − | | 一个具体程序（这个 <math>f</math> 的不动点 <math>c</math>），且这个 <math>c</math> '''依赖 <math>f</math>'''（不同 <math>f</math> 给出不同 <math>c</math>）
| |
| − | |}
| |
| − |
| |
| − | 也就是说，'''SRT 证明与 quine 不是"互逆"，而是同构'''——两者都是"先有一个具体的全可计算函数 <math>f</math>、再造一个不动点程序 <math>c</math> 满足 <math>\phi_c = \phi_{f(c)}</math>"。SRT 真正比 quine 强的地方只有一点：'''它证明了"先有 <math>f</math>、再造 <math>c</math>"这种构造对所有全可计算 <math>f</math> 都成立'''，而 quine 只演示了 <math>f =</math> Print 一个特例；SRT 给的不是"一个程序"，而是"对每个 <math>f</math> 都有一个程序（<math>f</math> 的不动点 <math>c</math>）"这样的普遍性陈述。这也解释了为何 SRT 在可计算性文献中被称为"second recursion theorem"——它把"quine 这种特例的构造手法"摆到了"自指可计算函数的普遍刻画"这一位置，把 quine 从"程序员的奇技"升格为"任何合理程序系统都封不住自指"的元定理。
| |
| − |
| |
| − | '''例 2（自我命名的集合）'''<ref name="rogers1967" />：是否存在程序 <math>n</math>，它所列出的集合恰好是单点集 <math>\{n\}</math>——'''一个枚举出自己编号的程序'''？直觉上这像是编号系统的"巧合"，但取变换规则 <math>f</math> 使得"程序 <math>f(x)</math> 恰好输出单点集 <math>\{x\}</math>"（这样的 <math>f</math> 显然可构造），应用表述 B 即得 <math>\phi_n = \phi_{f(n)}</math>，即 <math>W_n = \{n\}</math>。而且这个结论对'''任何合理的程序编号系统都成立'''——它不是编号的巧合，而是编号的必然。
| |
| − |
| |
| − | '''自指的机制'''（Rogers 的精辟分析）<ref name="rogers1967" />：不动点程序 <math>n</math> 作为一段指令，'''并不包含它自身的全文'''（这不可能，句子不能比自身还长），而是包含'''一份"如何重建自身"的配方'''——"先算出我的代码，再执行它"。这与 Gödel 在证明不完备定理时发明的"替换函数"（substitution function，把一个公式的编号代入公式自身）是同一种机制。自然语言中的对应物是这个短语：
| |
| − |
| |
| − | "the result of substituting 'the result of substituting "x" in "x"' in 'the result of substituting "x" in "x"'"
| |
| − | （把 "把 x 代入 x 的结果" 代入 "把 x 代入 x 的结果" 所得到的结果）
| |
| − |
| |
| − | ——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。
| |
| − |
| |
| − | === λ演算视角：与 Y 组合子的关系 ===
| |
| − |
| |
| − | <math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 <math>F</math>，<math>YF = F(YF)</math>，即 <math>Y</math> 直接生产出 <math>F</math> 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。
| |
| − |
| |
| − | Kiselyov 在'''分阶段 <math>\lambda</math> 演算'''（staged lambda-calculus，区分"代码"与"值"两个阶段的现代元编程框架）中重构了第二递归定理，得出一个漂亮的结论：'''第二递归定理就是 Y 组合子的"带代码"推广'''——[[Y组合子]]给出函数层面的不动点，SRT 给出"程序 + 自身代码"层面的不动点；当把"代码"取为平凡编码（程序即自身）时，SRT 的构造精确退化为 Y 组合子<ref name="kiselyov" />。
| |
| − |
| |
| − | 这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。
| |
| − |
| |
| − | === 与其它不动点定理的关系 ===
| |
| − |
| |
| − | SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。
| |
| − |
| |
| − | ==== Gödel 不动点引理（对角引理） ====
| |
| − |
| |
| − | 对任何包含足够算术的递归可公理化理论 <math>T</math>，对 <math>T</math> 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 <math>T</math> 可证 <math>\psi\iff\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（[[一致性]]、[[ω-一致性]]、[[不可判定性]]三层）见 §5.7.4 的详述。
| |
| − |
| |
| − | 注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。
| |
| − |
| |
| − | ==== [[Lawvere 不动点定理]]（1969） ====
| |
| − |
| |
| − | 这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''[[范畴论]]统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。
| |
| − |
| |
| − | '''[[Lawvere定理]]（标准陈述）'''：设 '''<math>C</math>''' 是一个 ''[[Cartesian 闭范畴]]''（Cartesian closed category，"对象 = 数据类型、[[态射]] = 数据类型间可计算变换、函数空间本身也是对象、可以反复变换"的信息世界）。设 '''<math>F: C \to C</math>''' 是一个[[函子]]（"世界内部的一种自我变换"）。如果存在一个'''满射态射'''（surjective morphism，形象地说"覆盖了 <math>F(A)</math> 的全部出口"）
| |
| − |
| |
| − | : <math>f: A \to F(A)</math> （每个 <math>F(A)</math> 元素都被 <math>f</math> 的像源元素覆写）
| |
| − |
| |
| − | 那么对'''任意'''态射 <math>g: F(A)\to A</math>，都存在一个不动物 <math>x: A\to A</math>，使得
| |
| − |
| |
| − | : <math> F(x) \circ f = g \circ f</math>
| |
| − |
| |
| − | 即顺着"<math>A\to F(A) \to A</math>"这条回路绕一圈，既可以按 <math>g</math> 走、也可以按 <math>F(x)</math> 走，'''两条路径等价'''。
| |
| − |
| |
| − | '''直观解读'''：所谓"自指世界"，就是那种'''函数空间可以作为自身参数来研究'''的地方（Cartesian 闭）。在这种世界里，只要有一个"程序能撞出比自己更复杂的结果"的接口（[[满射]]态射），'''任何"全局选择函数"（<math>g</math>）都必有不动物'''——你的 <math>g</math> 想要把世界再次变换回自己，总会撞到某个无法再造新东西的点（<math>x</math>），而那个点正好让变换等于"再变换一次"（<math>F(x) = g</math>）。"自指 <math>\to </math>不动点"在这种世界里是不可避免的结构——不论那世界是自然数 + 可计算函数（Turing、Kleene），还是形式系统 + 可证性（Gödel），还是集合论宇宙（Russell、Cantor）。
| |
| − |
| |
| − | '''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是：
| |
| − |
| |
| − | {| class="wikitable"
| |
| − | |-
| |
| − | ! Lawvere 抽象成分
| |
| − | ! SRT 实例化
| |
| − | |-
| |
| − | | Cartesian 闭范畴 <math>C</math>
| |
| − | | 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi:\mathbb{N}^k\rightarrow\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴）
| |
| − | |-
| |
| − | | 函子 <math>F</math>
| |
| − | | 适当选取（<math>C</math> 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 <math>F</math> 取作"按编号 <math>e</math> 取 <math>\phi_e</math>" 的函子
| |
| − | |-
| |
| − | | 满射态射 <math>f: A\to F(A)</math>
| |
| − | | 取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）
| |
| − | |-
| |
| − | | 任意态射 <math>g: F(A)\to A</math>
| |
| − | | 取 <math>g =</math> SRT 推论里那个'''给定的全可计算函数 <math>f</math>'''（"按它编程序"）。注意：SRT 表述要求 <math>f:\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"<math>f</math> 处处有定义"这一约束，保证 <math>g</math> 在 <math>F(A)</math> 的全部范围内都有意义。
| |
| − | |-
| |
| − | | 不动物 <math>x: A\to A</math>
| |
| − | | 正是 SRT 给出的那个'''不动点编号 <math>c</math>'''——它满足 <math>F(c) \circ f = g \circ f</math>，即 <math>\phi_c = \phi_{f(c)}</math>
| |
| − | |}
| |
| − |
| |
| − | '''关系定性'''：
| |
| − |
| |
| − | * [[#Lawvere 不动点定理（1969）|Lawvere 不动点定理]]'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）；
| |
| − | * Lawvere 也不仅是 SRT 的"更高层次表述"（它是数学基础层面的定理，把 SRT、[[#Gödel 不动点引理（对角引理）|Gödel 不动点引理]]、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同侧面'''）；
| |
| − | * 因此应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。
| |
| − |
| |
| − | '''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[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与自指===
| |
| − |
| |
| − | 第二递归定理最直接、也最让人着迷的威力，是它'''一劳永逸地解释了"自指"现象为什么合法'''。但要先澄清一个容易混淆的关键点：这些里程碑可以从'''两个正交的维度'''来理解——
| |
| − |
| |
| − | * '''结论的性质'''：是"否定性"（证否某物不存在：Cantor、Russell、Turing、Gödel），还是"肯定性"（证实自指对象存在：自复制、quine、SRT 本身）；
| |
| − | * '''结论活在哪个世界'''：纯集合论（SRT不适用），还是程序 / 可计算世界（可以用SRT）。
| |
| − |
| |
| − | 两个维度交叉，得到下表：
| |
| − |
| |
| − | {| class="wikitable"
| |
| − | |-
| |
| − | !
| |
| − | ! '''否定性结论'''（证否某物）
| |
| − | ! '''肯定性结论'''（证实某物存在）
| |
| − | |-
| |
| − | | '''纯集合论'''（SRT不适用）
| |
| − | | [[康托尔论证实数不可数]]、[[罗素悖论]]
| |
| − | | （无）
| |
| − | |-
| |
| − | | '''程序 / 可计算'''（可以用SRT）
| |
| − | | '''[[图灵停机问题]]、[[哥德尔不完备定理]]'''
| |
| − | | [[冯诺伊曼自复制自动机]]、[[quine程序]]、[[自省程序]]、SRT 本身
| |
| − | |}
| |
| − |
| |
| − | 由此看清每个现象的双重身份：'''[[图灵停机问题]]、[[哥德尔不完备定理]]'''在"风格"上是否定性自指（与 [[康托尔不可数问题]]、[[罗素悖论]]同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；康托尔不可数问题、罗素悖论位于纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
| |
| − |
| |
| − | ==== 康托尔对角线论证（1891） ====
| |
| − |
| |
| − | '''现象'''：实数集不可数。假设每个实数都被编号 <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">'''Moschovakis, Y. N. (2010).''' Kleene's amazing second recursion theorem. ''The Bulletin of Symbolic Logic'', 16(2), 189–239.【18 个应用的权威综述；本文应用部分的章节编号均指此文】</ref>。
| |
| − |
| |
| − | ==== 罗素悖论（1901） ====
| |
| − |
| |
| − | '''现象'''：考虑 <math>R = \{x : x \notin x\}</math>（所有"不属于自己"的集合组成的集合）。问 <math>R\in R</math> 是否成立？若 <math>R\in R</math>，则按定义 <math>R\notin R</math>；若 <math>R\notin R</math>，则按定义 <math>R\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论<ref name="russell1908">'''Russell, B. (1908).''' Mathematical logic as based on the theory of types. ''American Journal of Mathematics'', 30, 222–262.【罗素悖论的现代陈述】</ref>。
| |
| − |
| |
| − | '''与 SRT 的关系：同源，但独立'''。罗素悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"<math>e\in W_e</math>"，就得到 <math>K = \{e : e\notin W_e\}</math>——<math>K</math> 可枚举、其补集不可枚举。而"<math>K</math> 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的罗素悖论"，但罗素悖论本身与SRT只是同源关系。<ref name="russell1908" /><ref name="rogers1967" />
| |
| − |
| |
| − | ==== 图灵停机问题（1936） ====
| |
| − |
| |
| − | '''现象'''：不存在算法 <math>H</math> 能判定"任意程序 <math>e</math> 在任意输入 <math>x</math> 上是否会停机"。这是可计算性理论第一个、也是最著名的"不可判定"结果<ref name="turing1936">'''Turing, A. M. (1936).''' On computable numbers, with an application to the Entscheidungsproblem. ''Proceedings of the London Mathematical Society'', 42, 230–265.【停机问题不可判定】</ref>.
| |
| − |
| |
| − | '''双重身份'''：停机不可判定在'''结论性质'''上是否定性的（证明"判定器不存在"），与康托尔、罗素问题同类；但因为它活在"程序"世界，'''又能被 SRT 推出'''。下面展示完整的"套用"过程——这是所有例子里最干净的一个，最能看清 SRT 到底在哪里发力。
| |
| − |
| |
| − | '''套用 SRT 造否定性自指程序的完整演示'''：
| |
| − |
| |
| − | # '''假设'''存在判定器 <math>H</math>（<math>H(e,x)=1</math> 表示"程序 <math>e</math> 在输入 <math>x</math> 停机"，<math>=0</math> 表示不停机）。
| |
| − | # '''写出"想要的行为"，把"自己"写成参数 <math>z</math>'''：我们要一个与 <math>H</math> 唱反调的捣乱程序——"如果 <math>H</math> 说程序 <math>z</math>（在输入 <math>z</math> 上）会停机，我就死循环；如果 <math>H</math> 说不停机，我就立即停机"。写成可计算规则：<math>\psi(z, x) = \text{若} H(z, z) = 1，\text{则发散（死循环）；若} H(z, z) = 0，\text{则输出0（立即停机）。}</math>
| |
| − | # '''套 SRT'''：存在编号 f，使 <math>\phi_f(x) = \psi(f, x)</math>。SRT 在这一步把参数 <math>z</math> 换成了 <math>f</math> 自己，循环闭合：<math>\phi_f(x) = \text{若} H(f, f) = 1，\text{则发散；若 }H(f, f) = 0\text{，则输出 0。}</math>
| |
| − | # '''代入 <math>x = f</math> 制造矛盾'''：若 <math>H(f,f)=1</math>（<math>H</math> 说"<math>f</math> 在输入 <math>f</math> 停机"），但此时 <math>\phi_f(f)</math> 发散——<math>H</math> 判错；若 <math>H(f,f)=0</math>（<math>H</math> 说不停机），但此时 <math>\phi_f(f)=0</math> 停机——<math>H</math> 又判错。于是 <math>H</math> 无论如何都错 <math>\to </math>'''<math>H</math> 不存在'''。∎
| |
| − |
| |
| − | 关键就在第 3 步：<math>\psi</math> 里用的是参数 <math>z</math>（可以正常定义），SRT 把它换成 <math>f</math> 自己——'''没有 SRT，"<math>\phi_f</math> 的行为取决于 <math>H</math> 对 <math>f</math> 的判决"就是非法循环定义，写不出来'''。SRT 的全部威力，就是把这种循环合法化：你只管把"自己"写成参数，存在性交给定理<ref name="moschovakis2010" /><ref name="rogers1967" />。
| |
| − |
| |
| − | ==== 哥德尔第一不完备定理（1931） ====
| |
| − |
| |
| − | '''现象'''：任何"足够强"的一致可公理化理论 <math>T</math>（例如 [[皮亚诺公理|Peano 算术]]，简写为PA）都不完备：存在一个句子 <math>\sigma</math>，使 <math>T</math> 既证不出 <math>\sigma</math>、也证不出 <math>\neg\sigma</math><ref name="godel1931">'''Gödel, K. (1931).''' Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. ''Monatshefte für Mathematik und Physik'', 38, 173–198.【Gödel 不完备定理（Gödel 不动点引理是其核心证明工具，见 §5.6.1）】【§5.7.4】</ref>。
| |
| − |
| |
| − | '''术语——皮亚诺算术（PA）与 [[罗宾孙算术]]（Q）'''：'''PA''' 是 '''Peano 算术（Peano Arithmetic）'''的缩写，是'''一阶算术的标准公理系统'''，用于形式化刻画自然数（<math>0, 1, 2, \ldots</math>）及其加法、乘法。它由意大利数学家皮亚诺（G. Peano（1889））的公理发展而来，包含：①常元 0；②后继运算 <math>S</math>（每个数有唯一后继，0 不是任何数的后继，后继相同则原数相同）；③加法、乘法的递归定义；④'''归纳公理模式'''（induction schema：对任何一阶公式 <math>\phi</math>，若 <math>\phi(0)</math> 成立、且 <math>\phi(n) \Rightarrow \phi(n+1)</math>，则 <math>\phi</math> 对一切自然数成立）。PA 是哥德尔不完备定理的典型对象——它足够强（能在内部编码所有初等数论），又是可公理化的一致理论。而 '''Q（[[罗宾孙算术]]）'''是皮亚诺算术的一个'''弱化'''：保留①—③、去掉归纳公理模式，只留极有限的几条公理，是"足以推出不完备定理的最弱理论"之一（后文 [[Myhill定理]]即用它）。
| |
| − |
| |
| − | '''双重身份'''：与停机问题一样，哥德尔不完备在结论上是否定性的（证明"完备一致的理论不存在"）；哥德尔在1931的原证明走的是康托尔/罗素的否定性对角线老路、'''并不依赖 SRT'''。但因为它活在"形式系统可证性"这一可计算的世界，事后也能被 SRT 干净地推出。核心是'''不动点引理（Fixed Point Lemma）'''，它是 SRT 最纯粹形式的直接推论：
| |
| − |
| |
| − | * '''不动点引理'''：设 <math>T</math> 是任何足够强的可公理化理论，则对任何含一个自由变量的公式 <math>\theta(v)</math>，都存在句子 <math>\sigma</math>，使 <math>T</math> 可证 "<math>\sigma\iff\theta</math>(⌜<math>\sigma</math>⌝)"（⌜<math>\sigma</math>⌝ 是 <math>\sigma</math> 的哥德尔数）。即：'''任何性质 <math>\theta</math>，都存在一个句子 <math>\sigma</math>，在 <math>T</math> 可证的意义下恰好谈论"自己是否具有 <math>\theta</math>"'''<ref name="moschovakis2010" />。
| |
| − |
| |
| − | * 证明：取 <math>\theta(v)</math> = "<math>v</math> 不可证"，由不动点引理得 <math>\sigma\iff\text{"}\sigma\text{不可证"}</math>。若<math>\sigma</math> 可证，则它说的是真话（我不可证），矛盾；若 <math>\neg\sigma</math> 可证，则"<math>\sigma</math> 可证"，又矛盾。于是 <math>\sigma</math> 与 <math>\neg\sigma</math> 都不可证——第一不完备定理成立。把 <math>\theta</math> 换成 [[J. Barkley Rosser|Rosser]] 的精巧变体，还能去掉"<math>\omega</math>-一致性"这个额外假设，得到 '''Rosser 强化'''<ref name="godel1931" /><ref name="moschovakis2010" />。
| |
| − |
| |
| − | * '''[[Myhill定理]]（1955）'''：[[罗宾逊算术]] Q 的任何一致、可公理化扩张 <math>T</math>，其定理集都是'''[[创造集]]'''（见 §6.5.3），从而是 r.e.-完备的<ref name="moschovakis2010" />.
| |
| − |
| |
| − | 合起来我们可以得到一个惊人结论：'''所有'''足够强的一致公理化理论（皮亚诺算术、[[ZFC公理系统]]<math>\ldots\ldots</math>）都自动满足不动点引理的条件，因而都不完备、不可判定；而且任意两个这样的理论，其定理集在递归同构意义下完全相同<ref name="moschovakis2010" />。
| |
| − |
| |
| − | Rogers 还讨论过一个反向的自指：可以构造一个公理系统，其中包含'''断言自身一致性'''的句子（对任何公理集 <math>W_p</math>，存在 <math>n</math> 使 <math>W_n = W_p\cup</math>{⌜<math>W_n</math> 一致⌝}）。但 Gödel '''第二'''不完备定理说明：若 <math>W_p</math> 已含皮亚诺算术，这个"自信"的系统反而不可能一致<ref name="rogers1967" />。
| |
| − |
| |
| − | ==== [[冯诺伊曼]]的[[自复制自动机]]（1948） ====
| |
| − |
| |
| − | '''现象'''：存在能在物理上[[自复制自动机]]。[[冯诺伊曼]]在[[洛斯阿拉莫斯实验室]]设计的自动机方案含四部分：'''通用构造器 A'''（读入一段指令，构造出该指令描述的任何机器）、'''通用拷贝器 B'''（复制指令）、'''控制器 C'''（指挥 A 与 B 协同运作、并把指令传给新机器）、以及一段描述 A、B、C 三者如何组合的'''蓝图'''（即指令带）；机器 M<math> = \langle</math> A, B, C, 蓝图<math>\rangle</math> 启动后能造出 M 自己的副本<ref name="vonneumann1966">'''von Neumann, J. (1966).''' ''Theory of Self-Reproducing Automata'' (A. W. Burks 编). University of Illinois Press.【自复制自动机的奠基性设计（原稿始于 1948）】【§5.7.5】<ref name="lee1963">'''Lee, C. Y. (1963).''' A Turing machine which prints its own tape. ''Mathematical Tables and Other Aids to Computation'', 17, 403–406.【Rogers 1967 §11.4 第三图示的直接启发】</ref>。
| |
| − |
| |
| − | '''SRT 如何推出它'''：
| |
| − |
| |
| − | * '''定理（自复制图灵机）'''：存在一台[[图灵机]]，从空白纸带出发，停机时纸带上恰好写着'''它自己的完整描述（转移表）'''<ref name="moschovakis2010" />。
| |
| − |
| |
| − | * 证明思路是 SRT 的典型用法：定义 <math>\psi(z)</math> = "把编号 <math>z</math> 的机器的描述打印出来"——一个完全机械、与"谁被打印"无关的变换。SRT 给出不动点 <math>f</math>：程序 <math>f</math> 的行为 = 打印 <math>f</math> 自己的描述。循环凭空闭合。
| |
| − |
| |
| − | Rogers 给出更一般的框架：'''只要存在一台"通用建造机"（即 von Neumann 的 A 的抽象——给蓝图就造机器），就必存在一台机器，无论输入什么都造出自己的副本'''<ref name="rogers1967" />。这直接驳倒了"自复制不可能"的谬误论证（"复制需要蓝图，蓝图又需要蓝图的蓝图，无穷倒退"）：SRT 表明系统能用'''有限'''指令闭合这个回环<ref name="rogers1967" />。
| |
| − | [[文件:冯诺伊曼的自复制自动机的工作原理.png|缩略图|'''图4'''：自复制机的闭合回路——机器 M 的蓝图描述了 M 的全部部件（构造器 A、拷贝器 B、控制器 C）；启动后 A 读蓝图 <math>\to </math>造出 M 的新副本、B 复制蓝图、C 把它们组装起来。SRT 保证存在这样的蓝图，让有限指令即可闭合循环（驳斥了"蓝图之蓝图无穷倒退"的谬误）。]]
| |
| − |
| |
| − | ==== Quine（自打印程序） ====
| |
| − |
| |
| − | '''现象'''：一个'''不接受任何输入、只打印出自己源代码副本'''的程序<ref name="wikipedia_quine_computing">'''Wikipedia.''' ''Quine (computing)''. <https://en.wikipedia.org/wiki/Quine_(computing).【quine> 的准确定义：不接受输入、只输出自身源码、且不得读取自身源码】【§5.7.6】</ref>。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `cat $0`，被视为"作弊"，不算 quine），只能靠"代码部分 + 代表代码文本的数据部分"来构造性地打印自己；§5.4 例 1 的 Python 程序就是一个标准 quine。"quine" 一词由 [[侯世达|Hofstadter]] 在《[[哥德尔、艾舍尔、巴赫]]》中普及（借自哲学家 W. V. O. Quine 的名字，他构造过自指的句子）<ref name="hofstadter1979">'''Hofstadter, D. R. (1979).''' ''Gödel, Escher, Bach: An Eternal Golden Braid''. Basic Books.【"quine" 一词的普及来源】</ref>。
| |
| − |
| |
| − | '''SRT 如何推出它'''：把 SRT 里的变换规则 <math>f</math> 直接定义:'''"打印"程序'''——<math>f(c) =</math> "打印出 <math>c</math> 的源码的那个程序"。套用 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 <math>c</math>：
| |
| − |
| |
| − | : <math>\phi_c = \phi_{f(c)} = \phi_{"打印 c"}</math>
| |
| − |
| |
| − | 也就是说，程序 <math>c</math> 的行为 = 打印出 <math>c</math> 自己——这正是 quine。所以 quine 就是"取 <math>f =</math> Print 程序、再套 SRT"的一行产物。Kiselyov 在分阶段 <math>\lambda</math> 演算里形式化地证明，quine、[[twine]]（两个程序互相打印对方）、[[trade谜题]]都是 SRT 的不动点<ref name="kiselyov" />.
| |
| − |
| |
| − | ==== 自省程序与自省式自改进程序 ====
| |
| − |
| |
| − | '''[[自省程序]]（introspective program）'''：比 quine 强得多的自指——它能在运行'''"看到"自身（或自身的有界近似），并据此修改、调整自己的行为'''。[[Lisp]] 的 `eval`、Python 的 `inspect`/反射、调试器、动态语言的元对象协议都是它的化身。
| |
| − |
| |
| − | 这一思想最早是 '''Cutland''' 在 ''Computability: An Introduction to Recursive Function Theory''（1980）§1.9 中以 '''<math>\psi</math>-内省/全<math>\psi</math>-内省''' 之名给出严格定义并证明存在性（'''定理 1.9'''）<ref name="cutland1980" />。他关于 <math>\psi</math>-分析与全<math>\psi</math>-内省的原话是：
| |
| − |
| |
| − | 假设给定一个全可计算函数 <math>\psi</math> 和一个程序 <math>P</math>。所谓 <math>P(x)</math> 计算的 '''<math>\psi</math>-分析'''（<math>\psi</math>-analysis），是指 <math>P(x)</math> 计算到 <math>\psi(x)</math> 步的那段计算的代码。称程序 <math>P</math> 在 <math>x</math> 上是 '''<math>\psi</math>-自省'''的（<math>\psi</math>-introspective at <math>x</math>），若 <math>P(x)</math> 收敛并把它自己的 <math>\psi</math>-分析作为输出；若 <math>P</math> 在所有 <math>x</math> 上都是 <math>\psi</math>-自省的，则称为 '''完全 <math>\psi</math>-自省'''的（totally <math>\psi</math>-introspective）。
| |
| − |
| |
| − | * '''定理 1.9'''：存在一个程序 <math>P</math> 是完全 <math>\psi</math>-自省的。
| |
| − | * '''证明'''：直接对可计算函数 <math>f(e, x) = \sigma^*(e, x, \psi(x))</math> 应用推论 1.4（SRT 在 Cutland 体系里的等价形式，<math>\phi_c = \phi_{f(c)}</math> 的不动点形式），得到一个不动点 <math>n</math> 使得:<math>\phi_n(x) = f(n, x) = P_n(x)</math> 的 <math>\psi</math>-分析。□
| |
| − |
| |
| − | 其中 <math>\sigma(e, x, y)</math> 是 Cutland 引入的 '''有界通用函数'''——输出"程序 <math>e</math> 在输入 <math>x</math> 上运行至多 <math>y</math> 步后停下的那段计算的代码（<math>y</math> 步内不停则发散）。所以 <math>f(n, x) = \sigma(n, x, \psi(x))</math> 直译过来就是"把 <math>P_n(x)</math> 跑 <math>\psi(x)</math> 步后的整段计算的代码吐出来"。这里的 <math>\psi</math> 是任意的'''全可计算'''步数函数——既可取常数（"只看自身一固定切片"）也可随 <math>x</math> 变化。'''完全 <math>\psi</math>-自省''' 在 <math>\psi</math> 取常数情形即"输出自身代码的一个有界近似"，恰是现代"自省（introspection）"这一概念的形式化原型。
| |
| − |
| |
| − | '''SRT 的现代等价说法'''：与 quine 同构，只把 <math>f</math> 换成'''有界自模拟器 <math>f_T</math>'''——<math>f_T(c)</math> = "模拟程序 <math>c</math> 运行 <math>T</math> 步的那个程序"（<math>T</math> 是固定步数上界，因此 <math>f_T</math> 是可计算的全函数）。套 SRT（<math>\phi_c = \phi_{f(c)}</math>）得到不动点 <math>c</math>：<math>\phi_c = \phi_{f_T(c)} = \phi_{"模拟 c 运行 T 步"}</math>
| |
| − |
| |
| − | 即程序 <math>c</math> 的行为 = 在 <math>T</math> 步内'''模拟自己'''——它"看到"了自己的有界近似。自省程序的存在性因此是 SRT 的直接推论；这一节的脉络是：Cutland 1980 的定理 1.9 是原始定义/证明，<math>f_T</math> 这套叙事是更易上手的现代等价说法，而 Zhang、Yuan & Zhang (2026) 把它延伸到"自省式自改进程序"<ref name="cutland1980" /><ref name="zhang2026">'''Zhang, J., Yuan, B., & Zhang, Q. (2026).''' Self-Referential Introspection in Large Language Models: The Critical Threshold for Recursive Self-Improvement. ''Entropy'', 28(9), 951.【自省程序（f=<math>f_T</math> 有界自模拟）与自省式自改进程序的定义；SRT 在 LLM 递归自我改进中的应用】【§5.7.7】</ref>.
| |
| − |
| |
| − | '''自省式自改进程序（introspective self-improving program）'''：在自省基础上再进一步——程序不仅模拟自己，还'''基于自模拟结果来修改、改进自己'''。Zhang、Yuan & Zhang (2026) 用这一构造论证：存在能自我模拟、自我改进的程序，并把 von Neumann 的"复杂度阈值"重新诠释为大型语言模型递归自我改进所需的'''自省阈值'''（introspection threshold）——系统必须在自身描述中编码足够多的关于自身的信息，才能维持非退化的递归自我改进，否则会陷入熵退化或模型坍缩<ref name="zhang2026" />。
| |
| − |
| |
| − | ====统一性总结====
| |
| − |
| |
| − | 上述现象共享同一个"对角线 / 自指"技巧，从'''结论性质'''（否定/肯定）和'''所在世界'''（集合论/可计算）两个维度看，完整谱系是：
| |
| − |
| |
| − | [[文件:自指统一性总结.png|替代=自指/对角线部分总结|自指/对角线部分总结|600px]]
| |
| − |
| |
| − | 其中图灵停机问题、哥德尔不完备定理拥有'''双重身份'''：结论是否定性的（与康托尔、罗素问题同类），历史原证也走否定性对角线老路、不依赖 SRT；但因活在程序世界，又能被 SRT 事后更简洁地推出（§5.7.3 展示了停机问题的完整套用过程）。它们共同构成 SRT 的"自指"一面；SRT 还有另一面——"沿序数逐层构造"——见第六节。
| |
| − |
| |
| − | == SRT的其它应用 ==
| |
| − |
| |
| − | 上一节（§5.7）的那些现象都是"自指"本身的例子——程序或句子直接谈论自己。但 SRT 的威力远不止此：它同样是构造不直接涉及自指的复杂数学对象的基本工具。Moschovakis (2010) 以"回顾展"方式列举了 18 个 SRT 发挥关键作用的结果<ref name="moschovakis2010" />，其中最重要的一类是 Kleene 本人最钟爱的'''沿序数逐层构造'''（[[有效超限递归]]）——把递归定义从自然数推广到[[序数]]，从而定义出越来越复杂的对象。本节即以它开篇（前4个例子）；此后转入其余主题——注意第5个板块中的 Rice 家族与 SRT 是“同源，但独立”的关系（并非 SRT 应用），详见该节导言。逻辑学家 Leo Harrington 对 SRT 威力的概括最为传神：
| |
| − |
| |
| − | '''"You need a number z? You got it!"（你需要一个这样的数 z？给你！）'''<ref name="moschovakis2010" />
| |
| − |
| |
| − | === 通用序数记号系统与<math>\omega_1^{CK}</math> ===
| |
| − |
| |
| − | 这是 SRT '''最初的'''应用（见 3.1）。回顾§3.1 的背景：[[序数记号系统]]给可数序数指派自然数代号，使得 0 / 后继 / 极限三分可机械判定、前驱与[[柯西序列|基本序列]]可机械取出。在进入定理之前，先把本节反复用到的几个概念交代清楚（"序数"本身的背景见 §3.1 的背景框）：
| |
| − |
| |
| − | * '''代号与所指'''：记号系统里的每个自然数 <math>a</math> 都是一个'''代号'''，它所指的序数记作 <math>|a|</math>。一个序数 <math>\alpha</math> 的'''后继'''（successor）就是 <math>\alpha+1</math>（0 的后继是 1，<math>\omega</math> 的后继是 <math>\omega+1</math>）。'''极限序数'''（limit ordinal，下文统记作 <math>\lambda</math>）则是既非 0 也非任何序数之后继的序数——它不能靠"+1"走到，只能被一列递增的序数"逼近"，最典型的例子是 <math>\omega</math>（<math>0, 1, 2, 3, \ldots</math> 无限数完之后的那一步：任何自然数都不是它的"前一个"）。
| |
| − | * '''前驱与基本序列'''：后继代号 <math>x</math> 的'''前驱'''（predecessor）记 <math>P(x)</math>——所指序数被"+1"之前那个序数的代号。极限代号 <math>x</math> 的'''基本序列（fundamental sequence）'''是一条可机械取出的递增代号列 <math>x_0</math>, <math>x_1,x_2,\ldots</math>，所指序数 <math>|x_0| < |x_1| < \ldots</math> 逐渐逼近 <math>|x|</math>。
| |
| − | * <math>S_1</math> 的语法（<math>S_1</math> 是下文定理要构造的那个"通用"'''序数记号系统'''，Kleene 1938 为它设计的编码方案；后文的记号系统 O 沿用同一语法）：0 的代号固定为 1；代号 <math>a</math> 的后继的代号写成 '''<math>2^a</math>'''；极限序数的代号写成 '''<math>3\cdot 5^e</math>'''，并约定 <math>|3\cdot5^e| = \lim|\phi_e(n)|</math>（程序 <math>e</math> 逐个吐出逼近该极限的记号列，<math>\phi</math>ₑ 是编号为 <math>e</math> 的程序，见 §2.2）。取这三种质因数形态（1、2 的幂、3<math>\times5</math> 的幂）纯属编码技巧：对代号做质因数分解，就能机械判定它是 0 的代号、后继代号还是极限代号。
| |
| − |
| |
| − |
| |
| − | '''定理（Kleene 1938）'''：存在一个'''通用'''序数记号系统 <math>S_1</math>：对任何其他合法的序数记号系统<math>S</math>（"合法"即满足 §3.1 说的条件——0 / 后继 / 极限三分可机械判定、前驱与基本序列可机械取出），存在可计算函数把 <math>S</math> 的代号'''保序'''地翻译为 <math>S_1</math> 的代号（"保序"：若 <math>|x| < |y|</math>，则翻译后所指的序数仍保持这一大小关系——翻译不打乱任何两个序数的先后）<ref name="kleene1938">'''Kleene, S. C. (1938).''' On notation for ordinal numbers. ''The Journal of Symbolic Logic'', 3(4), 150–155.【第二递归定理的原始出处，定理与证明见 p.153】</ref><ref name="rogers1967" />。
| |
| − |
| |
| − | '''证明的思路'''（这是"有效超限递归"的范式，值得细看）：想要的翻译函数 <math>\psi</math> 应该满足
| |
| − |
| |
| − | : <math>\psi(x) = 1</math> （<math>x</math> 是 0 的代号时）
| |
| − | : <math>\psi(x) = 2^\psi(P(x))</math> （<math>x</math> 是后继序数的代号时，<math>P(x)</math> 是前驱代号）
| |
| − | : <math>\psi(x) = 3\cdot5^e</math> （<math>x</math> 是极限序数的代号时，<math>e</math> 是"逐点翻译基本序列"那个程序的编号）
| |
| − |
| |
| − | 第三行的 <math>e</math> 值得拆开细看——'''<math>\psi</math> 的定义需要用到 <math>\psi</math>，循环正藏在 e 的代码里'''。设 <math>\lambda</math> 是 <math>S</math> 能命名的某个极限序数（就是上文说的那种"既非 0 也非后继、只能被逼近"的序数，例如 <math>\omega</math>），<math>x</math> 是它在 <math>S</math> 中的代号；<math>S</math> 是合法记号系统，故 <math>x</math> 自带一条可计算的基本序列 <math>x_0,x_1,x_2,\ldots</math>——一列递增的代号，所指序数逐渐逼近 <math>\lambda</math>。按上面交代的语法，极限序数的代号必须写成 <math>3\cdot 5^e</math> 的形态，所以 <math>\psi(x)</math> 必须形如 <math>3\cdot5^e</math>，其中 <math>e</math> 是这样一个程序的编号：
| |
| − |
| |
| − | : 输入 <math>n\to </math>从 <math>x</math> 取出 <math>x_n\to </math>'''对 <math>x_n</math> 运行 <math>\psi</math>''' <math>\to </math>输出 <math>\psi(x_n)</math>
| |
| − |
| |
| − | （"逐点翻译基本序列"说的就是它。）这里有两个层面的循环，性质完全不同：
| |
| − |
| |
| − | * '''值的层面（无害）'''：<math>\psi(x) = 3\cdot5^e</math> 是'''一个完整的数'''，<math>e</math> 只是其中 5 的指数；程序 <math>e</math> 的输出是 <math>\psi(x_0)</math>, <math>\psi(x_1),\ldots</math>——<math>x</math> '''下面'''各项的翻译——它从不计算 <math>\psi(x)</math> 自己（极限值由记号的形态约定，不是程序算出来的）。所以不存在"<math>\psi(x)</math> 的值里嵌着 <math>\psi(x)</math> 的值"这种直接自指。
| |
| − | * '''代码的层面（真正的循环）'''：程序 <math>e</math> 要对 <math>x_n</math> 运行 <math>\psi</math>，就必须'''在自己的代码里写死 <math>\psi</math> 的程序编号'''——而 <math>\psi</math> 此刻还在定义中。也就是说，想定义 <math>\psi</math>，得先造出一个"代码里引用了 <math>\psi</math> 的编号"的程序。这正是"右边出现了正在定义的 <math>\psi</math> 自己（及其编号）"的所指；这类循环在普通数学里非法。
| |
| − |
| |
| − | SRT 恰好合法化它：先用 s-m-n 定理（§2.3）造一个可计算函数 <math>q(x, d)</math>——给定 <math>\psi</math> 的编号 <math>d</math>，机械地吐出"读 <math>n</math>、取 <math>x_n</math>、运行程序 <math>d</math>"那个程序的编号。于是想求的 <math>\psi</math> 满足：<math>\psi(x) = 3\cdot5^e</math>，其中 <math>e = q(x, d)</math>，而 <math>d</math> 正是 <math>\psi</math> 自己的编号。把右边整体看作 <math>d</math> 的函数、套 SRT 取不动点 <math>c</math>，令 <math>\psi = \phi_c</math>，循环即闭合；再沿序数归纳验证 <math>\psi</math> 确实是'''全函数'''（"全"：对每个输入代号都有输出，见 §2.1）且保序<ref name="kleene1938" />。
| |
| − |
| |
| − | 顺带分辨两行的差异：第二行 <math>\psi(x) = 2^\psi(P(x))</math> 是'''值依赖值'''的循环，且 <math>P(x)</math> 指向更小的序数，本质上是良基的（"良基"：不存在无穷下降链，所以"沿序数从小到大做归纳"是合法的）；第三行则是'''编号依赖编号'''的循环（<math>e</math> 的代码里嵌着 <math>\psi</math> 的编号），良基性救不了它——必须 SRT。
| |
| − |
| |
| − |
| |
| − | [[文件:Kleene记号系统O.png|缩略图|'''图5'''：[[Kleene's O|Kleene 记号系统 O]] 的树状结构示意。每个自然数都是某个序数的代号——规则：<math>\mid 1\mid = 0</math>（最底层）；<math>\mid 2^x\mid = \mid x\mid + 1</math>（后继，沿着"2 的幂"链向上）；<math>\mid 3\cdot5^e\mid = \lim_n\mid\phi_e(n)\mid</math>（'''极限'''——'''记号里携带基本序列程序的编号 e，这正是 SRT 大显身手的地方'''）。所有构造序数都在这棵树上生长；树顶是 <math>\omega_1^CK</math>（无法被任何机械记号触及的边界）。]]
| |
| − |
| |
| − | 在 <math>S_1</math> 的基础上，Kleene 进一步构造了带树状[[偏序关系]]的'''序数记号系统 O（Kleene's O）'''——"偏序"（partial order）指只在部分代号对之间定义的"小于"关系（O 中记作 <O，反映所指序数的大小）。O 是通用且极大的：每个可被任何合法记号系统命名的序数（称为'''构造序数'''，constructive ordinal）在 O 中都有代号。全体[[递归序数|构造序数]]的[[上确界]]（supremum：不小于它们中任何一个的最小序数）
| |
| − |
| |
| − | : '''<math>\omega_1^{CK}</math> = 最小的非构造序数（Church–Kleene 序数）'''
| |
| − |
| |
| − | 是逻辑学中最基本的"普适常数"之一：它是"机械命名能力"在序数世界中的绝对边界<ref name="kleene1938" /><ref name="rogers1967" />。Rogers 用同样的 SRT 技术证明：O 上的"序数加法"可由一个可计算函数实现<ref name="rogers1967" />。
| |
| − |
| |
| − | 问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
| |
| − |
| |
| − | Kiselyov 以现代眼光补充了这段历史的思想动机：Kleene 放弃用 <math>\lambda</math> 项（他与 Church 两年前的方案）做序数代号，正是因为 <math>\lambda</math> 项作为'''函数'''无法被机械地比较大小；极限序数的代号必须携带'''程序的编号'''而非函数本身——"只有编号（有穷对象）才能被直接给出，这是有穷主义立场的要求"<ref name="kleene1938" /><ref name="kiselyov" />。
| |
| − |
| |
| − | === 构造序数 = 递归序数 ===
| |
| − |
| |
| − | 可数序数有两种自然刻画："'''构造序数'''"（能被某个机械记号系统命名，见 6.1）与"'''递归序数'''"（某个可计算良序的长度——即存在一个可计算的大小关系，把一堆自然数排成该长度的"无限队列"）。
| |
| − |
| |
| − | * '''Markwald–Spector 定理（1954/1955）'''：两种刻画恰好等价——构造序数 ⟺ [[递归序数]]<ref name="rogers1967" /><ref name="moschovakis2010" />。
| |
| − |
| |
| − | 这是经典集合论事实"第二数类的两种刻画等价"的可计算版本；两个方向的证明都以 SRT 为归纳枢纽<ref name="moschovakis2010" />。
| |
| − |
| |
| − | === 超算术层级与 Spector 唯一性定理 ===
| |
| − |
| |
| − | 需要先铺垫三个概念。
| |
| − |
| |
| − | '''[[神谕]]（oracle）'''：给程序外接一块只读"数据库"——集合 A。程序运行中可随时查询"数 n 是否属于 A"并立即得到正确答案。这样的 A 称为神谕；"以 A 为神谕可计算"衡量的是：'''若把 A 白送给你，你还能多算出什么'''。
| |
| − |
| |
| − | '''[[Turing跳跃]]（Turing jump）'''：对任何集合 A，把"哪些以 A 为神谕的程序会停机"这一问题本身收集成一个集合，记作 A′（读作"A 撇"）。可以证明：A′ 以 A 为神谕仍不可计算——每跳一次，都得到一个严格更难的"相对版停机问题"。特别地，从空集 <math>\emptyset</math> 出发跳一次得到的 <math>\emptyset'</math>，正是通常意义下的停机问题（5.7.3）。
| |
| − |
| |
| − | '''沿构造序数"盖楼"'''：现在从 <math>H_0 = \emptyset</math> 出发，沿构造序数（见 6.1）逐层往上盖：
| |
| − |
| |
| − | : <math>H_{\alpha+1}</math> = (<math>H_\alpha</math>)′ （后继层：再跳一次，复杂度升一级）
| |
| − | : <math>H_\lambda = \cup_n H_{\lambda_n}</math> （极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）
| |
| − |
| |
| − | 在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 5.7.4 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 6.4 的主题。<ref name="moschovakis2010" />
| |
| − |
| |
| − | 问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？
| |
| − |
| |
| − | * '''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" />。
| |
| − |
| |
| − | === <math>HYP = \Delta^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 定理（1955）'''：自然数的集合 A 是 <math>\Delta^1_1</math> 的，当且仅当 A 是[[超算术]]的（HYP）<ref name="kleene1955">Kleene, S. C. (1955). On the forms of the predicates in the theory of constructive ordinals (second paper). ''American Journal of Mathematics'', 77, 405–428.【<math>\Delta^1_1</math> = 超算术集合（HYP）的原始定理出处（§6.4）】</ref><ref name="moschovakis2010" />。
| |
| − |
| |
| − | 这把可计算性理论（HYP，由机器和序数定义）与[[描述集合论]]（<math>\Delta^1_1</math>，由投影/量化定义）两大传统焊接在一起，是 Kleene 获 1983 年 AMS Steele 奖的核心成果之一。证明的两个引理（[[Kleene's O]] 是 <math>\Pi^1_1</math> 集、且是 <math>\Pi^1_1</math> 中"最复杂"的完备集）都靠 SRT 沿良基树作[[有效超限递归]]建立<ref name="moschovakis2010" />.
| |
| − |
| |
| − | 在此基础上，SRT 向实数空间（[[贝尔空间|Baire 空间]]，即自然数无穷序列的空间）推广后，成为'''[[有效描述集合论]]'''的引擎，三个代表性结果：
| |
| − |
| |
| − | 1. '''[[Suslin–Kleene定理]]'''：[[博雷尔集|Borel 集]]（从开集出发经可数次并、交、补生成的集合）与 <math>\Delta^1_1</math> 集之间可以可计算地互译。它同时蕴含经典 [[米哈伊尔·苏斯林|Suslin]] 定理（<math>\Delta^1_1 = Borel</math>）和上述 Kleene 定理，是两大传统的汇合点<ref name="moschovakis2010" />；
| |
| − | 2. '''[[赋范归纳定理]]'''（Moschovakis 1974）：对带有良好"秩函数"结构的归纳定义，其最小/最大不动点保持在相应的可定义层级内。它的证明使用"关系版 SRT"（不动点代码 <math>\varepsilon</math>* 使自己的每个后继元组都由自己的前段定义）。这可视为对 Kleene 1944 年错误（见 3.3）的"正确打开方式"：SRT 只给某个不动点，要拿到'''最小'''不动点需要额外的秩结构<ref name="moschovakis2010" />；
| |
| − | 3. '''[[编码引理]]'''（Moschovakis 1970）：在 ZF+DC+AD（确定性公理，一个与大[[基数]]理论相关的集合论假设）下，若[[连续统]]可满射到基数 <math>\kappa</math>，则可满射到 <math>\kappa</math> 的幂集。证明通过'''带参数的 SRT'''作有效超限递归——SRT 由此进入基数算术这一纯集合论领域；它还是 '''[[Jackson 定理]]'''（1989：在 AD 下，三型存在量词的 Kleene 序数恰好等于'''最小的弱不可达基数'''）的基本工具——这是连接高类型递归论与大基数理论的最惊人结果之一<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. 集，则写法是
| |
| − |
| |
| − | : <math>A = \{ e : W_e \in \mathcal{A}\}</math>
| |
| − |
| |
| − | （换成函数视角就是 <math>A = { e : \phi_e</math> 具有性质 <math>\mathcal{A}\}</math> 。）可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。
| |
| − |
| |
| − | 与 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> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。
| |
| − |
| |
| − | * '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
| |
| − | # 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；
| |
| − | # 对每个 <math>x</math>，用 s-m-n 定理（§2.3）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；
| |
| − | # 于是 <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">'''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" />。
| |
| − |
| |
| − | ==== Rice-Shapiro 定理（1956） ====
| |
| − |
| |
| − | Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：
| |
| − |
| |
| − | 设 <math>A = \{ e :W_e \in \mathcal{A}\}</math> 是索引集。A 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 <math>\mathcal{S} = \{S_0,S_1,S_2,\ldots</math>}，使得 <math>W\in \mathcal{A}</math> ⟺ <math>\delta</math>中存在某个 <math>S_i \subseteq W</math>。
| |
| − |
| |
| − | 含义：一个行为性质若能'''被枚举地识别'''（索引集 r.e.），它就必须由'''有限证据'''决定——W 一旦包含某个预列的有限集 <math>S_i</math>，性质即成立；反之，性质成立也只需某个有限子集作证。"能识别 ⟹ 只依赖有限信息"这一半是紧致性式的论证（若性质的成立只靠无限多证据，枚举过程就永远等不到决定性的一刻）；"有限可生成 ⟹ 可枚举"那一半是直接列举。两个方向都与 SRT 无关。
| |
| − |
| |
| − | 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定理]]：[[创造集]] = [[完备集]] ====
| |
| − |
| |
| − | '''背景'''：停机问题集合 <math>K = \{e : \text{程序} e \text{在输入} e \text{上停机}\}</math> 是 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">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" />。
| |
| − |
| |
| − | === 有效运算的连续性：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> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：
| |
| − |
| |
| − | '''Myhill–Shepherdson 定理（1955）'''：对可计算变换而言，两种方式恰好等价——任何"按代码"的可计算变换都能改写成"按值"的图灵机计算，反之亦然<ref name="myhill1955" /><ref name="moschovakis2010" />.
| |
| − |
| |
| − | 证明的两个关键引理（变换必然是单调的、必然是连续的）都依赖 SRT：构造一个"监视 <math>\Phi</math> 是否已输出、在此之前模仿函数 <math>\phi_1</math>、之后叛变为函数 <math>\phi_2</math>"的程序 z——z 的行为取决于 z 自己（经 <math>\Phi</math> 处理后）的表现，由 SRT 提供，再用"同一函数的不同编号必须得到同一结果"逼出矛盾<ref name="moschovakis2010" />.
| |
| − |
| |
| − | '''Kreisel–Lacombe–Shoenfield–Čeĭnin 定理（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现。<ref name="moschovakis2010" />
| |
| − |
| |
| − | [[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。
| |
| − |
| |
| − | 此外，Rogers 用 SRT 证明了 '''[[Blum定理]]'''：任意两个"通用部分函数"（即[[解释器]]）都只差一个可计算的重新编号（递归同构）——编号系统在"重新命名"意义下本质唯一<ref name="rogers1967" />.
| |
| − |
| |
| − | === Solovay 可证性逻辑 ===
| |
| − |
| |
| − | '''背景'''：'''可证性逻辑（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">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" />。
| |
| − |
| |
| − | === 应用地图一览 ===
| |
| − |
| |
| − | {| class="wikitable"
| |
| − | |-
| |
| − | ! 领域
| |
| − | ! 代表性结果
| |
| − | ! SRT 的角色
| |
| − | |-
| |
| − | | r.e. 索引集理论
| |
| − | | Rice 定理；Rice-Shapiro；Myhill：创造集 = 完备集
| |
| − | | 前两者：同源但独立（非 SRT）；Myhill：构造"监控自己"的程序〔§2〕
| |
| − | |-
| |
| − | | 有效运算
| |
| − | | Myhill–Shepherdson；KLS–Čeĭnin 连续性
| |
| − | | 证明单调性与连续性〔§§3–4〕
| |
| − | |-
| |
| − | | 可证性逻辑
| |
| − | | Solovay：GL 完备性
| |
| − | | 构造自指函数〔§6〕
| |
| − | |-
| |
| − | | 序数记号
| |
| − | | 通用系统、Kleene's O、<math>\omega_1^{CK}</math>
| |
| − | | 最初的用武之地〔§7〕
| |
| − | |-
| |
| − | | 超算术理论
| |
| − | | Markwald–Spector；Spector 唯一性；HYP = <math>\Delta^1_1</math>
| |
| − | | 每个证明的归纳枢纽〔§§8–9〕
| |
| − | |-
| |
| − | | 有效描述集合论
| |
| − | | Suslin–Kleene；赋范归纳；编码引理
| |
| − | | 关系版/参数版 SRT〔§10〕
| |
| − | |-
| |
| − | | 高类型递归
| |
| − | | Kleene 1959 体系；Jackson 定理
| |
| − | | 理论的第一块基石〔§11〕
| |
| − | |-
| |
| − | | 直觉主义数学
| |
| − | | 可实现性、bar 递归合法性
| |
| − | | 验证自指定义〔§12〕
| |
| − | |-
| |
| − | | 函数式编程
| |
| − | | Y 组合子的推广、部分求值
| |
| − | | 元编程的不动点原理<ref name="kiselyov" />
| |
| − | |}
| |
| − |
| |
| − | （表中"§"编号均指 Moschovakis 2010<ref name="moschovakis2010" /> 的章节。）
| |
| − |
| |
| − | == 评注与影响 ==
| |
| − |
| |
| − | # '''简单性与普适性的反差'''。SRT 的全部证明只有一行对角线，应用却横跨逻辑学几乎所有分支。Moschovakis 指出：其广泛适用性恰恰'''源于'''这种简单——它极易被翻译到自然数以外的语境（实数空间、任意 Polish 空间、高类型对象、模态逻辑），在每个语境中重新化身<ref name="moschovakis2010" />。
| |
| − | # '''两个递归定理的分工'''。第一递归定理保证'''递归定义有最小解'''（函数层面、序理论的不动点）；第二递归定理保证'''自指定义合法'''（代码层面的不动点）。前者回答"这个函数方程有解吗"，后者回答"我能在定义中引用被定义者自己的代码吗"。强定理蕴含弱定理，反之不然（见 4.4）。
| |
| − | # '''自指的数学化'''。从 Gödel 的替换函数、Turing 的通用机、von Neumann 的自复制自动机，到 quine、计算机病毒、编译器自举，乃至人工智能中"系统改进自身"的设想，"系统谈论自身"的可行性边界都由同一种对角线结构划定。Kleene 递归定理是这一结构最干净、最一般的陈述。
| |
| − | # '''历史反讽'''。Kleene 1938 年发明 SRT 是为了构造序数记号，而 1944 年他恰恰因为"拿到一个不动点却误以为拿到最小不动点"而犯下著名错误，直到 1955 年才纠正（见 3.3）——这个故事最恰当地说明了理解两个递归定理'''区别'''的重要性。
| |
| − | # '''Rogers 的总评'''：递归定理是"一个基本的研究工具、一个深刻的结果"（a basic research tool <math>\ldots</math> a deep result），它的深刻在于"以优雅和智识上的经济性，处理那些否则需要繁复构造的问题"<ref name="rogers1967" />；虽然它的直接效果常是产生各种"病态"结构（自我枚举的集合、自我打印的程序），但它在 Myhill 定理等结果中起到了"在此前独立定义的概念之间建立正则联系"的作用<ref name="rogers1967" />。
| |
| − |
| |
| − | <references />
| |