3,094
个编辑
更改
跳到导航
跳到搜索
第44行：
第44行： − − == 预备知识：读懂本词条所需的全部概念 == − − 本节用程序员熟悉的语言解释文中会反复出现的五个概念。已经熟悉的读者可以跳过。 − − === "可计算"与"部分函数" === − − '''[[可计算的]]（computable / effective / recursive）'''：一个函数是"可计算的"，意思是存在一套'''固定的、有穷的指令'''（程序），使得对任何输入，只要机械地按指令执行有穷多步，就能得到输出。"可计算的"（computable）、"有效的"（effective）、"递归的"（recursive）在本文中是同义词——这是历史造成的术语冗余，三个词来自 Church、Turing、Gödel–Kleene 三条等价的技术路线<ref name="kleene1938" />。 − − '''[[部分函数]]（partial function）'''：一台机器在某些输入上可能'''永远不停机'''（死循环），这时它在这些输入上'''没有输出'''。我们把"在部分输入上有定义、在其余输入上无定义"的函数称为部分函数；在所有输入上都有定义的称为'''[[全函数]]（total function）'''。程序天然对应部分函数，而不是数学课本里那种"处处有值"的函数——这是可计算性理论与普通数学的第一个思维差异。 − − '''记号 <math>\phi_e</math>'''：把全体程序（的所有可计算部分函数）排成一个序列，用自然数 0, 1, 2, <math>\ldots</math> 编号，'''<math>\phi_e</math> 表示"编号为 e 的程序所计算的那个部分函数"'''。这个编号也叫'''[[哥德尔配数]]（Gödel number）'''：关键思想是"程序本身也是一个有限符号串，可以编码成一个自然数"，于是'''程序即数据'''——程序可以作为另一个程序的输入被处理。<math>\phi_e(x)</math> 表示"编号 <math>e</math> 的程序在输入 <math>x</math> 上的输出"（可能无定义）。本文中 <math>p \downarrow</math> 表示"程序 <math>p</math> 停机（有输出）"，<math>p \uparrow</math> 表示"不停机（无输出）"。 − − === 通用程序（解释器） === − − 存在一台"通用机器"：给它输入 <math>(e, x)</math>，它就'''模拟'''编号 <math>e</math> 的程序在输入 <math>x</math> 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的[[通用图灵机]]是它的首个化身。用记号写就是：存在程序<math>i</math> 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" /> − − === s-m-n 定理（柯里化 / 参数特化） === − − '''[[s-m-n 定理]]'''说：给定一个双输入程序和它的'''第一个输入'''，可以机械地生成一个"把第一个输入写死在程序里"的新单输入程序。用程序员的话说，就是'''[[柯里化]]（currying）或部分应用（partial application）总是可以机械完成的'''：存在可计算的全函数 <math>S</math>，使得 − − : <math>\phi_{S(e, y)}(x) = \phi_e(y, x)</math> − − 即"程序 <math>S(e,y)</math>"在输入 <math>x</math> 上的行为 = "程序 <math>e</math>"在输入 <math>(y, x)</math> 上的行为。Kleene 1938 年论文中的 <math>S</math> 函数就是这个工具<ref name="kleene1938" />。'''第二递归定理的证明只需要这一个工具'''，此外什么都不需要——这是它惊人简单的原因。 − − === 递归可枚举集（r.e. set） === − − 一个自然数集合称为'''[[递归可枚举]]的（recursively enumerable, 简写为r.e.）'''，如果存在一台机器能把它的元素'''一个一个地全部列出来'''（允许重复、允许乱序；不在集合里的元素永远不会被列出）。等价地，r.e. 集就是某个程序'''有定义的输入的集合'''（即 <math>\phi_e</math> 的定义域），记作 <math>W_e</math>。典型例子："所有会停机的 (程序,输入) 对"构成的集合（[[停机问题]]集合 <math>K</math>）是 r.e. 的，但它的补集不是——这正是"[[停机问题不可判定]]"的现代表述。 − − === "不动点"的两种含义（重要！） === − − "[[不动点]]"在本文中出现于两个截然不同的层面，混淆它们是最常见的理解障碍： − − * '''函数层面的不动点'''（[[#第一递归定理（FRT）|第一递归定理]]）：变换规则 <math>\Psi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Psi(\phi)</math>；若 <math>\Psi(\phi) = \phi</math>（作为函数处处相等），<math>\phi</math> 就是 <math>\Psi</math> 的不动点。这与分析学中"<math>f(x) = x</math> 的解"同类。 − * '''代码层面的不动点'''（第二递归定理）：变换规则 <math>f</math> 把程序编号 <math>n</math> 变成新编号 <math>f(n)</math>；'''注意 <math>f(n)\neq n</math> 通常成立'''——程序代码确实变了；但神奇的是，新程序 <math>f(n)</math> 和旧程序 <math>n</math> '''计算的函数相同'''：<math>\phi_n = \phi_{f(n)}</math>。所以"不动"的不是代码，而是'''代码的行为'''。[[Hartley Rogers, Jr|Rogers]] 为此特意造了"'''不动点值'''（fixed-point value）"一词，强调它不是数值不动点<ref name="rogers1967" />。 − − == 历史背景 == − − === 起源：一篇研究"序数记号"的 6 页短文 === − − 第二递归定理诞生于 Kleene 1938 年发表于《符号逻辑杂志》（''The Journal of Symbolic Logic''）的一篇仅 6 页的短文《论序数的记号》（''On Notation for Ordinal Numbers''）<ref name="kleene1938" />。这篇论文的主题表面上与"递归定理"毫不相干： − − '''背景知识——[[序数]]（ordinal number）'''：序数是"无限队列的长度"的数学化。数完 0, 1, 2, 3, <math>\ldots</math>（全体自然数）之后，数学上允许继续数：第一个"超过所有自然数"的序数记作 <math>\omega</math>，然后还有 <math>\omega+1</math>, <math>\omega+2</math>, <math>\ldots</math>, <math>\omega\cdot2</math>, <math>\ldots</math>, <math>\omega^2</math>, <math>\ldots</math>, <math>\omega^\omega</math>, <math>\ldots</math>，可以无限延伸。所有"能用可数步骤达到"的序数称为'''[[可数序数]]'''，它们的总体（第二数类）是不可数的。 − − Church 与 Kleene 在 1930 年代问了一个构造性问题：'''能不能给每个可数序数起一个"机械可读的代号"（自然数编码），使得仅凭代号就能机械地判断：这个序数是 0、是某个序数的后继（+1）、还是某个递增序列的极限？并且在后两种情况下能机械地取出前驱代号或序列代号？''' 满足这些条件的编码方案称为一个'''[[序数记号系统]]'''（Kleene 称之为 [[r-system]]）<ref name="kleene1938" />。 − − Kleene 在论文的 §2 中建立了[[可计算函数]]的基本技术（编号、[[通用函数]]、§2.3 的 [[S函数]]），然后在 §2 的最后'''顺手'''陈述并证明了一个当时没有名字的定理<ref name="kleene1938" />： − − * '''若 <math>\psi(z, x)</math> 是任意可计算的部分函数，则存在一个数 <math>f</math>，使得 <math>\phi_f(x) = \psi(f, x)</math> 对所有 <math>x</math> 成立（等号含义：两边同时无定义，或同时有定义且相等）。''' − − * 证明：设 e 是函数 <math>\psi(S(y,y), x)</math> 的编号，取 <math>f = S(e, e)</math> 即可。 − − ——这就是'''第二递归定理'''的原始形态。Moschovakis 称之为 Kleene 没有意识到自己发掘出"小宝石"（little gem）<ref name="moschovakis2010" />；Kiselyov 则以"'''函数式珍珠'''（A Functional Pearl）"为题向函数式编程社区重新发掘了它<ref name="kiselyov" />。 − − 这个"小宝石"随即在论文<ref name="kleene1938" />的 §3 被用于证明该文的主要结果：'''存在一个"通用"[[序数记号系统]] <math>S_1</math>'''——任何其他合法记号系统能命名的序数，<math>S_1</math> 都能命名，且翻译过程本身是可计算的<ref name="kleene1938" />。这是"沿着序数逐层向上做递归定义"（后来称为'''[[有效超限递归]]'''，effective transfinite recursion）这一方法的首次应用。Kleene 由此构造出著名的'''[[记号系统 O]]（[[Kleene's O]]）'''，并证明存在最小的一个"不可命名"的序数——'''[[Church–Kleene 序数]] <math>\omega_1^{CK}</math>'''，即[[序数|可数序数]]中第一个无法被任何机械记号系统触及的序数<ref name="kleene1938" /><ref name="rogers1967" />。 − − === 命名史 === − − '''Kleene 本人'''始终只叫它 '''"the recursion theorem"（递归定理）'''——即使在他 1952 年的《元数学导论》（''Introduction to Metamathematics''）中两个定理同时出现时，也未加区分<ref name="moschovakis2010" />。 − − '''Rogers (1967)''' 在其经典教材第 11 章首次建议：在两个定理同台的语境中，把关于"函数变换规则的不动点"的定理称为'''第一递归定理'''（Rogers 书中 Theorems XI、XII），把 Kleene 1938 的定理称为'''第二递归定理'''（Rogers 书中 Theorem IV）<ref name="rogers1967" />。Moschovakis 明确表示支持："在允许投票的场合，我投票采纳 Rogers 的命名"<ref name="moschovakis2010" />。 − − 关于证明是怎么想到的：有学生曾问 Kleene，这个"短得可疑、巧得离谱"的两行证明从何而来，Kleene（也许是开玩笑地）回答说他只'''"拿着 s-m-n 性质瞎鼓捣"'''（"fiddled around with (b)"）<ref name="moschovakis2010" />。Moschovakis 评论说，这种"鼓捣"很可能受到 [[<math>\lambda</math> 演算]]（Church 与 Kleene 此前共同发展的形式系统）中类似[[对角线构造]]的启发〔同上〕。 − − === 一个值得铭记的教训 === − − 1944 年，Kleene 曾'''错误地'''宣称他构造的记号集 O 具有较低的[[逻辑复杂度]]（属于 <math>\Pi^0_2</math> 类），因为他把第二递归定理给出的'''某一个'''不动点，误当作了归纳定义所要求的'''最小'''不动点。事实上 O 的复杂度要高得多（它是<math>\Pi^1_1</math>-完备），Kleene 直到 1955 年才纠正<ref name="moschovakis2010" />。这个故事最生动地说明了：'''第二递归定理只保证"给你一个不动点"，不保证给你"最小/最特殊的那个"'''——这正是它区别于第一递归定理的关键（见 4.4 与 6.6）。 − − == 第一递归定理（FRT） == − − === 从"递归定义的函数"说起 === − − 编程中最自然的定义方式是'''[[递归]]'''：定义阶乘时写 `fac(n) = n * fac(n-1)`，等号右边出现了正在定义的函数自己。抽象地看，这类定义都在解一个"函数方程"： − − : <math>\phi = \Psi(\phi)</math> − − 其中 '''<math>\Psi</math> 是一个"函数变换规则"'''（输入一个函数 <math>\phi</math>，输出一个新函数 <math>\Psi(\phi)</math>；术语叫'''[[算子]]'''，operator）。例如阶乘定义对应的 <math>\Psi</math> 是：给定任意函数 <math>\phi</math>，输出新函数 <math>\phi'</math>，其中 <math>\phi'(0) = 1</math>， − : <math>\phi'(n) = n\cdot\phi(n−1)</math>。 − − 第一递归定理问的是：'''什么样的 <math>\Psi</math> 能保证方程 <math>\phi = \Psi(\phi)</math> 有解，而且解是[[可计算的]]？''' − − === 定理表述 === − − '''定义（可计算的变换规则）'''：如果变换 <math>\Psi</math> 满足下面两条，就称它是'''[[递归算子]]（recursive operator）'''： − − # '''单调性'''：<math>\phi \subseteq \psi</math>（即 <math>\psi</math> 在 <math>\phi</math> 有定义的地方都有定义且取值相同）蕴含 <math>\Psi(\phi) \subseteq \Psi(\psi)</math>； − # '''有限性/连续性'''：<math>\Psi(\phi)</math> 的每个输出只依赖 <math>\phi</math> 在'''有限个'''输入上的值。 − − 直觉地说，第二条就是"机器在任何时刻只能查看有限多的已有计算结果"——这是"机械可执行"的数学化。[[阶乘]]、[[斐波那契数列]]、以及绝大多数程序语言中的递归定义都满足这两条<ref name="rogers1967" />. − − − '''第一递归定理'''：设 <math>\Psi</math> 是递归算子，则存在函数 <math>\phi</math> 使得： − − # <math>\Psi(\phi) = \phi</math>（<math>\phi</math> 是方程的解，即 <math>\Psi</math> 的不动点）； − # '''最小性'''：任何其他解 <math>\psi</math> 都满足 <math>\phi \subseteq \psi</math>（<math>\phi</math> 是"信息最少"的解）； − # '''可计算性'''：<math>\phi</math> 是可计算的部分函数。 − − '''证明思路'''：从"处处无定义的空函数"出发，反复应用 <math>\Psi</math>：<math>\phi_0</math> = 空，<math>\phi_1 = \Psi(\phi_0)</math>，<math>\phi_2 = \Psi(\phi_1),\ldots\ldots</math>。单调性保证这个序列不断"变长"（每次迭代只增不减）；有限性保证最终收敛到一个函数 <math>\phi</math>，且 <math>\Psi(\phi) = \phi</math>；"每一步都是机械操作"保证 <math>\phi</math> 整体可计算。取所有 <math>\phi_n</math>的并就是答案<ref name="rogers1967" />。 − − − '''例子'''：方程组 <math>\phi(1) = 2</math>，<math>\phi(2x) = 2\phi(x)</math> 对应一个递归算子，其最小不动点是：<math>\phi(x) = x</math>（当 <math>x</math> 是 2 的幂），其余输入无定义。注意"最小性"自动处理了定义不完整的分支——机器在"非 2 的幂"上自然发散<ref name="rogers1967" />。 − − === 意义：递归定义的"存在性定理" === − − 第一递归定理的角色，类似于分析学中用[[不动点定理]]（如 Banach 压缩映像原理）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定义递归函数时无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比[[集合论]]中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''Church–Turing 论题'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。 − − 数学血统上，它是 '''Knaster–Tarski 不动点定理'''（[[序理论]]中"[[完备格]]上的[[单调映射]]必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。 − − === 与第二递归定理的关系 === − − Rogers 证明了：'''第二递归定理（强）蕴含第一递归定理（弱）'''——存在统一的机械方法，把"函数层面的不动点问题"翻译成"代码层面的不动点问题"，并且翻译后得到的不动点恰好是'''最小'''的<ref name="rogers1967" />。反过来不成立：第五、六节中第二递归定理的应用几乎都无法由第一递归定理得到。因此两者中'''第二递归定理更基本、更强大'''<ref name="rogers1967" />。 − − 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" />
无编辑摘要
第二递归定理被 [[Yiannis N. Moschovakis|Moschovakis]] 称为 '''"令人惊叹的"（amazing）'''——他的综述标题就叫 ''Kleene's Amazing Second Recursion Theorem''<ref name="moschovakis2010" />；计算机科学家 Neil Jones 称之'''"可计算性的瑞士军刀"（A Swiss Pocket Knife for Computability）'''〔转引自 Kiselyov<ref name="kiselyov">'''Kiselyov, O.''' ''Kleene Second Recursion Theorem: A Functional Pearl''.【<math>\lambda</math> 演算/函数式编程视角；quine、twine、性能分析；Unix `cat` 例子出处】</ref>, §1〕。它的一行证明看似只是个小技巧，却支撑了从 [[哥德尔|Gödel]] 不完备定理到[[序数]]理论、从程序自复制到有效[[描述集合论]]的庞大理论大厦（详见第五、六节）。
第二递归定理被 [[Yiannis N. Moschovakis|Moschovakis]] 称为 '''"令人惊叹的"（amazing）'''——他的综述标题就叫 ''Kleene's Amazing Second Recursion Theorem''<ref name="moschovakis2010" />；计算机科学家 Neil Jones 称之'''"可计算性的瑞士军刀"（A Swiss Pocket Knife for Computability）'''〔转引自 Kiselyov<ref name="kiselyov">'''Kiselyov, O.''' ''Kleene Second Recursion Theorem: A Functional Pearl''.【<math>\lambda</math> 演算/函数式编程视角；quine、twine、性能分析；Unix `cat` 例子出处】</ref>, §1〕。它的一行证明看似只是个小技巧，却支撑了从 [[哥德尔|Gödel]] 不完备定理到[[序数]]理论、从程序自复制到有效[[描述集合论]]的庞大理论大厦（详见第五、六节）。