程序编号与可接受编号

形式陈述 ​

固定一元部分可计算函数公理库部分可计算函数Partial computable function允许机器在函数未定义的输入上不停机的部分函数。的有效枚举

$${\phi }_0,{\phi }_1,{\phi }_2,\dots .$$

整数 $e$ 称程序或算法的索引，${\phi }_e$ 是该索引所计算的偏函数。编号首先必须是有效的：存在一个通用部分可计算函数

$$U(e,x)\simeq {\phi }_e(x),$$

其中 $\simeq$ 表示两边同时无定义或同时有定义且值相等。它还应支持有效参数化：给定多参数程序的索引及一部分固定输入，可以总可计算地生成剩余参数程序的索引。满足通用解释与这种编译性质、并能与其他合理编程系统有效互译的编号称可接受编号。

“可接受”不是要求编号唯一。不同可接受系统可以给同一程序不同整数，但存在总可计算翻译器保持所计算的偏函数；这使关于程序索引的基本定理不依赖某套偶然语法。

直觉 ​

通用图灵机公理库通用图灵机Universal Turing machine输入机器编码和输入串后模拟该机器运行的图灵机。说明程序能够作为数据交给一个固定解释器。可接受编号再要求这套代码系统不仅能解释，还能有效地把参数写进程序，像编译器把“程序模板 + 常量”变成新程序。自指和递归定理依赖的是这种可操作的代码结构，而不是把源码任意贴上整数标签。

索引描述语法，${\phi }_e$ 描述行为。许多不同程序会计算同一个偏函数；程序优化、无用指令和不同实现都可改变索引而保持语义。因而代码相等、程序行为相等和编号数值相等是三件不同的事。

例子与边界 ​

把每台图灵机的有限转移表编码为自然数，并令 ${\phi }_e(x)$ 模拟编号为 $e$ 的机器在输入 $x$ 上的输出，就得到程序枚举。合法编码由通用机解释；无效编码可统一约定为处处发散程序。若有一个双参数程序 $P(a,x)$，参数化性质允许从 $P$ 的索引与常量 $a_0$ 机械生成新索引 $q$，满足

$${\phi }_q(x)\simeq P(a_0,x).$$

边界在于任意双射或人为重排未必可接受。若编号把停机信息偷偷编码进索引位置，或者没有可计算的通用解释器，它即使集合论上枚举了所有偏函数，也不能支持程序变换定理。

映射 $e\mapsto {\phi }_e$ 不可能被当作可判定语义表。不同索引是否计算同一函数一般不可判定；也不能要求每个偏函数恰有一个索引，否则许多有效编程与固定点构造会失去所需的冗余。可接受性保证的是有效表达能力，不是程序等价判定器。

推论与应用 ​

有效参数化被$s$-$m$-$n$ 定理公理库s-m-n 定理s-m-n theorem · Parameter theorem把程序的部分输入有效固化为新程序索引的参数化定理。精确化：它把部分实参固化为新程序代码，同时保持代码变换本身总可计算。再结合对角式自应用，Kleene 递归定理公理库Kleene 递归定理Kleene recursion theorem · Kleene fixed-point theorem每个总可计算的程序代码变换都存在一个与其变换结果计算同一偏函数的程序索引。为每个总可计算代码变换构造语义固定点；Rice 定理公理库Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。则说明非平凡的部分可计算函数性质不可判定。

可接受编号还支撑可计算函数公理库可计算函数Computable function · Recursive function有图灵机对每个合法输入都停机并输出其值的全函数。的统一枚举、通用模拟、解释器和编译器的数学模型。结论针对程序行为而非源码文本：固定点通常满足 ${\phi }_e={\phi }_{f(e)}$，并不要求整数 $e=f(e)$，更不要求程序读取操作系统中的自身源文件。

参考资料

• Hartley Rogers Jr., Theory of Recursive Functions and Effective Computability, MIT Press, 1987, Chs. 1–5 and 11, acceptable programming systems and parameterization.
• Nigel Cutland, Computability: An Introduction to Recursive Function Theory, Cambridge University Press, 1980, Chs. 2–3, numberings and the parameter theorem.
• Stephen C. Kleene, Introduction to Metamathematics, North-Holland, 1952, §§44–53, enumeration and recursion theorems.