3,094
个编辑
更改
跳到导航
跳到搜索
第454行：
第454行： + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
无编辑摘要
'''与 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>。
'''与 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" />.