“把程序代码作为普通数据,再用本定理固化自应用所需的参数,可以证明Kleene 递归定理:任意总可计算代码变换都存在语义固定点。固定点满足程序行为相同,而非索引数值相等。”
形式陈述 ​
固定偏可计算函数的可接受编号
存在索引
作为部分函数外延相等。固定点是程序行为的固定点;定理既不要求
证明使用$s$-$m$-$n$ 定理。取总可计算的对角专门化函数
由
是部分可计算的。令
于是对所有
每个等号都来自已定义的专门化或通用模拟,因而证明没有假设程序能够神秘地读取自身源码。带参数版本进一步说,若代码变换还依赖参数
直觉 ​
定理名称中的“递归”指可计算函数论传统,而不是普通编程语言中的递归调用。它保证的是语义自指,不要求运行栈、反射 API 或文件系统访问。
例子与边界 ​
Quine 是直观例子:可以构造一个程序,在无输入时输出自身描述。更一般地,若
这里的等号只比较部分函数。两个程序可有不同运行时间、内存访问、输出前副作用或源码文本,却在指定抽象输出语义下计算同一函数。若讨论的观察语义包含日志或外部状态,就必须先把它们编码进函数输出,不能偷偷扩大等价概念。
递归定理不判定程序语义,也不与停机问题冲突。它构造一个满足行为方程的索引,却通常不能决定该行为是否停机或具有某个非平凡性质。
推论与应用 ​
递归定理是自复制程序、自描述系统和许多不可判定性证明的统一工具。Rice 定理的某些加强形式可借带参数递归定理构造会根据分析器预测反向行动的程序;病毒或自更新代码模型也用它说明代码可将自身描述纳入计算。
可接受编号保证通用解释与有效编译,
参考资料
- Stephen C. Kleene, Introduction to Metamathematics, North-Holland, 1952, §§52–53, recursion theorems.
- Hartley Rogers Jr., Theory of Recursive Functions and Effective Computability, MIT Press, 1987, Ch. 11, the recursion theorem.
- Nigel Cutland, Computability: An Introduction to Recursive Function Theory, Cambridge University Press, 1980, Ch. 11.