| 第365行： |
第365行： |
| | | | |
| | 这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。 | | 这一视角澄清了 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"/>。它的约束很苛刻——'''不能读自己的源码'''（靠读文件输出自己、如 `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 还有另一面——"沿序数逐层构造"——见第六节。
| |