| 第322行： |
第322行： |
| | === 推论：SRT 衍生出的若干重要结果 === | | === 推论：SRT 衍生出的若干重要结果 === |
| | | | |
| − | SRT 不是孤岛，但也不能把整片大陆都记在它名下。本节收录三条'''真正以 SRT 为证明枢纽'''的结果——它们的证明都必经 SRT，称"推论"名副其实： | + | SRT 不是孤岛，但也不能把整片大陆都记在它名下。本节收录两条'''真正以 SRT 为证明枢纽'''的结果——它们的证明都必经 SRT，称"推论"名副其实： |
| | | | |
| − | * '''[[Smullyan 双递归定理]]'''——SRT 的"联立化"推广：一次造出两个互相引用对方代码的程序（可推广到 <math>k</math> 个），是后续许多构造的通用工具；
| |
| | * '''[[Rogers 同构定理]]'''——SRT 的"编号[[独立性 (数学)|独立性]]"推论：任意两个[[通用图灵机|通用程序]]枚举之间必有保结构的可计算同构； | | * '''[[Rogers 同构定理]]'''——SRT 的"编号[[独立性 (数学)|独立性]]"推论：任意两个[[通用图灵机|通用程序]]枚举之间必有保结构的可计算同构； |
| | * '''[[Arslanov 完全性判据]]'''——相对化 SRT 的"刻画性"等价定理：一个 r.e. 集何时是 [[r.e.-完备的]]。 | | * '''[[Arslanov 完全性判据]]'''——相对化 SRT 的"刻画性"等价定理：一个 r.e. 集何时是 [[r.e.-完备的]]。 |
| − |
| |
| − | ==== Smullyan 双递归定理（1959, 1961） ====
| |
| − |
| |
| − | '''SRT 的联立推广'''：对任意两个可计算函数 <math>g</math>, <math>h</math>（不一定要求是全函数），存在两个程序 <math>m, n</math> 使得
| |
| − |
| |
| − | : <math>
| |
| − | \phi_m(x) = g(\langle m, n\rangle, x);\qquad
| |
| − | \phi_n(x) = h(\langle m, n\rangle, x)
| |
| − | </math>
| |
| − |
| |
| − | ——两个程序可以'''互相引用对方的代码'''，其中<math>\langle m,n\rangle</math>代表将两个自然数编码为一个自然数的编码方式。
| |
| − |
| |
| − | 由于这个Smullyan双递归定理是 SRT 的"二元推广"，因此我们可直接由 SRT 的证明套用：
| |
| − |
| |
| − | # 带参数的 SRT 造"第二号程序"：把"程序算 <math>h(\langle z, u\rangle, x)</math>"看成带两个参数 <math>z,u</math> 的偏可计算函数，先由 s-m-n（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）把 <math>z</math> 写死，再套 SRT，得到一个'''全'''可计算函数 <math>n_0</math>，对每个 <math>z</math> 都满足 <math>\phi_{n_0(z)}(x) = h(\langle z, n_0(z)\rangle, x)</math>；
| |
| − | # 再由 s-m-n 造"第一号程序"：令 <math>f(z)</math> 为"算 <math>g(\langle z, n_0(z)\rangle, x)</math> 的那个程序"——由于 <math>n_0</math> 全且可计算，<math>f</math> 也是全可计算的；
| |
| − | # 对 <math>f</math> 套普通 SRT：得到不动点 <math>m</math>，令 <math>n = n_0(m)</math>。于是 <math>\phi_m(x) = g(\langle m, n\rangle, x)</math>（SRT 的直接结论），且 <math>\phi_n(x) = h(\langle m, n_0(m)\rangle, x) = h(\langle m, n\rangle, x)</math>（<math>n_0</math> 的定义）。
| |
| − |
| |
| − | 注意 <math>g,h</math> 的"全性"从头到尾没有被用到——需要全函数的只是辅助构造 <math>n_0</math> 与 <math>f</math>，而它们的全性由 s-m-n 定理和 SRT 保证。这正是定理对偏函数照样成立的原因。
| |
| − |
| |
| − | 推广到 <math>k</math> 元：对任意 <math>k</math> 个全可计算函数 <math>g_1</math>, <math>\ldots</math>, <math>g_k</math>，存在 <math>k</math> 个程序 <math>m_1</math>, <math>\ldots</math>, <math>m_k</math> 使得 <math>\phi_{m_i}(x) = g_i(\langle m_1, \ldots, m_k\rangle, x)</math>。
| |
| − |
| |
| − | [[#Smullyan 双递归定理（1959, 1961）|双递归定理]]是后续许多重要构造的核心：① [[#超算术层级与 Spector 唯一性定理|§5.8.3]] 介绍的"两层超算术构造"里，[[克利福德·斯佩克特|Spector]] 定理需要同时构造两个互相缠绕的函数；② [[Myhill-Shepherdson 定理]]（[[#有效运算的连续性：Myhill–Shepherdson 与 KLS–Čeĭnin 定理|§5.8.6]] 简述）描述"如何用 r.e. 集作为其它 r.e. 集的有效操作"时也需要联立不动点；③ 某些停机问题的"相对化"证明也走双递归路线<ref name="smullyan1961">'''Smullyan, R. M. (1961).''' ''Theory of Formal Systems''. Princeton University Press.【双递归定理的提出者；§[[#Smullyan 双递归定理（1959, 1961）|5.5.1]]】</ref><ref name="rogers1967" />.
| |
| − |
| |
| − | 另外，值得一提的是，这个双递归定理以及对应的n递归定理的推广形式，实际上可以看成是多个部分互相指涉，互相依赖的形式，因此也就构成了[[自创生理论]]（Autopoesis）的数学基础。
| |
| | | | |
| | ==== Rogers 同构定理（1958） ==== | | ==== Rogers 同构定理（1958） ==== |