更改

在[[曼纽尔·布卢姆|Blum]]的机器无关复杂性理论中，SRT 与对角化结合产生了一批"存在性"结果。代表性的一例：Helm 与 Young 回答了 Blum 的一个问题——存在这样的可计算函数，任何为它"换上更快的程序"的尝试都要付出程序尺寸爆炸的代价，且刻画这一代价的增长函数快于任何递归函数<ref name="helmyoung1971">'''Helm, J.; Young, P. (1971).''' ''On size vs. efficiency for programs admitting speed-ups''. Journal of Symbolic Logic 36.【回答 Blum 的问题：加速必然伴随尺寸爆炸，代价函数增长快于任何递归函数】</ref>。"加速与简洁不可兼得"由此成为定理而非格言。

在[[曼纽尔·布卢姆|Blum]]的机器无关复杂性理论中，SRT 与对角化结合产生了一批"存在性"结果。代表性的一例：Helm 与 Young 回答了 Blum 的一个问题——存在这样的可计算函数，任何为它"换上更快的程序"的尝试都要付出程序尺寸爆炸的代价，且刻画这一代价的增长函数快于任何递归函数<ref name="helmyoung1971">'''Helm, J.; Young, P. (1971).''' ''On size vs. efficiency for programs admitting speed-ups''. Journal of Symbolic Logic 36.【回答 Blum 的问题：加速必然伴随尺寸爆炸，代价函数增长快于任何递归函数】</ref>。"加速与简洁不可兼得"由此成为定理而非格言。

更微妙的是，我们能否把 SRT 本身复杂性化？如果把编号限制到多项式时间的程序族上，SRT 还成立吗？困难出在证明的两个枢纽操作上：通用模拟在 P-时间世界里没有多项式时间版本（万能解释器本身要超线性时间），s-m-n 实例化（把参数写死）也会放大运行时间。因此对一般的多项式时间编号，'''带时间界的 SRT 不成立'''；不过 Kleene 1938 年的直接证明不经过通用程序，所以某些没有通用程序的子递归系统仍保有递归定理。一句话主旋律：'''自指免费，高效自指昂贵'''——不动点的"存在"有保证，"存在得节省"没有。

更微妙的是，我们能否把 SRT 本身复杂性化？如果把编号限制到多项式时间的程序族上，SRT 还成立吗？困难出在证明的两个枢纽操作上：通用模拟在 P-时间世界里没有多项式时间版本（万能解释器本身要超线性时间），s-m-n 实例化（把参数写死）也会放大运行时间。因此对一般的多项式时间编号，'''带时间界的 SRT 不成立'''；不过 Kleene 1938 年的直接证明不经过通用程序，所以某些没有通用程序的子递归系统仍保有递归定理。一句话主旋律：'''自指免费，高效自指则昂贵'''——不动点的"存在"有保证，"节省地存在"则没有。

==== 存在性与可构造性的分野 ====

==== 存在性与可构造性的分野 ====