停止性問題
halting problem
以下のような問題のことである
以下のようなチューリングマシン$ Hは存在しない
引数
任意のチューリングマシン$ M
任意の文字列$ \alpha
出力
$ Mを入力$ \alphaで動作開始すると
1: 有限ステップで停止する場合
0: 永久に停止しない場合
$ Hは、haltに相当するチューリングマシンmrsekut.icon $ M,\alphaを引数に取って、
$ M(\alpha)が有限時間で終了するかどうかを、
$ M(\alpha)を実行せずに、
判定するようなチューリングマシンは、存在しない
ということを言っている
停止性問題が決定不能であることの証明
以下の様なプログラム$ H,Mを考える
プログラム$ H
code:ts
const H = (A, x) => A(x)が停止する ? Yes : No
A(x)は、プログラムAにxを入力に与えて実行することを表す
A(x)を解釈して実行するような処理系が存在することを言っている
ちょっとメタmrsekut.icon
A(x)を実行できるようなインタプリタが存在するイメージ
プログラム$ M
code:ts
const 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 参考