3,094
个编辑
更改
→Rice定理（1951）
==== [[Rice定理]]（1951） ====
==== [[Rice定理]]（1951） ====
'''陈述'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。
'''[[Rice定理|莱斯定理]]'''：程序行为的任何'''非平凡'''性质都不可判定。精确地说：设 <math>\mathcal{A}</math> 是某类部分可计算函数，既非空也非全体，则它的索引集 <math>A = \{ e : \phi_e \in \mathcal{A}\}</math> 不是可计算集（更不是递归集）。
* '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
* '''证明思路（停机归约——教科书标准路线，不依赖 SRT）'''：
# 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"<math>\notin \mathcal{A}</math>；
# 取一个"见证"函数 <math>\phi_a \in \mathcal{A}</math>。若处处无定义的函数恰好也在 <math>\mathcal{A}</math> 中，就对"补性质"（行为不在 <math>\mathcal{A}</math> 中）重做一遍论证——两类情况完全对称，故以下不妨设"恒发散"，即<math>\notin \mathcal{A}</math>；
# 对每个 <math>x</math>，用 s-m-n 定理（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；
# 对每个 <math>x</math>，用 s-m-n 定理（[[#s-m-n 定理（柯里化 / 参数特化）|§2.3]]）机械地造一个程序 <math>h(x)</math>：它先模拟"程序 <math>x</math> 在输入 <math>x</math> 上"的运行——这一步是对角线（让 <math>x</math> 面对自己的行为）；一旦该模拟停机，<math>h(x)</math> 就转而执行程序 <math>a</math>；若模拟永不停机，<math>h(x)</math> 也永不停机；
# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（[[#图灵停机问题（1936）|§5.7.3]]）。
# 于是 <math>x</math> 停在自己的输入上 ⟺ <math>h(x)</math> 计算的是 <math>\phi_a</math>（<math>\in \mathcal{A}</math>）⟺ <math>h(x) \in A</math>。若 <math>A</math> 可计算，就能机械判定"<math>x</math> 是否停在 <math>x</math> 上"，停机问题被解决——矛盾（[[#图灵停机问题（1936）|§5.7.3]]）。