Rice 定理

Rice 定理把大量“这个程序算出的函数是否具有性质 $P$”的问题一次性归入不可判定：只要问题真正询问程序所计算的对象，答案既非对所有程序恒真也非恒假，就不存在对所有程序作出完备判定的算法。证明不是逐个分析性质，而是利用通用机器把某个已知不可判定行为嵌入程序语义：若源机器停机，就让新程序呈现具有 $P$ 的行为；否则呈现不具有 $P$ 的行为。决定性条件是性质只依赖程序算什么，而不依赖代码怎么写。

“$L(M)$ 是否为空、有限、正则、等于某个固定非平凡语言或包含字符串 101”都是非平凡语义性质，因此属于 Rice 定理范围并且不可判定。相反，“程序源码长度是否小于 $100$”“$M$ 是否有五个状态或恰有三个状态”是机器文本的语法性质，可直接检查；“$M$ 是否在 100 步内停机”也可做有限模拟。这些反例说明不能把所有程序问题都误称为 Rice 定理。定理本身只给不可判定性，不自动说明相应索引集是否可识别或属于哪个算术层级。

定理不意味着所有语义问题都不可处理：在有限状态机、总函数语言或受限类型系统中，相应性质可能可判定。它也不直接覆盖运行时间恰为多少步这类依赖具体实现的性质；应用前必须先确认性质对计算等价程序保持不变。

Rice 定理把大量逐题归约压缩成统一原则，用于证明程序等价、语言性质和部分函数性质不可判定。可接受编号公理库程序编号与可接受编号Program indexing · Acceptable numbering · Gödel numbering对部分可计算函数进行有效枚举，并要求编号支持通用解释与有效参数编译。说明索引如何指向程序行为，$s$-$m$-$n$ 定理公理库s-m-n 定理s-m-n theorem · Parameter theorem把程序的部分输入有效固化为新程序索引的参数化定理。提供有效代码参数化，Kleene 递归定理公理库Kleene 递归定理Kleene recursion theorem每个总可计算的程序代码变换都存在一个与其变换结果计算同一偏函数的程序索引。则可构造会引用自身索引的语义固定点；映射归约公理库映射归约Mapping reduction · Many-one reduction用可计算函数把一个语言成员关系变换为另一个语言成员关系。与停机问题公理库停机问题不可判定性Halting problem · Undecidability of halting不存在一个对任意程序和输入都能正确判断程序是否停机的算法。构成另一条标准证明骨架。实际静态分析必须限制语言，或在可靠性与完备性之间取舍。