3,094
个编辑
更改
跳到导航
跳到搜索
第200行：
第200行： − + − # 对 <math>\psi_1</math> 套 SRT 拿到不动点 <math>m</math>；+ − # <math>m</math> 唯一确定后，<math>n</math> 由 <math>\phi_n = \psi_2(m)</math> 的不动点结构给出。+ − − # **带参数的 SRT 造"第二号程序"**：把"程序算 <math>h(\langle z, u\rangle, x)</math>"看成带两个参数 <math>z,u</math> 的偏可计算函数，先由 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>； − −
→Smullyan 双递归定理（1959, 1961）
由于这个Smullyan双递归定理是 SRT 的"二元推广"，因此我们可直接由 SRT 的证明套用：
由于这个Smullyan双递归定理是 SRT 的"二元推广"，因此我们可直接由 SRT 的证明套用：
# 先用 s-m-n（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）构造两个可计算函数 <math>\psi_1(x) = g(S(x, x), x)</math>、<math>\psi_2(x) = h(S(x, x), x)</math>，二者均依赖自身编号；
# 带参数的 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> 也是全可计算的；
# 对 f 套普通 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> 的定义）。
# **再由 s-m-n 造"第一号程序"**：令 <math>f(z)</math> 为"算 <math>g(\langle z, n_0(z)\rangle, x)</math> 的那个程序"——由于 <math>n_0</math> 全且可计算，<math>f</math> 也是全可计算的；
# **对 f 套普通 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>g,h</math> 的"全性"从头到尾没有被用到——需要全函数的只是辅助构造 <math>n_0</math> 与 <math>f</math>，而它们的全性由 s-m-n 定理和 SRT 保证。这正是定理对偏函数照样成立的原因。