| 第317行: |
第317行: |
| | | | |
| | === 其它形式的第二递归定理 === | | === 其它形式的第二递归定理 === |
| − | ====uniform==== | + | ====Uniform 不动点定理==== |
| | + | '''Uniform不动点定理''':存在一个全可计算函数<math>r</math>(在标准编号下甚至可以取原始递归的),使得对每一个编号<math>e</math>: |
| | + | |
| | + | :<math> |
| | + | \phi_{r(e)}(x) ≃ \phi_e(r(e), x)(\forall x) |
| | + | </math> |
| | + | |
| | + | 三个要点: |
| | + | |
| | + | * 输入是<math>\psi</math> 本身的编号。前面所有版本里 <math>\psi</math> 都是“给定的”:表述 A 对给定的 <math>\psi</math> 断言不动点存在;表述 C 让不动点随参数 <math>u</math> 一致变化。Uniform 版的方向不同——它让不动点随 <math>\psi</math> 的描述(编号) 一致变化:<math>r</math> 是一个“自指编译器”,你喂给它任何一个二元程序的编号,它返回那个让 <math>\phi_e(·,·)</math> 自我指涉的程序编号。 |
| | + | * 无条件的全称命题。注意陈述里没有“若 <math>\phi_e</math> 可计算”之类的前提——对一切 <math>e</math> 都成立。<math>e</math>号程序在 <math>(r(e), x)</math> 上不停机时,两边同时无定义,等式照样成立。这跟“fixed-point free 函数必须是不可计算的”(Arslanov 判据)是一体两面:<math>r</math> 是全的,所以没有可计算函数能躲开它。 |
| | + | * 构造性到什么程度:把 §5.3 展开版证明逐步查一遍——第 0 步用 s-m-n 造 <math>\theta</math> 的编号(原始递归操作),第 2 步 <math>f = S(e,e)</math>(S 原始递归)——每一步都是编号上的原始递归运算。所以复合出来的 <math>e \iff f</math> 就是那个 <math>r</math>,原始递归。这也是为什么说 Kleene 1938/1952 的原始证明“实际上已经是 uniform 的”:证明即算法。 |
| | + | |
| | ====Smullyan双递归定理==== | | ====Smullyan双递归定理==== |
| | | | |