更改

可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。

可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析。

与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|6.5.3]]）。

与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 [[#Myhill定理：创造集 = 完备集|5.8.5.3]]）。

===== [[Rice定理]]（1951） =====

===== [[Rice定理]]（1951） =====

# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（[[#图灵停机问题（1936）|§5.7.3]]）。

# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（[[#图灵停机问题（1936）|§5.7.3]]）。

* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"，而那正是不可判定的对角线问题<ref name="rice1953">'''Rice, H. G. (1953).''' Classes of recursively enumerable sets and their decision problems. ''Transactions of the AMS'', 74, 358–366.【Rice 定理原始论文】【§6.5.1】</ref>.

* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"，而那正是不可判定的对角线问题<ref name="rice1953">'''Rice, H. G. (1953).''' Classes of recursively enumerable sets and their decision problems. ''Transactions of the AMS'', 74, 358–366.【Rice 定理原始论文】【§5.8.5.1】</ref>.

  '''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。

  '''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 <math>A</math> 可计算，取变换规则 <math>f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 <math>m</math> 使 <math>\phi_m = \phi_{f(m)}</math>。若 <math>m\in A</math>，则 <math>f(m)\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；<math>m\notin A</math> 同理。这条证明虽短，却是'''事后捷径'''——它没有揭示 Rice 定理与停机问题的血缘，而后者（上面的归约）才是定理的标准证明与本质机制<ref name="rogers1967" />。