更改

: <math>A = \{ e : W_e \in \mathcal{A}\}</math>

: <math>A = \{ e : W_e \in \mathcal{A}\}</math>

（换成函数视角就是 <math>A = { e : \phi_e</math> 具有性质 <math>\mathcal{A}\}</math> 。）可判定、可枚举这类词只能作用于自然数集合，索引集正是那道翻译层——它把"程序行为问题"转写成 <math>\mathbb{N}</math> 的子集，之后才能问"这个性质能判定吗、能枚举吗"。两个要点：其一，此类性质必须'''只看行为、不看代码'''（同一函数的两个不同编号在 A 中必须同真同假），否则退化为平凡的代码分析；其二，记号上 '''r.e.'''（computably enumerable，可计算可枚举）就是 §2.4 的 '''r.e.''' 的现代同义词，二者完全等价。

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

与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 6.5.3）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 §5.2 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。

与 SRT 的关系必须先分清：下面三个结果中，'''只有 Myhill 定理是 SRT 的应用'''（其证明核心是"程序 z 引用 z 自己的编号"，见 6.5.3）；'''Rice 与 Rice-Shapiro 不是 SRT 的推论'''——它们的标准证明分别是停机归约（对角线矛盾）与有限集/紧致性论证，全程不需要 SRT，SRT 至多给 Rice 提供一条事后捷径。也就是说，Rice 家族与 SRT"同源，但独立"：共享对角线血统，却不靠 SRT 的代码不动点力量成立。Rice 家族因此不宜与双递归定理等并列在 §5.2 的"推论"名义之下；本文把它们放在本板块，与 Myhill 定理并置，正是为了并排呈现"独立成立"与"依赖 SRT"这两种截然不同的关系。

==== Rice 定理（1951） ====

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

'''陈述'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 A = { e : <math>\phi_e \in \mathcal{A}</math> } 不是可计算集（更不是递归集）。

'''陈述'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。

