停止性問題

計算可能性理論において停止性問題（ていしせいもんだい、）または停止問題は、「どんなチューリングマシン、あるいは同様な計算機構についても、それが有限時間で停止するかを判定できるアルゴリズム」は可能か、という問題。
アラン・チューリングは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"に対し、
証明.
停止性問題を解くプログラム"H"が存在すると仮定して矛盾を導く。証明は嘘つきのパラドックスに類似している。
"M"("A")を、"H"("A","A")=YESならM(A)自身は停止せず、"H"("A","A")=NOなら0を出力してM(A)を停止するプログラムとする。("H"("A","A")と無限ループを組み合わせる事で"M"("A")を作る事ができる。)
"M"("M")は停止するだろうか？
よって停止性問題を解くプログラム"H"は存在しない。
カントールの対角線論法との関係.
対角線論法は、集合Sからその冪集合P(S)への全単射が存在しない(カントールの定理)事を示す為にゲオルク・カントールが使った論法である。
実は上述の証明は対角線論法も利用している。以下簡単の為、プログラムの入力は全て自然数とする。前述したようにプログラムは0と1からなる数字で書き表せるので、プログラム全体の集合は自然数全体の集合formula_1と自然に同一視できる。本当はformula_1の中にはプログラムに対応していないものもあるが、簡単の為その辺の事情は略する。
formula_3を次のように定義する：
以下φ("A","x")の事をφ"A"("x")と定義する。formula_4を、g("A")=￢φ"A"("A")により定義する。ただしここで「￢」は0と1を反転する写像。すなわち￢0=1、￢1=0。
すると対角線論法により、"g"=φ"M"となる"M"は存在しない。
さて、仮に停止性問題を常に正しく解くプログラム"H"が存在するとする。"M"("A")を、"H"("A","A")=YESなら停止せず、"H"("A","A")=NOなら0を出力して停止するプログラムとすると、"M"と"H"の定義より"g"=φ"M"が成立し、矛盾。したがって停止性問題を常に正しく解くプログラムは存在しない。
不完全性定理との関係.
停止性問題の決定不能性を利用してゲーデルの第一不完全性定理を示すことができる。
計算模型を適当に算術化すれば、「プログラム "M" は入力 "x" のもとで停止する」という述語 "Halt"("M","x") がΣ1述語となるようにできる。停止性問題の決定不能性はこの述語がΠ1述語でないことを述べている。したがって「プログラム "M" は入力 "x" のもとで停止しない」という述語はΠ1であるがΣ1でない。
述語論理を適当に算術化しておく。"T" をロビンソン算術を含む再帰的かつΣ1健全な理論とする。ここで "T" が再帰的とは、「"x" は "T" の公理のコードである」という述語が再帰的であることをいう。また "T" がΣ1健全とは、偽なΣ1文を証明しないことをいう。「"x" は "T" で証明可能な論理式のコードである」という述語 "Pr"("x") は再帰的可算であり、したがってΣ1述語である。
"T" が任意のΠ1文を証明または反証すると仮定して矛盾を導く。述語 "Halt"("M","x") を定義するΣ1論理式 "halt"("M","x") を取る。ここで ¬"halt"("M","x") は "T" 上でΠ1論理式であることに注意せよ。"T" はΣ1完全かつ無矛盾であるからΠ1健全である。仮定より "T" は任意のΠ1文を証明または反証するので、"T" はΠ1完全である。ゆえに、任意のプログラム "M" と入力 "x" について、以下は同値である：
ところで "Pr"(¬"halt"("M", "x")) はΣ1述語だから、¬"Halt"("M","x") もΣ1述語である。これは上に述べたことと矛盾する。
この証明は直観的には次のような意味である。もし "T" が任意の文を証明または反証するならば、"T"の定理を枚挙するプログラムを走らせて "halt"("M","x") または ¬"halt"("M","x") の形の定理が現れたらYESかNOを出力して停止する、という方法で停止性問題が肯定的に解けてしまう。（このプログラムの正当性は "T" のΣ1健全性とΠ1健全性、プログラムの停止性は任意の文を証明または反証するという仮定によって保証される。）これは停止性問題の決定不能性に反するので、 "T" では証明も反証もできない文が存在しなければならない。
以上の証明の停止性問題を再帰的でない任意の再帰的可算集合に置き換えることができる。例えば停止性問題の代りにラムダ計算の正規化可能性問題や述語論理の証明可能性問題を用いてもよい。