3,094
个编辑
更改
无编辑摘要
——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。
——按规则展开后，这个短语恰好指称'''它自己'''<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" />