s-m-n 定理

形式陈述 ​

固定偏可计算函数的可接受编号公理库程序编号与可接受编号Program indexing · Acceptable numbering · Gödel numbering对部分可计算函数进行有效枚举，并要求编号支持通用解释与有效参数编译。。对任意 $m,n\ge 1$，存在总可计算函数公理库可计算函数Computable function · Recursive function有图灵机对每个合法输入都停机并输出其值的全函数。

$$s_m^n:{\mathbb{N}}^{m+1}\to \mathbb{N}$$

使对所有程序索引 $e$、固定参数 $x_1,\dots ,x_m$ 和剩余输入 $y_1,\dots ,y_n$，

$${\phi }_{s_m^n(e,x_1,\dots ,x_m)}(y_1,\dots ,y_n)\simeq {\phi }_e(x_1,\dots ,x_m,y_1,\dots ,y_n).$$

符号 $\simeq$ 表示两边作为部分可计算函数公理库部分可计算函数Partial computable function允许机器在函数未定义的输入上不停机的部分函数。外延相等：同一输入上要么都不定义，要么都停机并给出相同值。函数 $s_m^n$ 本身对每组代码和固定参数都必须停机，即使被专门化的原程序以后会发散。

证明骨架是有效的程序模板构造。建立一个模板，它把常量 $e,x_1,\dots ,x_m$ 写入自身，并在收到 $y_1,\dots ,y_n$ 后调用通用解释器计算

$$U(e,x_1,\dots ,x_m,y_1,\dots ,y_n).$$

程序文本与常量都有有限有效编码，所以“把这些常量嵌入模板并输出新索引”是总可计算的语法变换。可接受编号保证生成代码可被统一解释，且与原程序在剩余输入上的行为一致。一般 $m,n$ 只是在编码元组和模板插槽数量上扩展同一构造。

直觉 ​

$s$-$m$-$n$ 定理是数学化的 partial evaluation。给一个多参数程序和前几项实参，可以只做编译工作，把这些实参写进一份新程序，而不必运行尚未给出的输入。新程序以后接收剩余参数时，表现得与旧程序收到完整参数完全一样。

定理处理的是程序代码，而不是先求出程序语义再重新编程。正因为代码变换总能完成，它才能成为自指、递归定理与索引集理论的可靠基础。

例子与边界 ​

设索引 $e$ 的二元程序计算

$${\phi }_e(a,b)=a+b.$$

固定 $a=5$ 后，$q=s_1^1(e,5)$ 是某个一元程序的索引，并满足 ${\phi }_q(b)=5+b$。更能体现部分性的例子是通用模拟器：固定机器索引 $e$ 后，可生成只等待输入 $x$ 的专用模拟程序；即使原机器在某些 $x$ 上永不停机，生成专用程序代码的过程仍会停机。

$s_m^n$ 不需要给出最短、最快或唯一的新程序。不同编译模板可产生不同索引，只要计算同一偏函数即可。公式也不声称

$$s_m^n(e,\overrightarrow{x})=e$$

或两份源码逐字符相同；结论只是运行行为外延相等。

定理不能用于判定任意程序语义。它能把参数写进代码，却不能告诉我们生成程序是否总停机、是否为空函数或是否与另一程序等价；这些非平凡语义问题仍受 Rice 定理限制。若编号只是任意集合论枚举，没有有效通用解释和编译性质，结论也可能失败。

推论与应用 ​

把程序代码作为普通数据，再用本定理固化自应用所需的参数，可以证明Kleene 递归定理公理库Kleene 递归定理Kleene recursion theorem · Kleene fixed-point theorem每个总可计算的程序代码变换都存在一个与其变换结果计算同一偏函数的程序索引。：任意总可计算代码变换都存在语义固定点。固定点满足程序行为相同，而非索引数值相等。

定理还支撑编译器专门化、解释器残留程序和通用模拟公理库通用图灵机Universal Turing machine输入机器编码和输入串后模拟该机器运行的图灵机。的形式分析。结合Rice 定理公理库Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。，它说明同一套有效编号既允许丰富的代码生成，又不提供语义判定捷径；“能构造程序”与“能决定程序做什么”必须严格区分。

参考资料

• Stephen C. Kleene, Introduction to Metamathematics, North-Holland, 1952, §§52–53, the parameter theorem.
• Hartley Rogers Jr., Theory of Recursive Functions and Effective Computability, MIT Press, 1987, Chs. 1–5 and 11.
• Nigel Cutland, Computability: An Introduction to Recursive Function Theory, Cambridge University Press, 1980, Ch. 3.