更改

=== 通用程序（解释器） ===

=== 通用程序（解释器） ===

存在一台"通用机器"：给它输入 <math>(e, x)</math>，它就'''模拟'''编号 <math>e</math> 的程序在输入 <math>x</math> 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的[[通用图灵机]]是它的首个化身。用记号写就是：存在程序<math>i</math> 使得 <math>\phi_i(e, x) = \phi_e(x)</math>。<ref name="rogers1967" />

存在一台"通用机器"：给它输入 <math>(e, x)</math>，它就'''模拟'''编号 <math>e</math> 的程序在输入 <math>x</math> 上的运行。这就是今天的'''解释器 / 虚拟机'''思想，Turing 1936 年的[[通用图灵机]]是它的首个化身。用记号写就是：存在程序<math>i</math> 使得 <math>\phi_i(e, x) = \phi_e(x)</math><ref name="rogers1967" />。

=== s-m-n 定理（柯里化 / 参数特化） ===

=== s-m-n 定理（柯里化 / 参数特化） ===

: <math>\phi_n = \phi_{f(n)}</math>

: <math>\phi_n = \phi_{f(n)}</math>

这是 Rogers 的原话——"''Let f be any recursive function; then there exists an n such that <math>\phi_n = \phi_{f(n)}</math>.''"<ref name="rogers1967" />。意思是：<math>f</math> 拿着程序 <math>n</math> 的源代码算出一个新程序 <math>f(n)</math>，而'''新程序与旧程序计算的是同一个函数'''。<ref name="rogers1967" />

这是 Rogers 的原话——"''Let f be any recursive function; then there exists an n such that <math>\phi_n = \phi_{f(n)}</math>.''"<ref name="rogers1967" />。意思是：<math>f</math> 拿着程序 <math>n</math> 的源代码算出一个新程序 <math>f(n)</math>，而'''新程序与旧程序计算的是同一个函数'''<ref name="rogers1967" />。

'''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 <math>y</math>——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 <math>e</math> 的程序在参数 <math>y</math> 下的行为"。那么存在一个可计算的全函数 <math>z</math>：你输入 <math>y</math>，它就输出针对这个参数的不动点编号 <math>z(y)</math>，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 <math>x</math> 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 <math>y</math> 给出不同的编号（<math>z</math> 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />

'''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 <math>y</math>——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 <math>e</math> 的程序在参数 <math>y</math> 下的行为"。那么存在一个可计算的全函数 <math>z</math>：你输入 <math>y</math>，它就输出针对这个参数的不动点编号 <math>z(y)</math>，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 <math>x</math> 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 <math>y</math> 给出不同的编号（<math>z</math> 是'''单射'''，即一对一）<ref name="rogers1967" /><ref name="moschovakis2010" />。

=== 推论：SRT 衍生出的若干重要结果 ===

=== 推论：SRT 衍生出的若干重要结果 ===

'''现象'''：考虑 <math>R = \{x : x \notin x\}</math>（所有"不属于自己"的集合组成的集合）。问 <math>R\in R</math> 是否成立？若 <math>R\in R</math>，则按定义 <math>R\notin R</math>；若 <math>R\notin R</math>，则按定义 <math>R\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论<ref name="russell1908">'''Russell, B. (1908).''' Mathematical logic as based on the theory of types. ''American Journal of Mathematics'', 30, 222–262.【罗素悖论的现代陈述】</ref>。

'''现象'''：考虑 <math>R = \{x : x \notin x\}</math>（所有"不属于自己"的集合组成的集合）。问 <math>R\in R</math> 是否成立？若 <math>R\in R</math>，则按定义 <math>R\notin R</math>；若 <math>R\notin R</math>，则按定义 <math>R\in R</math>。两边都矛盾，这个悖论动摇了朴素集合论<ref name="russell1908">'''Russell, B. (1908).''' Mathematical logic as based on the theory of types. ''American Journal of Mathematics'', 30, 222–262.【罗素悖论的现代陈述】</ref>。

'''与 SRT 的关系：同源，但独立'''。罗素悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"<math>e\in W_e</math>"，就得到 <math>K = \{e : e\notin W_e\}</math>——<math>K</math> 可枚举、其补集不可枚举。而"<math>K</math> 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的罗素悖论"，但罗素悖论本身与SRT只是同源关系。<ref name="russell1908" /><ref name="rogers1967" />

