形式陈述
固定偏可计算函数的可接受编号理路程序编号与可接受编号Program indexing · Acceptable numbering · Gödel numbering对部分可计算函数进行有效枚举，并要求编号支持通用解释与有效参数编译。 。对任意总可计算函数理路可计算函数Computable function · Recursive function有图灵机对每个合法输入都停机并输出其值的全函数。
存在索引 使
作为部分函数外延相等。固定点是程序行为的固定点；定理既不要求 ，也不要求两份程序文本相同。
证明使用$s$-$m$-$n$ 定理理路s-m-n 定理s-m-n theorem · Parameter theorem把程序的部分输入有效固化为新程序索引的参数化定理。。取总可计算的对角专门化函数 ，满足
由 的总可计算性和通用解释理路通用图灵机Universal Turing machine输入机器编码和输入串后模拟该机器运行的图灵机。，二元偏函数
是部分可计算的。令 是计算 的某个二元程序索引，并取
于是对所有 ，
等式链逐步使用专门化与通用模拟，构造出所需的语义固定点。
带参数版本要求 为总可计算代码变换，并给出总可计算 满足 。在上述证明中把 换成 。参数化定理一致地产生二元程序索引 ，计算 ；取 ，同一等式链逐个 成立。因而这里是有效选择一整族固定点，不只是逐个参数断言存在。
直觉
-- 定理能把常量写进程序，递归定理把这种编译能力用于自应用：先制造一个接收“某个程序代码及普通输入”的模板，再把模板自己的代码作为固定参数嵌回去。结果程序不必知道自己的数值索引，却表现得仿佛把自身索引交给了变换器。
定理名称中的“递归”指可计算函数论传统，而不是普通编程语言中的递归调用。它保证的是语义自指，不要求运行栈、反射 API 或文件系统访问。
例子与边界
Quine 是直观例子：可以构造一个程序，在无输入时输出自身描述。更一般地，若 生成一份“先输出关于索引 的说明，再执行某行为”的程序，递归定理给出某个 ，使 与这份针对 的生成程序行为相同。
这里的等号只比较部分函数。两个程序可有不同运行时间、内存访问、输出前副作用或源码文本，却在指定抽象输出语义下计算同一函数。若讨论的观察语义包含日志或外部状态，就必须先把它们编码进函数输出。
必须是总可计算的代码变换。若 在某些索引上发散，证明无法保证构造过程得到 的合法索引。定理也不保证数值固定点 ；例如 没有自然数数值固定点，但递归定理仍保证相邻两个索引可计算同一偏函数。
递归定理不判定程序语义，也不与停机问题冲突。它构造一个满足行为方程的索引，却通常不能决定该行为是否停机或具有某个非平凡性质。
推论与应用
递归定理是自复制程序、自描述系统和许多不可判定性证明的统一工具。Rice 定理理路Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。的某些加强形式可借带参数递归定理构造会根据分析器预测反向行动的程序；病毒或自更新代码模型也用它说明代码可将自身描述纳入计算。
可接受编号理路程序编号与可接受编号Program indexing · Acceptable numbering · Gödel numbering对部分可计算函数进行有效枚举，并要求编号支持通用解释与有效参数编译。保证通用解释与有效编译，-- 提供参数固化，递归定理才在其上完成语义固定点。
算术中的对角引理理路对角引理Diagonal lemma · Arithmetical fixed-point lemma对任意一个自由变量的算术公式，构造与该公式作用于自身编码可证等价的句子。同样先造模板、再代入模板的描述，但它的终点是 ，即理论内的可证等价。本页的终点则是两个程序计算同一偏函数。两种构造都不要求代码数值相等，所比较的对象及等价关系却不同。
参考资料
- 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.
