ライスの定理
Rice's theorem
停止性問題の一般化
あるプログラムAが、ある性質Fを持つかどうかを判定するプログラムMは存在しない
自明でない場合を除く
つまりMが「常に1を返す」、「常に0を返す」を除く
これぐらい自明だと当たり前に実装できる
プログラムの仕様検証の完全自動化が理論上不可能であることを数学的に表している
定理 ref 
p.64
①どんなk入力プログラムのコードnについてもg(n)\downarrowかつg(n)\in\{0,1\}
②ある2つのk入力プログラムのコードn_0,n_1が存在してg(n_0)=0かつg(n_1)=1
③mとnが同じk変数部分関数を計算するk入力プログラムのコードであるならば、必ずg(m)=g(n)
条件③は直接的に何を言っている #??
これ成り立たないことあるの？
もう少しさっくり書くと
gは「「k入力のプログラム」のコード」を引数に取って、0または1を返す
gの返り値が
0になるような「k入力のプログラム」も、
1になるような「k入力のプログラム」も
両方存在する
2つの異なる「k入力のプログラム」が同じ部分関数を計算するなら、0/1は必ず一致する
具体的に書くと
あるプログラムのゲーデル数を引数に取り、
「このプログラムが
Hello, World を出力するプログラム」かどうかを、そのプログラムを実行せずに判定する
ようなプログラムMは存在しない
具体化すると停止性問題になる
性質Fを「停止性」とすると、
あるプログラムAが、「停止性を持つかどうか」を判定するプログラムMは存在しない
になる
ライスの定理の証明 ref pp.64-65
3条件を満たす関数gが計算可能であると仮定する
1次変数関数fを以下で定義する
①x\in\mathrm{Program}_kかつg(x)=0のとき、f(x)=n_1
②x\in\mathrm{Program}_kかつg(x)=1のとき、f(x)=n_0
③x\notin\mathrm{Program}_k、f(x)=0
補足
kは任意に固定された自然数
k入力の全てのジャンププログラムのコードの集合を\mathrm{Program}_kとする
コードn_0,n_1は条件2のもの
gは①を満たしているので、fは全域関数になる
\forall n\in\mathrm{Program}_kについて、②より
g(n)=0ならば、g(f(n))=g(n_1)=1
g(n)=1ならば、g(f(n))=g(n_0)=0
したがって\forall n\in\mathrm{Program}_kについてg(n)\ne g(f(n))(★)
ここでわかっていること
gは計算可能
仮定より
「与えられた数は\mathrm{Program}_kの要素は部分関数か？」は計算可能
isCode == 1 かつ引数の長さがkであることをチェックよってfも計算可能
fに再帰定理を用いると、
rとf(r)がおなじになるようなr\in\mathrm{Program}_kが存在する(☆)
つまりrはk変数入力の関数のコード
fの定義より、この条件下でのf(r)はn_0かn_1のどちらか
n_0,n_1は②よりコード
つまりf(r)もk変数入力の関数のコード
よってr, f(r)を③のm,nに適用できる
しかし(★)と(☆)で矛盾
関連
ライスの定理の一般化
参考
証明など
数式での記述など
>ライスの定理は、プログラムにできることに限界があることを示していますが、それは何らかの能力が足りないから生まれているものではありません。
> 何とも皮肉なことに、能力があり過ぎる（自己参照さえできる）がゆえに、できないことが生まれているのです。
良い話だなー（しみじみ）