'''与 SRT 的关系：同源，但独立'''。罗素悖论也是"把谓词'不属于自身'同时用于所有集合"的对角线操作，和 SRT 共享同一个技巧，但 SRT 同样'''推不出'''它——它是朴素集合论内部的问题，不涉及程序。真正值得注意的，是 Rogers 指出的一个'''类比'''：把"集合"换成"可枚举的集合 <math>W_e</math>"、把"<math>\in</math>"换成"<math>e\in W_e</math>"，就得到 <math>K = \{e : e\notin W_e\}</math>——<math>K</math> 可枚举、其补集不可枚举。而"<math>K</math> 的补集不可枚举"恰好'''等价于停机问题不可判定'''（见 5.7.3），后者才是 SRT 真正推得出来的。换言之，"停机问题不可判定"可以看作"递归论版的罗素悖论"，但罗素悖论本身与SRT只是同源关系<ref name="russell1908" /><ref name="rogers1967" />。

==== 图灵停机问题（1936） ====

==== 图灵停机问题（1936） ====

: <math>H_\lambda = \cup_n H_{\lambda_n}</math>　（极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）

: <math>H_\lambda = \cup_n H_{\lambda_n}</math>　（极限层：把下面各层沿一条可计算上升的序列 <math>\lambda_0 < \lambda_1 < \lambda_2 < \ldots</math> 并起来——'''沿哪条序列取并由 <math>\lambda</math> 的代号给出'''，6.1 里"记号携带程序编号"的约定在此派上用场）

在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 5.7.4 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 6.4 的主题。<ref name="moschovakis2010" />

在某一层 <math>H_\alpha</math> 中可计算的集合，称为'''[[超算术的]]（hyperarithmetical, HYP）'''。这栋楼的前几层串起熟悉的图景：'''只盖有穷多层，得到的恰好是通常的算术层级'''——穷尽一阶算术（量词只作用于自然数）可定义的全部集合；盖到第 <math>\omega</math> 层（<math>\omega</math> 即 6.1 中最小的无穷序数），得到的集合已足以一举判定[[皮亚诺公理]]体系的全部真语句——包括所有皮亚诺公理体系证明不了的真命题（对照 5.7.4 的不完备性）；而楼并不停在这里，它沿构造序数一直盖到 <math>\omega_1^CK</math> 为止。HYP 因此是真正高于算术层级的层级——至于它究竟高到哪一步（恰好等价于一个"二阶量词"的定义能力），正是 6.4 的主题<ref name="moschovakis2010" />。

问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</math> 会不会不同？

问题来了：同一序数 <math>\alpha</math> 在系统中有'''无穷多个代号'''，用不同代号构造出的 <math>H_\alpha</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定理]]：[[创造集]] = [[完备集]] ====

证明的两个关键引理（变换必然是单调的、必然是连续的）都依赖 SRT：构造一个"监视 <math>\Phi</math> 是否已输出、在此之前模仿函数 <math>\phi_1</math>、之后叛变为函数 <math>\phi_2</math>"的程序 z——z 的行为取决于 z 自己（经 <math>\Phi</math> 处理后）的表现，由 SRT 提供，再用"同一函数的不同编号必须得到同一结果"逼出矛盾<ref name="moschovakis2010" />.

证明的两个关键引理（变换必然是单调的、必然是连续的）都依赖 SRT：构造一个"监视 <math>\Phi</math> 是否已输出、在此之前模仿函数 <math>\phi_1</math>、之后叛变为函数 <math>\phi_2</math>"的程序 z——z 的行为取决于 z 自己（经 <math>\Phi</math> 处理后）的表现，由 SRT 提供，再用"同一函数的不同编号必须得到同一结果"逼出矛盾<ref name="moschovakis2010" />.

'''Kreisel–Lacombe–Shoenfield–Čeĭnin 定理（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现。<ref name="moschovakis2010" />

'''Kreisel–Lacombe–Shoenfield–Čeĭnin 定理（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现<ref name="moschovakis2010" />.

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。