3,094
个编辑
更改
跳到导航
跳到搜索
第288行：
第288行： − − === 直观图景：程序如何"谈论"自己的代码 === − − '''例 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 的"双重身份"分析。
无编辑摘要
'''与"一行证明"的关系'''：§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> 都被对角线穿一格，循环天然闭合。
'''与"一行证明"的关系'''：§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像素]]
[[文件:列表法证明.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像素]]