停止性問題は決定不能
7/18/2020, 8:50:30 AM - 269 days ago
復習。
日本語で書くと
帰納関数のコードと引数に対して計算が止まるかどうかを判定する帰納述語は存在しない
である.
まず, 万能帰納関数というのが存在する. 万能帰納関数 comp とは, 以下を満たすような関数である.
任意の自然数 m および帰納関数 f:Nm→N に対して,
ある自然数 pf が存在し,
λ(x0,...,xm−1).comp(pf,⟨x0,...,xm−1⟩)≐f ただし, ⟨x0,...,xm−1⟩ は (x0,...,xm−1) のゲーデル数で, この数列と一対一対応するような自然数である.
pf は帰納関数 f のコードと呼ばれる. comp はいわばインタプリタのようなもので, f に対応するようなコード pf を
このインタプリタに与えれば, f が実行されるということである.
次に, 帰納関数のコードと引数に対して計算が止まるかどうかを判定する帰納述語 halt∈N2 を考える.
すなわち
halt(p,x) is true≡comp(p,x) is defined と定義する.
あるプログラムがある入力に対して停止するかどうかというのは, そのプログラムに対応するコード p と入力 x を万能帰納関数 comp
が受け取った時 undefined になるかならないかという話だから, halt が真であるか否かという話になる. halt が帰納述語であれば
真か偽か一意に定まり, 決定可能であることになる.
実際にはこのような帰納述語は存在せず, 停止性問題は決定不能であることを示す.
はじめに
comp+(p,x)={comp(p,x)0if comp(p,x) is definedif comp(p,x) is undefined を考える. これは万能帰納関数が全関数(任意の入力に対し undefined にならない関数)になるよう修正を加えたものになる.
comp+ が帰納関数である(必ず停止し, 値が一意に定まる)と仮定しよう. ここで, diag:N→N
を
diag(x)=comp+(x,⟨x⟩)+1 ⋯(i) と定義する. comp+ が全関数かつ帰納関数であることから, diag も全関数かつ帰納関数である.
ここで, diag に対応するコードを p0 とおく. 万能帰納関数 comp の定義より,
comp(p0,⟨x⟩)≐diag(x) さらに diag が全関数であることから
comp+(p0,⟨x⟩)=diag(x) ⋯(ii) (i),(ii) より
comp+(p0,⟨p0⟩)=diag(p0)=comp+(p0,⟨p0⟩)+1 となり, 矛盾が導けた. したがって, 背理法により comp+ は帰納関数ではない.
この事実から, 帰納述語 halt が存在しないことも示せる. 仮に存在するとした場合,
comp+(p,x)={comp(p,x)0if halt(p,x) is trueif halt(p,x) is false で, 「帰納関数から帰納述語による場合分けで定義される関数も帰納関数である」という性質から comp+ が帰納関数であることが言えてしまうが,
これはまさに先ほど示した内容と矛盾する. よって示された.