停止性問題のソースを表示

{{出典の明記|date=2018年1月}}
[[計算可能性理論]]において'''停止性問題'''（ていしせいもんだい、{{lang-en-short|halting problem}}）または'''停止問題'''は、「どんな[[チューリングマシン]]<ref group="注">ここを「アルゴリズム」としてしまうと、[[循環論法]]になってしまって問題としておかしくなる。</ref>、あるいは[[チャーチ＝チューリングのテーゼ|同様な計算機構]]についても、それが有限時間で停止するかを判定できる[[アルゴリズム]]」は可能か、という問題。

[[アラン・チューリング]]は1936年、停止性問題を解くアルゴリズムは存在しないことをある種の[[カントールの対角線論法|対角線論法]]のようにして証明した。
すなわち、そのようなアルゴリズムを実行できるチューリングマシンの存在を仮定すると「自身が停止するならば無限ループに陥って停止せず、停止しないならば停止する」ような別の構成が可能ということになり、[[矛盾]]となる。

== 概要 ==
プログラム''A''にデータ''x''を入力して実行する、ということを''A''(''x'')と書き、''A''(''x'')が''y''を出力するとき''y''=''A''(''x'')と書くことにする。

現代のコンピュータの使い方であれば、中身がプログラムであるバイナリの[[実行ファイル]]を、単なるデータファイルとして扱うこともできる、ということから、プログラムを、他のプログラムへの入力データにできる、ということは感覚的にわかる。また具体的には、エミュレータに実行ファイルを渡す、というのが一例である。チューリングは、「いかなる[[チューリングマシン]]をも模倣できるチューリングマシン」である「万能チューリングマシン」が可能であることを示し、模倣されるチューリングマシンはそのテープの初期状態に記述される、というようにして議論を進めた。

以下記号を簡単にする為、「データとしてのプログラムA」も、Aと書く。 よって例えばプログラムA、Bがあったとして、「A(B)」は、「プログラムAに、データとしてのプログラムBを入力として渡す」の意である。停止性問題とは、「プログラムAとデータxが与えられたとき、A(x)が停止するかどうかを決定せよ」という問題である。

また「停止性問題の決定不能性」とは、停止性問題を常に正しく解くプログラムは存在しない、ということである。 すなわち以下の性質を満たすプログラム''H''は存在しない。

全てのプログラム''A''と全てのデータ''x''に対し、
* ''A''(''x'')の実行は停止する ⇒ ''H''(''A'',''x'')はYESを出力する。
* ''A''(''x'')の実行は停止しない ⇒ ''H''(''A'',''x'')はNOを出力する。

