更改

上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。[[奈杰尔·卡特兰|Cutland]] 在《Computability》<ref name="cutland"/> §2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。

上面的一行证明把对角线方法压缩到了极致——好处是直接，坏处是看不出"对角线"长什么样。[[奈杰尔·卡特兰|Cutland]] 在《Computability》<ref name="cutland"/> §2.3 (Theorem 2.3) 给出过一种更直观的'''列表法'''证明，'''用一张"行 = 枚举、列 = 位置"的二维表，把"对角线"和"沿对角线的循环"都画在纸面上'''。三步走。

'''1. 把"所有可计算函数的枚举"摆成一张表'''

# 把"所有可计算函数的枚举"摆成一张表

按 §2.2，每个可计算部分函数都有一个编号；所有这种编号的全体记作 {<math>\phi_k</math>}。对任意"枚举函数" E（把一列编号映射成一列可计算函数），E 的第 n 项就是 <math>\phi_{E(n)}</math>，即"编号为 E(n) 的程序"。现在考虑'''所有"可计算函数的枚举"'''——它们每一个都是某个可计算函数 h。Cutland 把它们自身也排成一张表：用编号为 k 的程序 <math>\phi_k</math> 自己去枚举，得到

按 §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> 的第 n 项 = <math>\phi_{\phi_k(n)}</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> 是一个枚举'''、'''每列 n 是"该行第 n 个值"'''、'''每格是某个具体的可计算函数'''。这张表把"枚举可计算函数的所有方式"完整地、不重不漏地列了出来。

——双重编号 <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. 对角线枚举 D'''

# 对角线枚举<math>D</math>

把这张表沿'''主对角线'''的格子圈出来——它们正是

把这张表沿'''主对角线'''的格子圈出来——它们正是

> D = ( <math>\phi_\phi_0(0)</math>,  <math>\phi_\phi_1(1)</math>, <math>\phi_\phi_2(2)</math>, <math>\ldots</math> )

: <math>D = (\phi_\phi_0(0),  \phi_\phi_1(1), \phi_\phi_2(2),\ldots)</math>

D 仍然是一个可计算的枚举：由 h(x) = <math>\phi_x(x)</math> 给出（图 6 黄底一行的"沿主对角线"）。它满足一个关键性质：

<math>D</math> 仍然是一个可计算的枚举：由 <math>h(x) = \phi_x(x)</math> 给出（图 6 黄底一行的"沿主对角线"）。它满足一个关键性质：

> '''D 和每行 <math>E_k</math> 都共享一项：第 (k+1) 项都是 <math>\phi_\phi_k(k)</math>'''

: '''<math>D</math> 和每行 <math>E_k</math> 都共享一项：第 <math>(k+1)</math> 项都是 <math>\phi_\phi_k(k)</math>'''

——因为 <math>E_k</math> 的第 (k+1) 项 = <math>\phi_\phi_k(k)</math>，而 D 的第 (k+1) 项 = <math>\phi_\phi_k(k)</math>，两者恰好对得上（图 6 右侧红字注释）。

——因为 <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. 沿 D 把 f 套进去，得到 f 的不动点'''

# 沿 <math>D</math> 把 <math>f</math> 套进去，得到 <math>f</math> 的不动点

设 f 是任意全可计算函数。沿 D 的每一项先用 f 变一下号，再去取对应的可计算函数，得到另一个枚举：

设 <math>f</math> 是任意全可计算函数。沿 <math>D</math> 的每一项先用 <math>f</math> 变一下号，再去取对应的可计算函数，得到另一个枚举：

> D* = ( <math>\phi_{f(\phi_0(0))}</math>, <math>\phi_{f(\phi_1(1))}</math>, <math>\phi_{f(\phi_2(2))}</math>, <math>\ldots</math> )

# <math>D^* = (\phi_{f(\phi_0(0))},\phi_{f(\phi_1(1))}, \phi_{f(\phi_2(2))},\ldots)</math>

D* 也可计算（由 f(h(x)) 给出）——既然 D* 本身也是"枚举可计算函数"的一种方式，它'''必然是表里某一行 <math>E_m</math>'''。这正是循环闭合的地方：套用 f 之后，必然撞回表内。

<math>D^*</math> 也可计算（由 <math>f(h(x))</math> 给出）——既然 <math>D^*</math> 本身也是"枚举可计算函数"的一种方式，它'''必然是表里某一行 <math>E_m</math>'''。这正是循环闭合的地方：套用 <math>f</math> 之后，必然撞回表内。

取 k = m：D* = <math>E_m</math>，所以 D* 的第 (m+1) 项 = <math>E_m</math> 的第 (m+1) 项 = <math>\phi_\phi_m(m)</math>。而 D* 的第 (m+1) 项由定义也是 <math>\phi_{f(\phi_m(m))}</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>：

> <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>

# <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>

Cutland 用 Lemma 2.1 把"第 m 行"调整成全的（即 <math>\phi_m</math> 是全函数），所以 <math>\phi_m(m)</math> 是一个良定的自然数 n。设 n = <math>\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>\phi_n = \phi_{f(n)}</math>

n 就是 f 的不动点 ∎。<ref name="cutland1980" />

<math>n</math> 就是 <math>f</math> 的不动点 ∎。<ref name="cutland1980" />

'''与"一行证明"的关系'''：§5.3 的证明把表上 D* = <math>E_m</math> 的循环直接写成 <math>\psi(S(e,e), x)</math> 的柯里化形式——h(x) = <math>\phi_x(x)</math> 对应"e = 编号(<math>\psi(S(y,y), x)</math>)"，S(e,e) 就是用自应用把表上的对角线点亮；'''列表法只是把这一行在表格里完整地展开'''。两者本质相同：列表法暴露了"为什么沿对角线循环必会撞回表里"——'''每行 <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> 都被对角线穿一格，循环天然闭合'''。



'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>E_k</math>，每格填 <math>\phi_\phi_i(j)</math>；主对角线（红圈）上的格子构成对角枚举 D。'''黄底 D 行'''：把对角线上的格子抽出，得到 D = (<math>\phi_\phi_0(0)</math>, <math>\phi_\phi_1(1)</math>, <math>\phi_\phi_2(2)</math>, <math>\ldots</math>)。*''D'' 行*''：把 f 套到 D 上得到 D'' = (<math>\phi_{f(\phi_0(0))}</math>, <math>\phi_{f(\phi_1(1))}</math>, <math>\ldots</math>)——可计算 <math>\Rightarrow </math>必是某行 <math>E_m</math>。'''绿框'''：取 k = m 撞上 <math>E_m</math>，得 <math>\phi_\phi_m(m) = \phi_{f(\phi_m(m))}</math>，再设 n = <math>\phi_m(m)</math> 即得 <math>\phi_n = \phi_{f(n)}</math>——f 的不动点。

'''图6'''：Cutland (1980) 列表法证明的视觉化。'''上半'''：四行四列的"枚举之枚举"表 <math>E_0</math>, <math>E_1</math>, <math>E_2</math>, <math>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> 的不动点。

=== 直观图景：程序如何"谈论"自己的代码 ===

=== 直观图景：程序如何"谈论"自己的代码 ===