Skip to content

Kleene 递归定理

Kleene recursion theorem · Kleene fixed-point theorem

每个总可计算的程序代码变换都存在一个与其变换结果计算同一偏函数的程序索引。

形式陈述

固定偏可计算函数的可接受编号 φ0,φ1,。对任意总可计算函数

f:NN,

存在索引 e 使

φe=φf(e)

作为部分函数外延相等。固定点是程序行为的固定点;定理既不要求 e=f(e),也不要求两份程序文本相同。

证明使用$s$-$m$-$n$ 定理。取总可计算的对角专门化函数 δ,满足

φδ(x)(y)φx(x,y).

f,δ 的总可计算性和通用解释,二元偏函数

ψ(x,y)φf(δ(x))(y)

是部分可计算的。令 a 是计算 ψ 的某个二元程序索引,并取

e=δ(a).

于是对所有 y

φe(y)φδ(a)(y)φa(a,y)ψ(a,y)φf(δ(a))(y)=φf(e)(y).

每个等号都来自已定义的专门化或通用模拟,因而证明没有假设程序能够神秘地读取自身源码。带参数版本进一步说,若代码变换还依赖参数 z,可以总可计算地选择固定点索引 e(z)

直觉

s-m-n 定理能把常量写进程序,递归定理把这种编译能力用于自应用:先制造一个接收“某个程序代码及普通输入”的模板,再把模板自己的代码作为固定参数嵌回去。结果程序不必知道自己的数值索引,却表现得仿佛把自身索引交给了变换器。

定理名称中的“递归”指可计算函数论传统,而不是普通编程语言中的递归调用。它保证的是语义自指,不要求运行栈、反射 API 或文件系统访问。

例子与边界

Quine 是直观例子:可以构造一个程序,在无输入时输出自身描述。更一般地,若 f(e) 生成一份“先输出关于索引 e 的说明,再执行某行为”的程序,递归定理给出某个 e,使 φe 与这份针对 e 的生成程序行为相同。

这里的等号只比较部分函数。两个程序可有不同运行时间、内存访问、输出前副作用或源码文本,却在指定抽象输出语义下计算同一函数。若讨论的观察语义包含日志或外部状态,就必须先把它们编码进函数输出,不能偷偷扩大等价概念。

f 必须是总可计算的代码变换。若 f 在某些索引上发散,证明无法保证构造过程得到 f(e) 的合法索引。定理也不保证数值固定点 e=f(e);例如 f(e)=e+1 没有自然数数值固定点,但递归定理仍保证相邻两个索引可计算同一偏函数。

递归定理不判定程序语义,也不与停机问题冲突。它构造一个满足行为方程的索引,却通常不能决定该行为是否停机或具有某个非平凡性质。

推论与应用

递归定理是自复制程序、自描述系统和许多不可判定性证明的统一工具。Rice 定理的某些加强形式可借带参数递归定理构造会根据分析器预测反向行动的程序;病毒或自更新代码模型也用它说明代码可将自身描述纳入计算。

可接受编号保证通用解释与有效编译,s-m-n 提供参数固化,递归定理才在其上完成语义固定点。三层缺一不可;把最终结论简化成“程序可以读自己的文件”会掩盖真正的构造机制。

参考资料
  • 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.