s-m-n 定理 | Codeboy's Blog

形式陈述

固定偏可计算函数的可接受编号。对任意 $m,n\ge1$ ，存在总可计算函数

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

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

\varphi_{s_m^n(e,x_1,\ldots,x_m)} (y_1,\ldots,y_n) \simeq \varphi_e(x_1,\ldots,x_m,y_1,\ldots,y_n).

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

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

U(e,x_1,\ldots,x_m,y_1,\ldots,y_n).

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

在可接受编号的统一预言机版本中，同一模板也给出

\Phi_{s_m^n(e,\vec x)}^A(\vec y) \simeq\Phi_e^A(\vec x,\vec y) \qquad\text{对所有 }A.

解释器把查询转交同一个预言机，编译器只写入有限常量，不查询 $A$ 。所以 $s_m^n$ 是普通总可计算函数，并非需要先知道 $A$ 才能生成的代码变换。这个一致形式适用于相对停机集与 Turing 跳跃。

直觉

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

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

例子与边界

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

\varphi_e(a,b)=a+b.

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

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

s_m^n(e,\vec x)=e

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

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

推论与应用

把程序代码作为普通数据，再用本定理固化自应用所需的参数，可以证明Kleene 递归定理：任意总可计算代码变换都存在语义固定点。固定点满足程序行为相同，而非索引数值相等。

定理还支撑编译器专门化、解释器残留程序和通用模拟的形式分析。结合Rice 定理，它说明同一套有效编号既允许丰富的代码生成，又不提供语义判定捷径；“能构造程序”与“能决定程序做什么”必须严格区分。

记忆化流图专门化给出积极执行静态计算的具体算法：只有可达的标签—静态存储键有限时，逐键生成才保证结束。它可以把静态自环留下来，也可能因不断增长的静态计数而生成无穷多个版本。这与本定理的总可计算模板不矛盾：模板只把参数写入代码，并不要求在生成阶段完成所有可提前做的计算。

参考资料

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.
Andrew Marks, Computability Theory, 2024，Exercise 15.3，不依赖预言机的参数编译器。