更改

递归定理 (查看源代码)

2026年9月12日 (六) 09:08的版本

大小无更改、 2026年9月12日 (星期六)

无编辑摘要

第242行：第242行：

: <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 的"列表法"证明（§[[#列表法（Cutland 1980）：把"对角线"画成一张表|5.3.2]]）】</ref>.

+

<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 的"列表法"证明（§[[#列表法（Cutland 1980）：把"对角线"画成一张表|5.2.2]]）】</ref>.

−

'''与"一行证明"的关系'''：[[#一行对角线|§5.3.1]] 的证明把表上 <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.2.1]] 的证明把表上 <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像素]]

第276行：第276行：

——用公式写就是 <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.1]] 那一行证明——给定 <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 输出层面）。两边共用同一种"自指核心动作"——'''让程序合法地把"自己的表示"当作输入'''：

+

'''SRT 的证明，本身就是一个 Quine 构造——而且方向和 quine 完全相同'''。再回看 [[#一行对角线|§5.2.1]] 那一行证明——给定 <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"

第294行：第294行：

| '''构造方向'''

| 先有具体 <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>f</math>（[[#证明|§5.2]] 假设中任意一个），再造 <math>c</math>（<math>c</math> 由对 <math>f</math> 套 SRT 得到）

|-

| '''目的'''

第430行：第430行：

|-

| 满射态射 <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.1]] 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）

+

| 取定 [[#"可计算"与"部分函数"|§2.1]] 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 [[#一行对角线|§5.2.1]] 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）

|-

| 任意态射 <math>g: F(A)\to A</math>

第443行：第443行：

* [[#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]] 的[[对角线论证]]）。

+

* 因此应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 [[#证明|§5.2]] 的[[对角线论证]]）。

−

'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[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 停机统一为范畴论特例】【§[[#Lawvere 不动点定理（1969）|5.6.2]]】</ref>。

+

'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，[[#证明|§5.2]] 的对角线证明就是你所需要的——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 停机统一为范畴论特例】【§[[#Lawvere 不动点定理（1969）|5.6.2]]】</ref>。

=== SRT与自指===

Jake

行政员、界面管理员、管理员

3,094

个编辑