停止性問題
halting problem
決定不可能である
1936年にAlan Turingが証明
以下のような問題のことである
以下のようなチューリングマシンHは存在しない
引数
任意のチューリングマシンM
任意の文字列\alpha
出力
Mを入力\alphaで動作開始すると
1: 有限ステップで停止する場合
0: 永久に停止しない場合
M,\alphaを引数に取って、
M(\alpha)が有限時間で終了するかどうかを、
M(\alpha)を実行せずに、
判定するようなチューリングマシンは、存在しない
ということを言っている
停止性問題が決定不能であることの証明
以下の様なプログラムH,Mを考える
プログラムH
tsconst H = (A, x) => A(x)が停止する ? Yes : No A(x) は、プログラム A に x を入力に与えて実行することを表す A(x) を解釈して実行するような処理系が存在することを言っているちょっとメタ
A(x) を実行できるようなインタプリタが存在するイメージプログラムM
tsconst M = (A) => {
if(H(A,A) === Yes) {
while(true){} // 無限ループ。停止しない
} else {
return 0 // 0を出力して停止
}
}このようなHが存在することを仮定して以下を証明する
つまり「Hのような計算が計算可能である」ことを仮定している
M(M) を考える M の引数に M を与えたもの「
M(M) は停止する」「 M(M) は無限ループになる」のどちらを仮定しても矛盾が生じる「
M(M) は無限ループになる」を仮定した場合→
H(M,M) === Yes である ∵Mの定義より→
M(M) が停止する ∵Hの定義より→仮定に矛盾
「
M(M) は停止する」を仮定した場合→
H(M,M) === No である ∵Mの定義より→
M(M) は停止しない ∵Hの定義より→仮定に矛盾
よって上の定義を満たすようなプログラムHは存在しない
つまりHは計算不可能
>したがって、どんなにコンピュータや科学が進歩しても、次のようなプログラム(ソフトウェア)は現れない。
>
> ・プログラムが正しいか間違っているかを自動的に判断するプログラム。
> ・間違っているプログラムを自動的に修正するプログラム。
> ・プログラムと仕様を入力し、そのプログラムが仕様を満しているかを判断するプログラム。 ref
参考