停止性問題

計算可能性理論において停止性問題（ていしせいもんだい、英: halting problem）または停止問題は、「どんなチューリングマシン、あるいは同様な計算機構についても、それが有限時間で停止するかを判定できるアルゴリズム」は可能か、という問題。

アラン・チューリングは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からなる数字で書き表せるので、プログラム全体の集合は自然数全体の集合$\mathbb {N}$と自然に同一視できる。本当は$\mathbb {N}$の中にはプログラムに対応していないものもあるが、簡単の為その辺の事情は略する。

$\phi :\mathbb {N} \times \mathbb {N} \mapsto \{0,1\}$を次のように定義する：

A(x)が停止すればφ(A,x)=1、そうでなければφ(A,x)=0。

以下φ(A,x)の事をφ_A(x)と定義する。$g:\mathbb {N} \mapsto \{0,1\}$を、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) がΣ₁述語となるようにできる。停止性問題の決定不能性はこの述語がΠ₁述語でないことを述べている。したがって「プログラム M は入力 x のもとで停止しない」という述語はΠ₁であるがΣ₁でない。

述語論理を適当に算術化しておく。T をロビンソン算術を含む再帰的かつΣ₁健全な理論とする。ここで T が再帰的とは、「x は T の公理のコードである」という述語が再帰的であることをいう。また T がΣ₁健全とは、偽なΣ₁文を証明しないことをいう。「x は T で証明可能な論理式のコードである」という述語 Pr(x) は再帰的可算であり、したがってΣ₁述語である。

T が任意のΠ₁文を証明または反証すると仮定して矛盾を導く。述語 Halt(M,x) を定義するΣ₁論理式 halt(M,x) を取る。ここで ¬halt(M,x) は T 上でΠ₁論理式であることに注意せよ。T はΣ₁完全かつ無矛盾であるからΠ₁健全である。仮定より T は任意のΠ₁文を証明または反証するので、T はΠ₁完全である。ゆえに、任意のプログラム M と入力 x について、以下は同値である：

• ¬Halt(M,x) が成り立つ
• ¬halt(M,x) は T で証明可能である
• Pr(¬halt(M, x)) が成り立つ

ところで Pr(¬halt(M, x)) はΣ₁述語だから、¬Halt(M,x) もΣ₁述語である。これは上に述べたことと矛盾する。

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

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

関連項目

• ゲーデルの不完全性定理
• ライスの定理
• チャイティンの定数
• 無限ループ