3,094
个编辑
更改
无编辑摘要
= Kleene 递归定理（Kleene's Recursion Theorems） =
= Kleene 递归定理（Kleene's Recursion Theorems） =
两个定理的对照表（其中涉及的符号会在第二节逐一解释，此处可先跳过细节）：
两个定理的对照表（其中涉及的符号会在第二节逐一解释，此处可先跳过细节）：
| |'''第一递归定理'''（First Recursion Theorem, FRT）|'''第二递归定理'''（Second Recursion Theorem, SRT）|
{| class="wikitable"
| -------- | -------------------------------------------------------- | ------------------------------------------------------------------------------------- |
|-
|'''作用对象'''|函数本身（"把函数变成函数"的规则）|程序的编号（代码）|
!
|'''结论'''|任何可计算的函数变换规则 <math>\Psi</math> 都有最小不动点 <math>\phi</math>，且 <math>\phi</math> 是可计算的：<math>\Psi(\phi) = \phi</math>|任何可计算的程序变换规则 f 都有不动点 n：程序 n 与程序 f(n) 计算同一个函数，记作 <math>\phi_n = \phi_{f(n)}</math>|
! '''第一递归定理'''（First Recursion Theorem, FRT）
|'''数学血统'''|序理论中 Knaster–Tarski 不动点定理的"可计算版本"<ref name="rogers1967" />|对角线方法（diagonalization，Cantor、Gödel、Turing 用过的同一种论证技术）的集大成者<ref name="rogers1967" />|
! '''第二递归定理'''（Second Recursion Theorem, SRT）
|'''别称'''|弱递归定理|强递归定理、Kleene 不动点定理|
|-
|'''首次出现'''|Kleene (1952)《元数学导论》中明确表述<ref name="moschovakis2010" />|Kleene (1938) §2 末尾，当时甚至没有名字，证明只有两行<ref name="kleene1938" />|
| '''作用对象'''
| 函数本身（"把函数变成函数"的规则）
| 程序的编号（代码）
|-
| '''结论'''
| 任何可计算的函数变换规则 <math>\Psi</math> 都有最小不动点 <math>\phi</math>，且 <math>\phi</math> 是可计算的：<math>\Psi(\phi) = \phi</math>
| 任何可计算的程序变换规则 f 都有不动点 n：程序 n 与程序 f(n) 计算同一个函数，记作 <math>\phi_n = \phi_{f(n)}</math>
|-
| '''数学血统'''
| 序理论中 Knaster–Tarski 不动点定理的"可计算版本"<ref name="rogers1967" />
| 对角线方法（diagonalization，Cantor、Gödel、Turing 用过的同一种论证技术）的集大成者<ref name="rogers1967" />
|-
| '''别称'''
| 弱递归定理
| 强递归定理、Kleene 不动点定理
|-
| '''首次出现'''
| Kleene (1952)《元数学导论》中明确表述<ref name="moschovakis2010" />
| Kleene (1938) §2 末尾，当时甚至没有名字，证明只有两行<ref name="kleene1938" />
|}
'''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 §5.3 那一行证明——给定 f，构造 <math>\psi(x) = \phi_{S(x,x)}</math>（其中 S 把 f 与"自应用"组合起来），取 e 满足 <math>\phi_e = \psi</math>，再对 <math>\psi</math> 套 SRT 取不动点——会发现它和 quine 是'''同一种构造'''，差别只在目的（执行层面 vs 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：
'''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 §5.3 那一行证明——给定 f，构造 <math>\psi(x) = \phi_{S(x,x)}</math>（其中 S 把 f 与"自应用"组合起来），取 e 满足 <math>\phi_e = \psi</math>，再对 <math>\psi</math> 套 SRT 取不动点——会发现它和 quine 是'''同一种构造'''，差别只在目的（执行层面 vs 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：
| |'''quine 的自指'''|'''SRT 证明的自指'''|
{| class="wikitable"
|---|---|---|
|-
|'''自指的载体'''|字符串 `c`（程序的源码）|编号 e（程序在 <math>\phi</math> 枚举里的下标）|
!
|'''载体在哪里被引用'''|`print(c % c)` 把 c 嵌入 print 的实参|<math>\psi(x) = \phi_{S(x,x)}</math> 把 e 作为通用函数的下标|
! '''quine 的自指'''
|'''构造方向'''|先有具体 f（= Print），再造 c（c 的代码里嵌入 f 的引用）|先有具体 f（§5.3 假设中任意一个），再造 c（c 由对 f 套 SRT 得到）|
! '''SRT 证明的自指'''
|'''目的'''|让 c 的输出 = c 的源码|让 <math>\phi_c</math> 等价于 <math>\phi_{f(c)}</math>|
|-
|'''得到什么'''|一个具体程序（f = Print 时的不动点）|一个具体程序（这个 f 的不动点 c），且这个 c '''依赖 f'''（不同 f 给出不同 c）|
| '''自指的载体'''
| 字符串 `c`（程序的源码）
| 编号 e（程序在 <math>\phi</math> 枚举里的下标）
|-
| '''载体在哪里被引用'''
| `print(c % c)` 把 c 嵌入 print 的实参
| <math>\psi(x) = \phi_{S(x,x)}</math> 把 e 作为通用函数的下标
|-
| '''构造方向'''
| 先有具体 f（= Print），再造 c（c 的代码里嵌入 f 的引用）
| 先有具体 f（§5.3 假设中任意一个），再造 c（c 由对 f 套 SRT 得到）
|-
| '''目的'''
| 让 c 的输出 = c 的源码
| 让 <math>\phi_c</math> 等价于 <math>\phi_{f(c)}</math>
|-
| '''得到什么'''
| 一个具体程序（f = Print 时的不动点）
| 一个具体程序（这个 f 的不动点 c），且这个 c '''依赖 f'''（不同 f 给出不同 c）
|}
也就是说，'''SRT 证明与 quine 不是"互逆"，而是同构'''——两者都是"先有一个具体的全可计算函数 f、再造一个不动点程序 c 满足 <math>\phi_c = \phi_{f(c)}</math>"。"quine 是 f = Print 时的特例"是对的，但"quine 是先有 f 反求 c、SRT 是先有 c 对任意 f 都成立"是错的——SRT 证明里 c '''也是''' f 的函数（换一个 f 就换一个 c）。SRT 真正比 quine 强的地方只有一点：'''它证明了"先有 f、再造 c"这种构造对所有全可计算 f 都成立'''，而 quine 只演示了 f = Print 一个特例；SRT 给的不是"一个程序"，而是"对每个 f 都有一个程序（f 的不动点 c）"这样的普遍性陈述。这也解释了为何 SRT 在可计算性文献中被称为"second recursion theorem"——它把"quine 这种特例的构造手法"摆到了"自指可计算函数的普遍刻画"这一位置，把 quine 从"程序员的奇技"升格为"任何合理程序系统都封不住自指"的元定理。
也就是说，'''SRT 证明与 quine 不是"互逆"，而是同构'''——两者都是"先有一个具体的全可计算函数 f、再造一个不动点程序 c 满足 <math>\phi_c = \phi_{f(c)}</math>"。"quine 是 f = Print 时的特例"是对的，但"quine 是先有 f 反求 c、SRT 是先有 c 对任意 f 都成立"是错的——SRT 证明里 c '''也是''' f 的函数（换一个 f 就换一个 c）。SRT 真正比 quine 强的地方只有一点：'''它证明了"先有 f、再造 c"这种构造对所有全可计算 f 都成立'''，而 quine 只演示了 f = Print 一个特例；SRT 给的不是"一个程序"，而是"对每个 f 都有一个程序（f 的不动点 c）"这样的普遍性陈述。这也解释了为何 SRT 在可计算性文献中被称为"second recursion theorem"——它把"quine 这种特例的构造手法"摆到了"自指可计算函数的普遍刻画"这一位置，把 quine 从"程序员的奇技"升格为"任何合理程序系统都封不住自指"的元定理。
'''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是：
'''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是：
|Lawvere 抽象成分|SRT 实例化|
{| class="wikitable"
|---|---|
|-
|Cartesian 闭范畴 C|取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi</math>: <math>\mathbb{N}^k</math> ⇀ <math>\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴）|
! Lawvere 抽象成分
|函子 F|适当选取（C 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 F 取作"按编号 e 取 <math>\phi_e</math>" 的函子|
! SRT 实例化
|满射态射 f: A <math>\to F(A)</math>|取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 e 看作可枚举的元素、保证 F(A) 的每个元素都能表示为"以 f(e) 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 e <math>\mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）|
|-
|任意态射 g: F(A) <math>\to A</math>|取 g = SRT 推论里那个'''给定的全可计算函数 f'''（"按它编程序"）。注意：SRT 表述要求 f: <math>\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"f 处处有定义"这一约束，保证 g 在 F(A) 的全部范围内都有意义。|
| Cartesian 闭范畴 C
|不动物 x: A <math>\to A</math>|正是 SRT 给出的那个'''不动点编号 c'''——它满足 F(c) ∘ f = g ∘ f，即 <math>\phi_c = \phi_{f(c)}</math>|
| 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi</math>: <math>\mathbb{N}^k</math> ⇀ <math>\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴）
|-
| 函子 F
| 适当选取（C 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 F 取作"按编号 e 取 <math>\phi_e</math>" 的函子
|-
| 满射态射 f: A <math>\to F(A)</math>
| 取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 e 看作可枚举的元素、保证 F(A) 的每个元素都能表示为"以 f(e) 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 e <math>\mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）
|-
| 任意态射 g: F(A) <math>\to A</math>
| 取 g = SRT 推论里那个'''给定的全可计算函数 f'''（"按它编程序"）。注意：SRT 表述要求 f: <math>\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"f 处处有定义"这一约束，保证 g 在 F(A) 的全部范围内都有意义。
|-
| 不动物 x: A <math>\to A</math>
| 正是 SRT 给出的那个'''不动点编号 c'''——它满足 F(c) ∘ f = g ∘ f，即 <math>\phi_c = \phi_{f(c)}</math>
|}
'''关系定性'''：
'''关系定性'''：
两个维度交叉，得到下表：
两个维度交叉，得到下表：
| |'''否定性结论'''（证否某物）|'''肯定性结论'''（证实某物存在）|
{| class="wikitable"
| --------------------- | ----------------------- | --------------------------------- |
|-
|'''纯集合论'''（SRT 够不着）|Cantor 不可数、Russell 悖论|（无）|
!
|'''程序 / 可计算'''（SRT 够得着）|'''Turing 停机、Gödel 不完备'''|von Neumann 自复制、quine、自省程序、SRT 本身|
! '''否定性结论'''（证否某物）
! '''肯定性结论'''（证实某物存在）
|-
| '''纯集合论'''（SRT 够不着）
| Cantor 不可数、Russell 悖论
| （无）
|-
| '''程序 / 可计算'''（SRT 够得着）
| '''Turing 停机、Gödel 不完备'''
| von Neumann 自复制、quine、自省程序、SRT 本身
|}
由此看清每个现象的双重身份：'''Turing 停机、Gödel 不完备'''在"风格"上是否定性自指（与 Cantor、Russell 同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；Cantor、Russell 活在纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
由此看清每个现象的双重身份：'''Turing 停机、Gödel 不完备'''在"风格"上是否定性自指（与 Cantor、Russell 同类），但它们活在程序世界，所以'''又能被 SRT 事后统一推出'''；Cantor、Russell 活在纯集合论世界，SRT 造不出"实数"或"集合"，只能算'''同源但独立'''。下面逐个讲清楚。
=== 应用地图一览 ===
=== 应用地图一览 ===
|领域|代表性结果|SRT 的角色|
{| class="wikitable"
| -------- | -------------------------------------- | ------------------- |
|-
|r.e. 索引集理论|Rice 定理；Rice-Shapiro；Myhill：创造集 = 完备集|前两者：同源但独立（非 SRT）；Myhill：构造"监控自己"的程序〔§2〕|
! 领域
|有效运算|Myhill–Shepherdson；KLS–Čeĭnin 连续性|证明单调性与连续性〔§§3–4〕|
! 代表性结果
|可证性逻辑|Solovay：GL 完备性|构造自指函数〔§6〕|
! SRT 的角色
|序数记号|通用系统、Kleene's O、<math>\omega_1^CK</math>|最初的用武之地〔§7〕|
|-
|超算术理论|Markwald–Spector；Spector 唯一性；HYP = <math>\Delta^1_1</math>|每个证明的归纳枢纽〔§§8–9〕|
| r.e. 索引集理论
|有效描述集合论|Suslin–Kleene；赋范归纳；编码引理|关系版/参数版 SRT〔§10〕|
| Rice 定理；Rice-Shapiro；Myhill：创造集 = 完备集
|高类型递归|Kleene 1959 体系；Jackson 定理|理论的第一块基石〔§11〕|
| 前两者：同源但独立（非 SRT）；Myhill：构造"监控自己"的程序〔§2〕
|直觉主义数学|可实现性、bar 递归合法性|验证自指定义〔§12〕|
|-
|函数式编程|Y 组合子的推广、部分求值|元编程的不动点原理<ref name="kiselyov" />|
| 有效运算
| Myhill–Shepherdson；KLS–Čeĭnin 连续性
| 证明单调性与连续性〔§§3–4〕
|-
| 可证性逻辑
| Solovay：GL 完备性
| 构造自指函数〔§6〕
|-
| 序数记号
| 通用系统、Kleene's O、<math>\omega_1^CK</math>
| 最初的用武之地〔§7〕
|-
| 超算术理论
| Markwald–Spector；Spector 唯一性；HYP = <math>\Delta^1_1</math>
| 每个证明的归纳枢纽〔§§8–9〕
|-
| 有效描述集合论
| Suslin–Kleene；赋范归纳；编码引理
| 关系版/参数版 SRT〔§10〕
|-
| 高类型递归
| Kleene 1959 体系；Jackson 定理
| 理论的第一块基石〔§11〕
|-
| 直觉主义数学
| 可实现性、bar 递归合法性
| 验证自指定义〔§12〕
|-
| 函数式编程
| Y 组合子的推广、部分求值
| 元编程的不动点原理<ref name="kiselyov" />
|}
（表中"§"编号均指 Moschovakis 2010 的章节。）
（表中"§"编号均指 Moschovakis 2010 的章节。）