== 証明 ==
停止性問題を解くプログラム''H''が存在すると仮定して矛盾を導く。証明は[[自己言及のパラドックス#嘘つきのパラドックスの論理構造|嘘つきのパラドックス]]に類似している。

''M''(''A'')を、''H''(''A'',''A'')=YESならM(A)自身は停止せず、''H''(''A'',''A'')=NOなら0を出力してM(A)を停止するプログラムとする。(''H''(''A'',''A'')と[[無限ループ]]を組み合わせる事で''M''(''A'')を作る事ができる。)

''M''(''M'')は停止するだろうか？

* ''M''(''M'')が停止したとすると、''M''の定義より''H''(''M'',''M'')=NO。''H''の定義より ''H''(''M'',''M'')=NOとなるのは''M''(''M'')が停止しないときのみなので、矛盾。
* ''M''(''M'')が停止しないとすると、''M''の定義より''H''(''M'',''M'')=YES。''H''の定義より、''H''(''M'',''M'')=YESとなるのは''M''(''M'')が停止するときのみなので、矛盾。

よって停止性問題を解くプログラム''H''は存在しない。

== カントールの対角線論法との関係 ==
[[対角線論法]]は、集合Sからその冪集合P(S)への全単射が存在しない(カントールの定理)事を示す為に[[ゲオルク・カントール]]が使った論法である。

実は上述の証明は対角線論法も利用している。以下簡単の為、プログラムの入力は全て自然数とする。前述したようにプログラムは0と1からなる数字で書き表せるので、プログラム全体の集合は自然数全体の集合<math>\mathbb{N}</math>と自然に同一視できる。本当は<math>\mathbb{N}</math>の中にはプログラムに対応していないものもあるが、簡単の為その辺の事情は略する。

<math>\phi:\mathbb{N} \times \mathbb{N} \mapsto \{0,1\}</math>を次のように定義する：
:''A''(''x'')が停止すればφ(''A'',''x'')=1、そうでなければφ(''A'',''x'')=0。

以下φ(''A'',''x'')の事をφ<sub>''A''</sub>(''x'')と定義する。<math>g:\mathbb{N} \mapsto \{0,1\}</math>を、g(''A'')=￢φ<sub>''A''</sub>(''A'')により定義する。ただしここで「￢」は0と1を反転する写像。すなわち￢0=1、￢1=0。

すると対角線論法により、''g''=φ<sub>''M''</sub>となる''M''は存在しない。

さて、仮に停止性問題を常に正しく解くプログラム''H''が存在するとする。''M''(''A'')を、''H''(''A'',''A'')=YESなら停止せず、''H''(''A'',''A'')=NOなら0を出力して停止するプログラムとすると、''M''と''H''の定義より''g''=φ<sub>''M''</sub>が成立し、矛盾。したがって停止性問題を常に正しく解くプログラムは存在しない。

== 不完全性定理との関係 ==
停止性問題の決定不能性を利用して[[ゲーデルの不完全性定理|ゲーデルの第一不完全性定理]]を示すことができる。

計算模型を適当に[[ゲーデル数|算術化]]すれば、「プログラム ''M'' は入力 ''x'' のもとで停止する」という述語 ''Halt''(''M'',''x'') が[[算術的階層|&Sigma;<sub>1</sub>述語]]となるようにできる。停止性問題の決定不能性はこの述語が&Pi;<sub>1</sub>述語でないことを述べている。したがって「プログラム ''M'' は入力 ''x'' のもとで'''停止しない'''」という述語は&Pi;<sub>1</sub>であるが&Sigma;<sub>1</sub>でない。

述語論理を適当に算術化しておく。''T'' を[[ロビンソン算術]]を含む再帰的かつ&Sigma;<sub>1</sub>健全な理論とする。ここで ''T'' が[[帰納的集合|再帰的]]とは、「''x'' は ''T'' の公理のコードである」という述語が再帰的であることをいう。また ''T'' が&Sigma;<sub>1</sub>健全とは、偽な&Sigma;<sub>1</sub>文を証明しないことをいう。「''x'' は ''T'' で証明可能な論理式のコードである」という述語 ''Pr''(''x'') は[[帰納的可算集合|再帰的可算]]であり、したがって&Sigma;<sub>1</sub>述語である。

''T'' が任意の&Pi;<sub>1</sub>文を証明または反証すると仮定して矛盾を導く。述語 ''Halt''(''M'',''x'') を定義する&Sigma;<sub>1</sub>論理式 ''halt''(''M'',''x'') を取る。ここで ¬''halt''(''M'',''x'') は ''T'' 上で&Pi;<sub>1</sub>論理式であることに注意せよ。''T'' は&Sigma;<sub>1</sub>完全かつ無矛盾であるから&Pi;<sub>1</sub>健全である。仮定より ''T'' は任意の&Pi;<sub>1</sub>文を証明または反証するので、''T'' は&Pi;<sub>1</sub>完全である。ゆえに、任意のプログラム ''M'' と入力 ''x'' について、以下は同値である：
* ¬''Halt''(''M'',''x'') が成り立つ
* ¬''halt''(''M'',''x'') は ''T'' で証明可能である
* ''Pr''(¬''halt''(''M'', ''x'')) が成り立つ
ところで ''Pr''(¬''halt''(''M'', ''x'')) は&Sigma;<sub>1</sub>述語だから、¬''Halt''(''M'',''x'') も&Sigma;<sub>1</sub>述語である。これは上に述べたことと矛盾する。

この証明は直観的には次のような意味である。もし ''T'' が任意の文を証明または反証するならば、''T''の定理を枚挙するプログラムを走らせて ''halt''(''M'',''x'') または ¬''halt''(''M'',''x'') の形の定理が現れたらYESかNOを出力して停止する、という方法で停止性問題が肯定的に解けてしまう。（このプログラムの正当性は ''T'' の&Sigma;<sub>1</sub>健全性と&Pi;<sub>1</sub>健全性、プログラムの停止性は任意の文を証明または反証するという仮定によって保証される。）これは停止性問題の決定不能性に反するので、 ''T'' では証明も反証もできない文が存在しなければならない。

以上の証明の停止性問題を再帰的でない任意の再帰的可算集合に置き換えることができる。例えば停止性問題の代りに[[ラムダ計算]]の正規化可能性問題や述語論理の証明可能性問題を用いてもよい。

== 脚注 ==
{{脚注ヘルプ}}
=== 注釈 ===
{{Notelist2}}

== 関連項目 ==
* [[ゲーデルの不完全性定理]]
* [[ライスの定理]]
* [[チャイティンの定数]]
* [[無限ループ]]

{{Normdaten}}

{{DEFAULTSORT:ていしせいもんたい}}
[[Category:決定不能問題]]
[[Category:計算可能性理論]]
[[Category:計算理論]]
[[Category:思考実験]]
[[Category:数学の問題]]
[[Category:アラン・チューリング]]
[[Category:数学に関する記事]]