赖斯定理

不失一般性,假设处处未定义的函数 $\emptyset$(由一个对任何输入都永不停机的程序所计算)不具有性质 $P$——否则改用补性质 $\lnot P$ 论证,它可判定当且仅当 $P$ 可判定。由于 $P$ 非平凡,固定某个程序 $e_0$,其函数 $\varphi_{e_0}$ 具有性质 $P$。

反证:假设 $P$ 可由某算法 $D$ 判定(给定一个程序索引,$D$ 停机并正确报告该程序的函数是否具有性质 $P$)。我们把停机问题归约到 $P$,从而与定理1矛盾。

对任意一对 $(e,x)$,有效地构造(通过简单的文本操作——克莱尼的 s-m-n 定理)一个新程序 $e'$,它对任意输入 $y$:先模拟程序 $e$ 在输入 $x$ 上运行;一旦该模拟停机,$e'$ 就接着模拟程序 $e_0$ 在输入 $y$ 上运行并输出其结果。

考察两种情形。若 $e$ 在 $x$ 上停机:对 $e$ 在 $x$ 上的模拟会结束,于是 $e'$ 在所有输入上的行为都与 $e_0$ 完全一致,即 $\varphi_{e'}=\varphi_{e_0}$——它具有性质 $P$(因为 $P$ 是语义的,只依赖于所计算的函数,而 $\varphi_{e_0}$ 具有 $P$)。若 $e$ 在 $x$ 上不停机:对 $e$ 在 $x$ 上的模拟永不结束,于是 $e'$ 在任何输入 $y$ 上都永远到不了模拟 $e_0$ 的那一步;因此 $\varphi_{e'}$ 就是处处未定义的函数 $\emptyset$,按假设它不具有性质 $P$。

所以:$e$ 在 $x$ 上停机 $\iff$ $\varphi_{e'}$ 具有性质 $P$ $\iff$ $D(e')$ 回答"是"。由于 $(e,x)\mapsto e'$ 可计算,算法"由 $(e,x)$ 计算出 $e'$,再运行 $D(e')$"就能判定停机问题——与定理1矛盾。故不存在这样的 $D$:$P$ 不可判定。$\blacksquare$