'''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：

* '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：

1. 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；

# 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；

2. 对每个 x，用 S-m-n 定理（§2.3）机械地造一个程序 h(x)：它先模拟"程序 x 在输入 x 上"的运行——这一步是对角线（让 x 面对自己的行为）；一旦该模拟停机，h(x) 就转而执行程序 a；若模拟永不停机，h(x) 也永不停机；

# 对每个 <math>x</math>，用 s-m-n 定理（§2.3）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；

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

直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 x 停在自己身上吗"，而那正是不可判定的对角线问题。<ref name="rice1953" />

* 直觉：任何非平凡的"行为分类"都把停机问题吸收为自己内部的一个子问题——你若想机械地给每个程序的行为贴标签，就不得不先回答"程序 <math>x</math> 停在自己身上吗"，而那正是不可判定的对角线问题。<ref name="rice1953" />

> '''注（SRT 捷径，非本质）'''：[[莱斯定理|Rice 定理]]也可用 SRT 三行证完：设 A 可计算，取变换规则 f(x) = "x <math>\in A</math> 时给一个 <math>\notin A</math> 的编号，否则给一个 <math>\in A</math> 的编号"（A 非空非全，顺序搜索即可机械实现），SRT 给出不动点 m 使 <math>\phi_m = \phi_{f(m)}</math>。若 m <math>\in A</math>，则 f(m) <math>\notin A</math>，同一函数 <math>\phi_m = \phi_{f(m)}</math> 却一个在 A 内、一个在 A 外（索引集只看行为），矛盾；m <math>\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" />。

==== Rice-Shapiro 定理（1956） ====

==== Rice-Shapiro 定理（1956） ====

Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：

Rice 定理回答"'''能否'''判定"；[[莱斯-夏皮罗定理|Rice-Shapiro 定理]]进一步刻画"'''何时能半判定'''"——把注意力从"A 是否可计算"收窄到"A 自身何时是 r.e. 的"：

> 设 A = { e : <math>W_e \in \mathcal{A}</math> } 是索引集。A 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 𝒮 = {<math>S_0</math>, <math>S_1</math>, <math>S_2</math>, <math>\ldots</math>}，使得 W <math>\in \mathcal{A}</math> ⟺ 𝒮 中存在某个 <math>S_i \subseteq W</math>。

设 <math>A = \{ e :W_e \in \mathcal{A}\}</math> 是索引集。A 是 r.e. 的，'''当且仅当''' <math>\mathcal{A}</math> 是"有限可生成"的：存在一个可计算列举的有限集列 <math>\mathcal{S} = \{S_0,S_1,S_2,\ldots</math>}，使得 <math>W\in \mathcal{A}</math> ⟺ <math>\delta</math>中存在某个 <math>S_i \subseteq W</math>。

含义：一个行为性质若能'''被枚举地识别'''（索引集 r.e.），它就必须由'''有限证据'''决定——W 一旦包含某个预列的有限集 <math>S_i</math>，性质即成立；反之，性质成立也只需某个有限子集作证。"能识别 ⟹ 只依赖有限信息"这一半是紧致性式的论证（若性质的成立只靠无限多证据，枚举过程就永远等不到决定性的一刻）；"有限可生成 ⟹ 可枚举"那一半是直接列举。两个方向都与 SRT 无关。

含义：一个行为性质若能'''被枚举地识别'''（索引集 r.e.），它就必须由'''有限证据'''决定——W 一旦包含某个预列的有限集 <math>S_i</math>，性质即成立；反之，性质成立也只需某个有限子集作证。"能识别 ⟹ 只依赖有限信息"这一半是紧致性式的论证（若性质的成立只靠无限多证据，枚举过程就永远等不到决定性的一刻）；"有限可生成 ⟹ 可枚举"那一半是直接列举。两个方向都与 SRT 无关。

Rice-Shapiro 不是 SRT 的推论，而是索引集理论中独立的结构定理，并且它比 Rice 定理更强——由它可以推出 Rice 定理：若非平凡索引集 A 可计算，则 A 与补集都是 r.e. 索引集，Rice-Shapiro 给 <math>\mathcal{A}</math> 与其补类都套上"有限可生成"；而有限可生成自动蕴含"超集仍在类中"，把两个类里各自的成员并起来，就得到同时属于两类的一个 r.e. 集，矛盾。可见在"识别程序性质"的问题上，真正的母定理是 Rice-Shapiro 而非 SRT。<ref name="rogers1967" /><ref name="soare1987" />

Rice-Shapiro 不是 SRT 的推论，而是索引集理论中独立的结构定理，并且它比 Rice 定理更强——由它可以推出 Rice 定理：若非平凡索引集 A 可计算，则 A 与补集都是 r.e. 索引集，Rice-Shapiro 给 <math>\mathcal{A}</math> 与其补类都套上"有限可生成"；而有限可生成自动蕴含"超集仍在类中"，把两个类里各自的成员并起来，就得到同时属于两类的一个 r.e. 集，矛盾。可见在"识别程序性质"的问题上，真正的母定理是 Rice-Shapiro 而非 SRT。<ref name="rogers1967" /><ref name="soare1987" />

==== Myhill 定理：创造集 = 完备集 ====

==== [[Myhill定理]]：[[创造集]] = [[完备集]] ====

'''背景'''：停机问题集合 K = {e : 程序 e 在输入 e 上停机} 是 r.e. 集中"最不可判定"的——任何 r.e. 集都能通过可计算的翻译归约到它（称为 '''r.e.-完备'''，complete）。另有一个看似完全不同的概念：一个 r.e. 集 A 称为'''创造集（creative set）'''，如果它的补集是"能系统地生产反例"的——存在一个可计算程序，你给它任何与 A 不交的 r.e. 集，它都能吐出一个既不在 A 里也不在那个集合里的元素。创造性是 Post 1944 年为刻画"不可判定的源泉"而引入的概念。

'''背景'''：停机问题集合 K = {e : 程序 e 在输入 e 上停机} 是 r.e. 集中"最不可判定"的——任何 r.e. 集都能通过可计算的翻译归约到它（称为 '''r.e.-完备'''，complete）。另有一个看似完全不同的概念：一个 r.e. 集 A 称为'''创造集（creative set）'''，如果它的补集是"能系统地生产反例"的——存在一个可计算程序，你给它任何与 A 不交的 r.e. 集，它都能吐出一个既不在 A 里也不在那个集合里的元素。创造性是 Post 1944 年为刻画"不可判定的源泉"而引入的概念。

> '''定理（Myhill 1955）'''：每个创造集都是 r.e.-完备的；两个概念重合。<ref name="myhill1955" /><ref name="rogers1967" /><ref name="moschovakis2010" />

* '''定理（Myhill 1955）'''：每个创造集都是 r.e.-完备的；两个概念重合<ref name="myhill1955" /><ref name="rogers1967" /><ref name="moschovakis2010" />.

'''证明中 SRT 的关键一步'''：想把任意 r.e. 集 B 归约到创造集 A，需要构造一个程序 z，使得"若 x <math>\in B</math>，则 z 枚举出 {u(z)}；否则 z 枚举空集"——'''z 的定义里用到了 z 自己的编号'''（u(z) 是生产反例的程序作用于 z）。这正是 SRT 合法化的自指；没有这个自指，证明无法闭合。由此 Rogers 还得到推论：'''所有创造集在"可计算的重新命名"意义下完全相同（两两递归同构）'''——从可计算性角度看它们"长得一模一样"<ref name="rogers1967" />。

'''证明中 SRT 的关键一步'''：想把任意 r.e. 集 B 归约到创造集 A，需要构造一个程序 z，使得"若 x <math>\in B</math>，则 z 枚举出 {u(z)}；否则 z 枚举空集"——'''z 的定义里用到了 z 自己的编号'''（u(z) 是生产反例的程序作用于 z）。这正是 SRT 合法化的自指；没有这个自指，证明无法闭合。由此 Rogers 还得到推论：'''所有创造集在"可计算的重新命名"意义下完全相同（两两递归同构）'''——从可计算性角度看它们"长得一模一样"<ref name="rogers1967" />。