ライスの定理

Rice's theorem

Henry Gordon Rice

ある関数が計算不可能であることを示すとある条件

停止性問題の一般化

あるプログラムAが、ある性質Fを持つかどうかを判定するプログラムMは存在しない

自明でない場合を除く

つまりMが「常に1を返す」、「常に0を返す」を除く

これぐらい自明だと当たり前に実装できる

プログラムの仕様検証の完全自動化が理論上不可能であることを数学的に表している

定理 ref 『C言語による計算の理論』.icon p.64

1変数部分関数$ gが以下の3条件を満たすなら、$ gは計算不可能である

①どんな$ 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 『C言語による計算の理論』.icon 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に適用できる

しかし(★)と(☆)で矛盾