停止性問題
停止性問題（ていしせいもんだい）あるいはHalt(ホルト)は、（直接的には）計算可能性理論の問題で、チューリング機械（≒プログラム、アルゴリズム）Aに入力xを入れたら有限時間で停止するか、という問題。アラン・チューリングは1936年、停止性問題を解くチューリング機械が存在しない事を対角線論法で示した。すなわちそのようなチューリング機械の存在を仮定すると、自身が停止すると判定したならば無限ループを行い、停止しないと判定したならば停止するような別のチューリング機械が構成できるという矛盾が導かれる。
概要
プログラムAにデータxを入力して実行する事をA(x)と書き、A(x)がyを出力するときy=A(x)と書く。コンピュータではいかなるデータも0と1の数字で表し、したがってプログラム自身も0と1の数字で表せる。 コンピュータ用語ではこの数値化を「符号化」と呼び、理論計算機科学では「ゲーデル数化」という。以下記号を簡単にする為、プログラムAを数字で表したものも、Aと書く。 よって例えばプログラムA、Bに対し、「A(B)」は、「プログラムBを表す数字をBとし、AにBを入力して実行する」の意である。停止性問題とは、「プログラムAとデータxが与えられたとき、A(x)が有限時間で停止するかどうかを決定せよ」という問題である。
また「停止性問題の決定不能性定理」とは、停止性問題を常に正しく解くプログラムは存在しない、という定理である。 すなわち以下の性質を満たすプログラムHは存在しない、という定理である。
全てのプログラムAと全てのデータxに対し、
- A(x)が有限時間で停止する ⇒ H(A,x)は有限時間でYESを出力して停止する。
- A(x)は有限時間では停止しない ⇒ H(A,x)は有限時間でNOを出力して停止する。
Hの定義より、Hは入力(A,x)によらず必ず停止する事に注意されたい。A(x)が停止するかどうかを、必ず停止するHを使って決定する事はできない、というのが定理の趣旨である。
証明
背理法で示す。証明は、嘘つきのパラドックスに類似した論法を使う。
停止性問題を常に正しく解くプログラムHが存在したとする。
M(A)を、H(A,A)=YESなら停止せず、H(A,A)=NOなら0を出力して停止するプログラムとする。(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)の事をφA(x)と定義する。<math>g:\mathbb{N} \mapsto \{0,1\}</math>を、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が成立し、矛盾。したがって停止性問題を常に正しく解くプログラムは存在しない。
