停止の問題

計算可能性理論において、停止問題とは、任意のコンピュータ プログラムと入力の記述から、プログラムの実行が終了するか、あるいは永久に実行し続けるかを決定する問題である。停止問題は決定不能であり、つまり、すべての可能なプログラムと入力のペアに対して停止問題を解決する一般的なアルゴリズムは存在しない。この問題は、一部の関数が数学的に定義可能であっても計算可能ではないことを示しているため、計算可能性の議論で頻繁に取り上げられる。

問題の正式な記述の重要な部分は、通常はチューリング マシンを介して、コンピュータとプログラムの数学的定義です。次に、証明は、プログラムが停止するかどうかを決定する可能性のある任意のプログラムfについて、 f が誤った決定を下す「異常な」プログラムg が存在することを示します。具体的には、 g は、何らかの入力で呼び出されると、独自のソースとその入力をfに渡し、 fがgが行うと予測することと反対のことを行うプログラムです。gに対するfの動作は、すべての可能性のあるケースで停止問題を解決する プログラムfが存在しないことを意味するため、決定不能性を示します。

停止問題とは、固定されたチューリング完全な計算モデル、つまりチューリングマシンと同等になるほど十分に一般的な、特定のプログラミング言語で記述できるすべてのプログラムにおけるコンピュータ プログラムの特性に関する決定問題です。問題は、プログラムとプログラムへの入力が与えられた場合、その入力で実行したときにプログラムが最終的に停止するかどうかを決定することです。この抽象的なフレームワークでは、プログラムの実行に必要なメモリの量や時間に関するリソース制限はありません。停止するまでに任意の時間がかかり、任意の量のストレージ スペースを使用できます。問題は、特定の入力で特定のプログラムが停止するかどうかだけです。

例えば、擬似コードでは、プログラム

while (true) continue

停止せず、むしろ無限ループで永遠に続きます。一方、プログラム

print "Hello, world!"

停止します。

これらのプログラムが停止するかどうかの判断は簡単ですが、より複雑なプログラムでは問題が伴います。この問題に対する 1 つのアプローチは、プログラムをいくつかのステップで実行し、停止するかどうかをチェックすることです。ただし、プログラムが実行されている限り、最終的に停止するか、永久に実行され続けるかはわかりません。チューリングは、任意のプログラムと入力に対して、その入力で実行したときにプログラムが停止するかどうかを常に正しく判断するアルゴリズムは存在しないことを証明しました。チューリングの証明の本質は、そのようなアルゴリズムはどれも矛盾した出力を生成する可能性があり、したがって正しくないということです。

無限ループの中には非常に便利なものもあります。たとえば、イベントループは通常、無限ループとしてコーディングされます。^[1]しかし、ほとんどのサブルーチンは終了するように設計されています。^[2]特に、ハードリアルタイムコンピューティングでは、プログラマーは終了することが保証されているだけでなく、指定された期限前に終了することが保証されているサブルーチンを記述しようとします。^[3]

これらのプログラマーは、汎用 (チューリング完全) プログラミング言語を使用する場合もありますが、MISRA CやSPARKなどの制限されたスタイルで記述しようとするため、結果として得られるサブルーチンが指定された期限前に終了することが簡単に証明されます。^{[引用が必要]}

また、これらのプログラマーは最小電力ルールを適用し、意図的に完全にチューリング完全ではないコンピュータ言語を使用します。多くの場合、これらはCoqなどのすべてのサブルーチンが終了することを保証する言語です。^{[引用が必要]}

停止問題の難しさは、決定手順がすべてのプログラムと入力に対して機能しなければならないという要件にあります。特定のプログラムは、与えられた入力で停止するか、停止しないかのいずれかです。常に「停止する」と答えるアルゴリズムと、常に「停止しない」と答えるアルゴリズムを考えてみましょう。特定のプログラムと入力に対して、これら 2 つのアルゴリズムのどちらかが正しく答えますが、どちらが正しいかは誰にもわかりません。しかし、どちらのアルゴリズムも停止問題を一般的には解決しません。

与えられたソース コードの実行をシミュレートするプログラム (インタープリタ)があります。このようなプログラムは、次の場合にプログラムが停止することを証明できます。インタープリタ自体が最終的にシミュレーションを停止し、元のプログラムが停止したことを示します。ただし、入力プログラムが停止しない場合はインタープリタも停止しないため、このアプローチでは前述の停止の問題を解決できません。停止しないプログラムに対して「停止しない」という回答を正しく出すことができません。

停止問題は、線形有界オートマトン（LBA）または有限メモリを持つ決定性マシンでは理論的に決定可能である。有限メモリを持つマシンは有限数の構成を持ち、したがってそのマシン上の決定性プログラムは最終的に停止するか、以前の構成を繰り返す必要がある。^[4]

...有限状態マシンは、完全に放置すると、最終的には完全に周期的な繰り返しパターンに陥ります。この繰り返しパターンの持続時間は、マシンの内部状態の数を超えることはできません...

しかし、それぞれが2つの状態を持つ100万個の小さな部品を持つコンピュータでは、少なくとも2 ^1,000,000個の状態が考えられます。^[5]

これは 1 の後に約 30 万個のゼロが続くものです...たとえそのような機械が宇宙線の周波数で動作するとしても、銀河の進化の永劫も、そのようなサイクルを旅する時間に比べれば取るに足らないものでしょう。

機械は有限であり、有限オートマトンには「いくつかの理論的な限界がある」^{[5] 。}

...関係する大きさから、状態図の単なる有限性に主に基づく定理や議論は、それほど大きな意味を持たないのではないかと疑うべきである。

また、各可能な決定の後に状態を列挙することによって、有限のメモリを持つ非決定性マシンが、非決定性決定の可能なシーケンスのどれか、またはすべてで停止するかを自動的に決定することもできます。

1936 年 4 月、アロンゾ・チャーチはラムダ計算の問題の決定不能性の証明を発表しました。チューリングの証明はその後、1937 年 1 月に発表されました。それ以来、1950 年代に出現した停止問題を含む、他の多くの決定不能問題が説明されてきました。

• 1900年：ダヴィト・ヒルベルトがパリで開催された第2回国際数学者会議で「23の質問」（現在ヒルベルトの問題として知られている）を提示した。「そのうちの2番目は、彼が示したように数学の厳密さが依存する『ペアノの公理』の一貫性を証明することであった。」 （1900） ^[6]
• 1920年 - 1921年：エミール・ポストはタグシステムの停止問題を研究し、それが解決不可能な問題の候補であると考えた。^{[7]その解決不可能性はずっと後になって}マービン・ミンスキーによって確立された。^[8] （1920年） （1921年）
• 1928年：ヒルベルトはボローニャ国際会議で「第二問題」を再構成した。^[9]彼は3つの疑問を提起した。すなわち、#1：数学は完全か？#2：数学は一貫しているか？#3：数学は決定可能か？^{[10] 3番目の疑問は}決定問題として知られている。^[11] （1928年）
• 1930年：クルト・ゲーデルが、 1928年のヒルベルトの最初の2つの疑問に対する答えとして証明を発表。^[12]「最初、彼[ヒルベルト]はただ怒ってイライラしていただけだったが、その後、問題に建設的に対処しようとし始めた...ゲーデル自身は、自分の研究がヒルベルトの形式主義的な観点と矛盾していないと感じており、その考えを論文で表現した」 （1930年） ^[13]
• 1931年：ゲーデルが『プリンキピア・マテマティカと関連体系の形式的に決定不可能な命題についてI』を出版 （1931年）^[14]
• 1935年4月19日：アロンゾ・チャーチが「初等整数論の解決不可能な問題」を出版し、実効計算可能な関数の直感的な概念は、一般的な再帰関数、または同等にラムダ定義可能な関数によって形式化できると提案した。彼は、ラムダ計算の停止問題（つまり、与えられたラムダ式が正規形を持つかどうか）は実効計算可能ではないことを証明した。 ( 1935-04-19 ) ^[15]
• 1936年：チャーチは再帰関数による計算の概念を用いて、Entscheidungsproblemが解けないことを初めて証明した。 （1936年） ^[16]
• 1936年10月7日：エミール・ポストの論文「有限組み合わせプロセス。定式化I」が受理される。ポストは彼の「プロセス」に「（C）停止」という命令を追加する。彼はそのようなプロセスを「タイプ1...それが決定するプロセスが各特定の問題に対して終了する場合」と呼んだ。 ( 1936-10-07 ) ^[17]
• 1936 年 5 月 - 1937 年 1 月:アラン チューリングの論文「計算可能数とその決定問題への応用」が1936 年 5 月に印刷され、1937 年 1 月に印刷されました。 ^[18]チューリングは 3 つの問題が決定不可能であることを証明しました。「満足」問題、「印刷」問題、および決定問題です。^[19]チューリングの証明は、機械による計算の概念を導入している点でチャーチの証明とは異なります。これは「解決不可能であることが証明された決定問題の最初の例」の 1 つです。^{[20] [ページが必要]} ( 1936-05 ) ( 1937-01 )
• 1939年：J・バークレー・ロッサーはゲーデル、チャーチ、チューリングによって定義された「効果的な方法」の本質的な同等性を観察する （1939年）^[21]
• 1943 年:スティーブン・クリーネは論文の中で、「完全なアルゴリズム理論を構築するには、手順を記述する必要があります。その手順は必ず終了し、その結果から「述語値は真か?」という質問に対して「はい」または「いいえ」という明確な答えを読み取ることができます」と述べています。 （1943年）
• 1952年：クリーネはチューリングマシンの停止問題の解決不可能性についての議論を含め、それを「最終的に停止する」マシン、つまり停止するマシンの観点から再定式化した。「...任意のマシンが任意の状況から起動された場合、最終的に停止するかどうかを決定するアルゴリズムは存在しない。」 （1952年） ^[22]
• 1952年：マーティン・デイビスは1952年にイリノイ大学の制御システム研究所で行われた一連の講義で「停止問題」という用語を使用した。これがこの用語の最初の使用例である可能性が高い。 （1952年） ^[23]

多くの論文や教科書では、停止問題の定義と決定不能性の証明をチューリングの1936年の論文に挙げている。しかし、これは正しくない。^{[19] [24]}チューリングは、1936年の論文を含め、出版したどの著作でも「停止」や「停止する」という用語を使用していない。^[25] 1936年から1958年までの学術文献を調べたところ、「停止問題」という用語を使用した最初の出版資料はロジャーズ（1957）であることが判明した。しかし、ロジャーズはデイビス（1958）の草稿を入手できたと述べており、^[19]マーティン・デイビスは序文で「専門家は、トピックの配置と扱いに目新しい点を見つけるかもしれない」と述べているため、^[26]この用語はデイビスによるものとしなければならない。^{[19] [24]}デイビスは手紙の中で、1952年から停止問題について言及していたと述べています。^[23]デイビスの本での用法は次のとおりです。^[27]

「[...] [チューリングマシン] Z が、与えられた初期状態に置かれた場合に、最終的に停止するかどうかを判定したい。この問題を Z の停止問題と呼ぶ。[...]

定理2.2停止問題が再帰的に解決不可能なチューリングマシンが存在する。

関連する問題として、シンボル S _i "に関する単純なチューリングマシン Z の印刷問題があります。

デイヴィスの定式化の先駆けとして考えられるのは、クリーネの1952年の声明であるが、これは文言のみが異なる: ^{[19] [22]}

特定の状況から起動された特定のマシンが最終的に停止するかどうかを決定するアルゴリズムは存在しません。

停止問題は、デイビスの印刷問題（「与えられた状態から起動したチューリングマシンは、与えられた記号を印刷することがあるか？」）と、チューリングの1936年の論文で検討された印刷問題（「空のテープから起動したチューリングマシンは、与えられた記号を印刷することがあるか？」）の両方とチューリング等価である。しかし、チューリング等価性はかなり緩く、2つの問題が同じであることを意味するわけではない。印刷するが停止しないマシンと、停止するが印刷しないマシンがある。印刷問題と停止問題は異なる問題を扱っており、重要な概念的および技術的な違いを示す。したがって、デイビスが次のように言ったのは単に控えめだった。^[19]

また、これらの問題の本質的な解決不可能性は、チューリングによって初めて発見されたとも言えるでしょう。

チューリングは、最初の証明で、チューリングマシンを導入することでアルゴリズムの概念を形式化しました。しかし、その結果はチューリングマシンに特有のものではなく、マルコフアルゴリズム、ラムダ計算、ポストシステム、レジスタマシン、タグシステムなど、チューリングマシンと計算能力が同等の他の計算モデルにも同様に当てはまります。

重要なのは、形式化によって、アルゴリズムを、そのアルゴリズムが操作できる何らかのデータ型に直接マッピングできることです。たとえば、形式化によってアルゴリズムが文字列上の関数 (チューリング マシンなど) を定義できる場合、これらのアルゴリズムを文字列にマッピングできるはずです。また、形式化によってアルゴリズムが自然数上の関数 (計算可能関数など) を定義できる場合、アルゴリズムを自然数にマッピングできるはずです。文字列へのマッピングは通常最も簡単ですが、n文字のアルファベット上の文字列も、 n進数表記システムの数値として解釈することで数値にマッピングできます。

決定問題の従来の表現は、問題の特性を持つオブジェクトの集合である。停止集合

K = {( i , x ) | プログラムiは入力xで実行されると停止します}

停止問題を表します。

この集合は再帰的に列挙可能であり、これはそれに含まれるすべてのペア ( i ,  x )をリストする計算可能な関数が存在することを意味する。しかし、この集合の補集合は再帰的に列挙可能ではない。^[28]

停止問題には同等の定式化が多数存在します。チューリング次数が停止問題のチューリング次数と等しい集合はいずれもそのような定式化です。そのような集合の例には次のものがあります。

• { i | プログラムiは、入力 0 で実行すると最終的に停止します}
• { i | 入力xがあり、入力xで実行するとプログラムi が最終的に停止します}。

クリストファー・ストラチーは、停止問題が解けないことを背理法で証明した。 ^{[29] [30]}証明は次のように進む。サブルーチンfが停止した場合（入力なしで実行した場合）にtrueを返し、それ以外の場合はfalseを返す、完全に 計算可能な関数 halts(f)が存在すると仮定する。ここで、次のサブルーチンを考えてみよう。

def  g ():
    停止した場合 ( g ): loop_forever ()
        

halts(g) は、 true または false を返す必要があります。これは、 halts が total であると想定されているためです。 halts(g) が true を返す場合、 g は loop_forever を呼び出して停止することはなく、これは矛盾です。 halts(g) が false を返す場合、gはloop_foreverを呼び出さないため停止します。これも矛盾です。 全体的に、g はhalts がgに指示する動作の逆の動作を行うため、halts(g) はgが停止するかどうかと一致する真理値を返すことができません。 したがって、 haltsが全計算可能関数であるという最初の想定はfalse である必要があります。

上記の概念は証明の一般的な方法を示していますが、計算可能な関数halts はサブルーチンを直接引数として取るのではなく、プログラムのソースコードを取ります。さらに、gの定義は自己参照的です。厳密な証明はこれらの問題に対処します。全体的な目標は、任意のプログラムi が任意の入力xで停止するかどうかを決定する完全に 計算可能な関数が存在しないことを示すことです。つまり、次の関数h ("halts") は計算可能ではありません。^[31]

${\displaystyle h(i,x)={\begin{cases}1&{\text{if }}{\text{ program }}i{\text{ 入力 }}x で停止し、\\0&{\text{それ以外の場合。}}\end{cases}}}$

ここで、プログラム i は、固定されたチューリング完全な計算モデルの すべてのプログラムの列挙におけるi番目のプログラムを指します。

証明は、2 つの引数を持つ全計算可能関数は要求される関数hにはなり得ないことを直接証明することによって進められます。概念のスケッチにあるように、全計算可能 2 項関数fが与えられれば、次の部分関数 gも何らかのプログラムeによって計算可能です。

${\displaystyle g(i)={\begin{cases}0&{\text{if }}f(i,i)=0,\\{\text{undefined}}&{\text{otherwise.}}\end{cases}}}$

gが計算可能であることの検証は、次の構成要素 (または同等のもの) に依存します。

• 計算可能なサブプログラム（ fを計算するプログラムはプログラムeのサブプログラムです）
• 値の重複（プログラムe はgの入力iからfの入力i、i を計算する）、
• 条件分岐（プログラムeはf ( i , i )の計算値に応じて2つの結果を選択する）、
• 定義された結果を生成しない（例えば、永久にループするなど）、
• 0 の値を返します。

eの次の疑似コードは、 g を計算する簡単な方法を示しています。

手順e ( i ) : if f ( i , i ) == 0 then 0を返し、そうでない場合は永久にループする 
         
         
    
         

g は部分的に計算可能なので、計算モデルがチューリング完全であるという仮定により、g を計算するプログラムeが存在するはずです。このプログラムは、停止関数hが定義されているすべてのプログラムの 1 つです。証明の次のステップでは、h ( e , e ) がf ( e , e ) と同じ値を持たないことが示されています。

gの定義から、次の 2 つのケースのうち 1 つが必ず成立することがわかります。

• f ( e , e ) = 0 なのでg ( e ) = 0 です。この場合、プログラムe は入力eで停止するため、h ( e , e ) = 1 です。
• f ( e , e ) ≠ 0 なので、g ( e ) は未定義です。この場合、プログラムe は入力eで停止しないので、h ( e , e ) = 0 になります。

どちらの場合でも、f はhと同じ関数にはなりません。f は2 つの引数を持つ任意の全計算可能関数であるため、このような関数はすべてhと異なる必要があります。

この証明は、カントールの対角線論法に類似しています。上の表に示すように、各自然数に対して 1 列 1 行の 2 次元配列を視覚化できます。f ( i , j ) の値は、列i行jに配置されます。f は完全に計算可能な関数であると想定されているため、配列のどの要素もf を使用して計算できます。関数gの構築は、この配列の主対角線を使用して視覚化できます。配列の位置 ( i , i ) に 0 がある場合、g ( i ) は 0 です。それ以外の場合、g ( i ) は未定義です。矛盾は、配列の列eがg自体に対応するという事実から生じます。ここで、 f が停止関数hであると仮定すると、g ( e ) が定義されている場合 (この場合は g ( e ) = 0)、g ( e )は停止するため、f ( e,e ) = 1 となります。しかし、g ( e ) = 0 となるのはf ( e,e ) = 0 の場合のみであり、 f ( e,e ) = 1と矛盾します。同様に、g ( e ) が定義されていない場合は、停止関数f ( e,e ) = 0 となり、gの構成ではg ( e ) = 0となります。これは、 g ( e ) が定義されていないという仮定と矛盾します。どちらの場合も矛盾が生じます。したがって、任意の計算可能関数f は停止関数hにはなり得ません。

問題が決定不可能であることを証明する典型的な方法は、停止問題を に簡略化することです。たとえば、自然数に関する特定のステートメントが真か偽かを決定する一般的なアルゴリズムは存在しません。その理由は、特定の入力が与えられた場合、特定のプログラムが停止するという命題は、自然数に関する同等のステートメントに変換できるためです。アルゴリズムが自然数に関するすべてのステートメントの真理値を見つけることができれば、このステートメントの真理値も確実に見つけることができますが、それによって元のプログラムが停止するかどうかが決まります。 ${\displaystyle P}$${\displaystyle P}$

ライスの定理は、停止問題は解決不可能であるという定理を一般化したものです。ライスの定理は、任意の非自明な特性について、すべてのプログラムに対して、入力プログラムによって実装された部分関数がその特性を持つかどうかを決定する一般的な決定手順は存在しないと述べています。(部分関数は、必ずしも結果を生成するとは限らない関数であるため、結果を生成するか停止に失敗するプログラムをモデル化するために使用されます。) たとえば、「入力 0 で停止する」という特性は決定不可能です。ここで、「非自明」とは、特性を満たす部分関数の集合が空集合でもすべての部分関数の集合でもないことを意味します。たとえば、「入力 0 で停止するか停止に失敗する」は明らかにすべての部分関数に当てはまるため、自明な特性であり、単に「真」を報告するアルゴリズムによって決定できます。また、この定理はプログラムによって実装された部分関数の特性にのみ当てはまります。ライスの定理はプログラム自体の特性には適用されません。たとえば、「100 ステップ以内に入力 0 で停止する」は、プログラムによって実装される部分関数の特性ではありません。これは、部分関数を実装するプログラムの特性であり、非常に決定可能です。

グレゴリー・チャイティンは、記号Ωで表される停止確率を定義しました。これは、ランダムに生成されたプログラムが停止する確率を表すと非公式に言われている実数の一種です。これらの数は、停止問題と同じチューリング次数を持ちます。これは、定義することはできますが、完全に計算することはできない、通常の超越数です。つまり、Ω の最初の数桁は単純なケースでは計算できますが、その桁を生成する アルゴリズムは存在しないことが証明できます。

停止問題に対する否定的な答えは、チューリングマシンでは解決できない問題があることを示しているため、チャーチ＝チューリングのテーゼは、効果的な方法を実装するマシンによって達成できることを制限します。ただし、人間の想像力で考えられるすべてのマシンがチャーチ＝チューリングのテーゼの対象となるわけではありません（例：オラクルマシン）。長期的にはチューリングマシンによるシミュレーションを逃れる実際の決定論的な物理プロセスが存在するかどうか、特にそのような仮説上のプロセスが計算機（ハイパーコンピュータ）の形で有効に活用され、チューリングマシンの停止問題などを解決できるかどうかは未解決の問題です。また、そのような未知の物理プロセスが人間の脳の働きに関係しているかどうか、そして人間が停止問題を解決できるかどうかも未解決の問題です。 ^[32]

チューリングの証明は、アルゴリズムが停止するかどうかを判定する機械的で一般的な方法（チューリングマシンや同等の計算モデルのプログラムなど）は存在しないことを示している。しかし、停止問題の個々のインスタンスには明確な答えがあり、それが実際に計算可能であるかどうかはわからない。特定のアルゴリズムと入力が与えられれば、それが停止するか停止しないかを示すことができる場合が多く、実際、コンピュータ科学者は正当性証明の一環としてまさにそれを行うことが多い。証明を構築するために自動的に使用できるヒューリスティックがいくつかあり、典型的なプログラムでは頻繁に成功する。この研究分野は自動停止解析として知られている。

停止問題ヒューリスティックの理論的パフォーマンス、特に再帰アルゴリズムによって正しく分類できる特定のサイズのプログラムの割合に関するいくつかの結果が確立されています。これらの結果は、割合が計算不可能であり、「サイズ」を決定するために使用されるプログラム エンコーディングの選択に大きく依存するため、正確な数値を示しません。たとえば、プログラムを状態の数で分類し、プログラムがテープの左側から外れるとエラー (停止せずに) になる特定の「チューリング半無限テープ」計算モデルを使用するとします。次に、状態の数によって均一に選択されたプログラムに対して、 となります。しかし、この結果は、ある意味で「自明」です。なぜなら、これらの決定可能なプログラムは単にテープから外れたものであり、ヒューリスティックは単にエラーのために停止しないことを予測するだけだからです。したがって、一見無関係な詳細、つまりエラーのあるプログラムの扱いが、プログラムの割合を決定する決定要因になる場合があります。^[33]${\displaystyle \lim _{n\to \infty }P(x\,{\text{停止は決定可能}}\mid x\,{\text{状態がある}}\,n\,{\text{状態}})=1}$${\displaystyle x}$

これらの問題を回避するために、プログラムの「サイズ」に関するいくつかの制限された概念が開発されてきた。稠密なゲーデル番号付けは、各計算可能関数が 1 から n までの各インデックスのシーケンスで正の分数で発生するようにプログラムに番号を割り当てます。つまり、ゲーデル化 φ が稠密であるためには、すべての に対して、となる が存在する必要があります。たとえば、非自明なプログラムにインデックスを割り当て、他のすべてのインデックスにエラー状態を割り当てる番号付けは稠密ではありませんが、構文的に正しいBrainfuckプログラムの稠密なゲーデル番号付けは存在します。^[34]稠密なゲーデル番号付けが最適と呼ばれるのは、他の任意のゲーデル番号付けに対して、1-1 の全再帰関数と、すべての、およびに対してとなる定数が存在する場合です。この条件により、すべてのプログラムのインデックスが、他の任意のゲーデル番号付けでのインデックスとそれほど大きくないことが保証されます。最適なゲーデル番号付けは、ユニバーサルチューリングマシンの入力に番号を付けることで構築されます。^[35] 3つ目のサイズの概念は、バイナリ文字列で動作するユニバーサルマシンを使用し、入力プログラムを記述するために必要な文字列の長さを測定する。ユニバーサルマシンUとは、他のすべてのマシンVに対して、 となる全計算可能関数hが存在するマシンである。最適なマシンとは、コルモゴロフの計算量不変性の境界を達成するユニバーサルマシンである。つまり、すべてのマシンVに対して、すべての出力xに対して、長さnのVプログラムがxを出力する場合、最大で長さがxを出力するUプログラムが存在するようなcが存在する。^[36]${\displaystyle i}$${\displaystyle c>0}$${\displaystyle \liminf _{n\to \infty }\#\{j\in \mathbb {N} :0\leq j<n,\phi _{i}=\phi _{j}\}/n \geq c}$${\displaystyle 2^{n}}$${\displaystyle \alpha}$${\displaystyle f}$${\displaystyle c}$${\displaystyle i}$${\displaystyle \alpha_{i}=\phi_{f(i)}}$${\displaystyle f(i)\leq ci}$${\displaystyle V(x)=U(h(x))}$${\displaystyle n+c}$

部分計算可能関数（アルゴリズム）について考える。それぞれについて、最大 のサイズメトリックのすべてのプログラム間のエラーの割合を考慮し、終了に失敗するか、「わからない」という答えを生成するか、間違った答えを生成する（つまり停止して を出力する）か、停止せずに を出力する各プログラムをカウントする。密なゲーデル化と最適マシンの場合、動作は次のように記述できる。^{[34] [36]}${\displaystyle A}$${\displaystyle n}$${\displaystyle \epsilon _{n}(A)}$${\displaystyle n}$${\displaystyle x}$${\displaystyle A}$${\displaystyle x}$${\displaystyle A(x)}$DOES_NOT_HALT${\displaystyle x}$${\displaystyle A(x)}$HALTS

• すべてのアルゴリズムについて、。つまり、問題のサイズが非常に大きくなっても、どのアルゴリズムでも最小エラー率は正になります。${\displaystyle A}$${\displaystyle \liminf _{n\to \infty }\epsilon _{n}(A)>0}$
• すべてのアルゴリズム に対して、となるような が存在します。つまり、問題のサイズが無制限に大きくなっても、どのアルゴリズムでもそのエラー率よりも悪い結果が頻繁に発生する正のエラー率が存在するということです。${\displaystyle \epsilon >0}$${\displaystyle A}$${\displaystyle \limsup _{n\to \infty }\epsilon _{n}(A)\geq \epsilon }$
• ${\displaystyle \inf _{A}\liminf _{n\to \infty }\epsilon _{n}(A)=0}$言葉で言えば、特定のサイズが増加するシーケンスに対してエラー率がゼロに任意に近づくようなアルゴリズムのシーケンスが存在します。ただし、この結果により、間違った答えを生成するアルゴリズムのシーケンスが可能になります。
• 定義されていないかもしれないが決して間違った答えを出さない「正直な」アルゴリズムだけを考えれば、メトリックに応じて0になる場合とならない場合がある。特に左合計ユニバーサルマシンの場合は0だが、実質的に最適なマシンの場合は0より大きい。^[36]${\displaystyle \inf _{A\,{\textrm {正直}}}\liminf _{n\to \infty }\epsilon _{n}(A)}$

これらの境界の複雑な性質は、 の振動的な動作によるものです。 任意に大きな「ブロック」で提供される、まれに発生する新しい種類のプログラムがあり、繰り返しの割合は常に増加しています。 新しい種類のブロックが完全に含まれていれば、エラー率は少なくとも ですが、ブロック間では、正しく分類された繰り返しの割合が任意に高くなる可能性があります。 特に、最初の N 個の入力を単に記憶し、それらの同等物を認識する「タリー」ヒューリスティックにより、任意の低いエラー率に無限に頻繁に到達できます。^[34]${\displaystyle \epsilon _{n}(A)}$${\displaystyle \epsilon }$

ゲーデルの不完全性定理によって提起された概念は、停止問題によって提起された概念と非常に似ており、証明もかなり似ています。実際、第一不完全性定理の弱い形式は、停止問題の決定不能性の簡単な帰結です。この弱い形式は、完全かつ健全な自然数の公理化は不可能であると主張する点で、不完全性定理の標準的な記述とは異なります。「健全」な部分が弱められた部分です。つまり、問題の公理体系は、自然数に関する真の記述のみを証明する必要があるということです。健全性は一貫性を意味するので、この弱い形式は強い形式の帰結と見なすことができます。ゲーデルの第一不完全性定理の標準形式の記述は、記述の真理値にはまったく関係がなく、数学的証明を通じてそれを見つけることができるかどうかという問題にのみ関係していることに留意することが重要です。

定理の弱い形式は、停止問題の決定不能性から次のように証明できます。^[37]自然数に関するすべての真の一階論理ステートメントの健全な（したがって一貫性のある）完全な公理化があると仮定します。次に、これらすべてのステートメントを列挙するアルゴリズムを構築できます。これは、自然数nが与えられたときに自然数に関する真の一階論理ステートメントを計算するアルゴリズムN ( n )が存在し、すべての真のステートメントに対して、 N ( n ) がそのステートメントを生成するnが少なくとも 1 つ存在することを意味します。ここで、表現 a を持つアルゴリズムが入力iで停止するかどうかを決定したいとします。このステートメントは、たとえばH ( a , i )などの一階論理ステートメントで表現できることがわかっています。公理化は完全であるため、N ( n ) = H ( a、i )となるnが存在するか、 N ( n ′ ) = ¬ H ( a、i ) となるn ′が存在することになります。したがって、H ( a、i ) またはその否定が見つかるまですべてのnを反復すると、常に停止し、さらに、得られる答えは真になります (健全性により)。つまり、これにより停止問題を決定するアルゴリズムが得られます。このようなアルゴリズムは存在できないことがわかっているため、自然数に関するすべての真の一階論理ステートメントの一貫した完全な公理化が存在するという仮定は偽でなければなりません。

停止問題の多くの変種は、計算可能性の教科書で見つけることができます。^[38]通常、これらの問題はRE完全であり、標準的な停止問題と同じように算術階層における複雑さの集合を記述します。したがって、変種は決定不可能であり、標準的な停止問題は各変種に還元され、逆もまた同様です。ただし、いくつかの変種は解決不可能性の度合いが高く、標準的な停止問題に還元できません。次の2つの例はよく見られる例です。 ${\displaystyle \Sigma _{1}^{0}}$

普遍停止問題（再帰理論ではトータリティとも呼ばれる）は、与えられたコンピュータプログラムがあらゆる入力に対して停止するかどうかを決定する問題である（トータリティという名前は、計算された関数が完全であるかどうかという同等の質問に由来している）。この問題は、停止問題のように決定不可能なだけでなく、非常に決定不可能である。算術階層の観点から見ると、これは -完全である。^[39]${\displaystyle \Pi _{2}^{0}}$

これは特に、停止問題に対する オラクルを使用しても決定できないことを意味します。

いくつかの入力に対しては停止問題に正しい答えを返すのに、他の入力に対してはまったく答えを返さないプログラムは数多くあります。しかし、「プログラムpが与えられた場合、それは部分停止ソルバーであるか」という問題 (説明した意味で) は、停止問題と同じくらい難しいものです。これを理解するには、それを実行するアルゴリズム PHSR (「部分停止ソルバー認識器」) があると仮定します。すると、次のようにして停止問題を解決するためにそれを使用できます。入力プログラムxがyで停止するかどうかをテストするには、入力 ( x、y )でtrueを報告し、他のすべての入力で発散するプログラムpを作成します。次に、PHSR を使用してp をテストします。

上記の議論は停止問題を PHS 認識に還元するものであり、同様に、すべての入力に対する停止などのより困難な問題も還元することができ、これは PHS 認識が決定不可能であるだけでなく、算術階層の上位、具体的には-完全であることを意味します。 ${\displaystyle \Pi _{2}^{0}}$

非可逆チューリングマシンは、テープの一部が非決定的に消失する可能性があるチューリングマシンである。非可逆チューリングマシンでは停止問題は決定可能であるが、非原始再帰的である。^[40]

停止問題に対する予言を持つマシンは、特定のチューリングマシンが特定の入力で停止するかどうかを判断できますが、一般に、自分自身と同等のマシンが停止するかどうかを判断することはできません。

• 忙しいビーバー
• ゲーデルの不完全性定理
• ブラウワー・ヒルベルト論争
• コルモゴロフ複雑性
• P対NP問題
• 終了分析
• 最悪の場合の実行時間

• チャーチ、アロンゾ(1936)。「初等数論の解決不可能な問題」。アメリカ数学ジャーナル。58 (2): 345–363。doi :10.2307/2371045。JSTOR  2371045。
• コープランド、B. ジャック編 (2004)。『チューリングの真髄: コンピューティング、論理、哲学、人工知能、人工生命に関する重要な著作、そしてエニグマの秘密』オックスフォード: クラレンドン プレス。ISBN 0-19-825079-7。
• デイビス、マーティン(1965)。『決定不能、決定不能命題、解決不能問題、計算可能関数に関する基本論文』ニューヨーク：レイヴン・プレス。チューリングの論文はこの巻の 3 番目です。論文にはゲーデル、チャーチ、ロッサー、クリーネ、ポストによる論文が含まれます。
• デイビス、マーティン（1958年）「計算可能性と解決不可能性」ニューヨーク：マグロウヒル。。
• ロジャース、ハートリー (Jr.) (1957)。再帰関数と実効計算可能性の理論。マサチューセッツ工科大学。
• クリーネ、スティーブン・コール（1952）。メタ数学入門。ノースホランド。ISBN 0923891579。第 13 章 (「計算可能な関数」) には、チューリング マシンの停止問題の解決不可能性に関する説明が含まれています。チューリングの用語である円のない非停止マシンとは異なり、クリーネは「停止する」、つまり停止するマシンについて言及しています。
• Lucas, Salvador (2021 年 6 月). 「停止問題の起源」. Journal of Logical and Algebraic Methods in Programming . 121 : 100687. doi :10.1016/j.jlamp.2021.100687. hdl : 10251/189460 . S2CID  235396831.
• ミンスキー、マービン(1967)。『計算：有限マシンと無限マシン』。ニュージャージー州エングルウッドクリフス：プレンティスホール。ISBN 0131655639。第 8 章、セクション 8.2「停止問題の解決不可能性」を参照してください。
• ムーア、クリストファー、メルテンス、ステファン (2011)。計算の性質。オックスフォード大学出版局。doi : 10.1093/acprof:oso/ 9780199233212.001.0001。ISBN 978-0-19-923321-2。
• リード、コンスタンス（1996年）。ヒルベルト。ニューヨーク：コペルニクス。ISBN 0387946748。1970 年に初版が出版された、1880 年代から 1930 年代までのドイツの数学と物理学の興味深い歴史書。数学者、物理学者、エンジニアによく知られている何百人もの名前がページ内に登場します。おそらく、明白な参照がなく、脚注もほとんどないため、内容が損なわれているかもしれませんが、リードは、ヒルベルトを個人的に知っていた人々への多数のインタビュー、およびヒルベルトの手紙と論文が情報源であると述べています。
• Sipser, Michael (2006)。「セクション 4.2: 停止問題」。計算理論入門(第 2 版)。PWS Publishing。pp. 173–182。ISBN 0-534-94728-X。
• チューリング、AM (1937)。「計算可能数について、そしてその計算問題への応用」。ロンドン数学会紀要。s2-42 (1)。Wiley: 230–265。doi :10.1112/plms/s2-42.1.230。ISSN 0024-6115。S2CID  73712  。^{[永久リンク切れ‍ ]}、チューリング、AM（1938）。「計算可能数について、そして計算問題への応用。訂正」。ロンドン数学会紀要。s2-43（1）。ワイリー：544–546。doi ： 10.1112 / plms / s2-43.6.544。ISSN 0024-6115  。^{[永久リンク切れ‍ ]}これは、チューリングがチューリングマシンを定義し、停止問題を定式化し、それが（ Entscheidungsproblemと同様に）解決不可能であることを示す画期的な論文です。
• ペンローズ、ロジャー(1989)。『皇帝の新しい心：コンピュータ、心、物理法則について』（1990 年訂正再版）。オックスフォード：オックスフォード大学出版局。ISBN 0192861980。第 2 章「アルゴリズムとチューリング マシン」を参照してください。非常に複雑な説明ですが (より優れたモデルについては Davis の論文を参照してください)、チューリング マシンと停止問題、および Church のラムダ計算について詳しく説明されています。
• ホップクロフト、ジョン E. ;ウルマン、ジェフリー D. (1979)。オートマトン理論、言語、計算入門(第 1 版)。Addison- Wesley。ISBN 81-7808-347-7。第 7 章「チューリング マシン」を参照してください。「言語」の機械解釈、NP 完全性などを中心にした本です。
• ホッジス、アンドリュー（1983年）。『アラン・チューリング：謎』ニューヨーク：サイモン＆シュスター。ISBN 0-671-49207-1。彼の証明に至る歴史と議論については、「真理の精神」の章を参照してください。
• エゴン・ベルガー (1989)。計算可能性、複雑さ、論理。アムステルダム: 北オランダ。ISBN 008088704X。
• Abdulla, Parosh Aziz; Jonsson, Bengt (1996). 「信頼できないチャネルを持つプログラムの検証」.情報と計算. 127 (2): 91–101. doi : 10.1006/inco.1996.0053 .
• AMチューリング全集
  • グッド、アーヴィング・ジョン編 (1992)。純粋数学。ノースホランド。ISBN 978-0-444-88059-8。
  • Gandy, RO; Yates, CEM 編 (2001 年 12 月 5 日)。数学論理学。エルゼビア。ISBN 978-0-08-053592-0。
  • インス、DC編（1992年）。機械知能。ノースホランド。ISBN 978-0-444-88058-1。
  • Saunders, PT編 (1992年11月26日)。形態形成。エルゼビア。ISBN 978-0-08-093405-1。

• c2:停止問題
• アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセル、『プリンキピア・マテマティカ』、ケンブリッジ大学出版局、1962年。パラドックスの問題に関して、著者らは、集合がその「決定関数」のいずれにおいてもオブジェクトにならない問題について論じており、特に「序論」第1章24ページの「形式論理で生じる困難」、第2章I.「悪循環原理」37ページ以降、および第2章VIII.「矛盾」60ページ以降で論じている。
• Martin Davis、「What is a computing」、Mathematics Today、Lynn Arthur Steen、Vintage Books (Random House)、1980 年。すばらしい小論文で、おそらくチューリング マシンについて非専門家向けに書かれたものの中では最高のものです。Davis はチューリング マシンを Post の計算モデルに基づくはるかに単純なモデルに簡略化します。Chaitin 証明について説明します。Emil PostとJulia Robinsonの短い伝記が含まれています。
• Edward Beltrami 著『What is Random? Chance and order in mathematical and order in mathematical and order』、Copernicus: Springer-Verlag、ニューヨーク、1999 年。数学に興味のある非専門家向けの読みやすい本で、難しい内容は最後にまとめられています。チューリング マシン モデルも掲載されています。Chaitinの貢献について論じています。
• アーネスト・ネーゲルとジェームズ・R・ニューマン著『ゲーデルの証明』ニューヨーク大学出版局、1958年。非常に難しい主題についての素晴らしい著作。数学に興味のある非専門家向け。96 ～97ページと脚注でゲンツェンの証明について論じている。付録ではペアノの公理について簡単に論じ、形式論理を読者にやさしく紹介している。
• Daras, Nicholas J.; Rassias, Themistocles M. (2018).現代の離散数学と解析：暗号、情報システム、モデリングへの応用。シャム、スイス。ISBN 978-3319743240。{{cite book}}: CS1 maint: location missing publisher (link)第 3 章のセクション 1 には、停止問題の質の高い説明、背理法による証明、および停止問題の便利なグラフィック表現が含まれています。
• Taylor Booth、「Sequential Machines and Automata Theory」、Wiley、ニューヨーク、1967年。第9章「チューリングマシン」を参照。難しい本で、電気技術者や技術専門家向け。再帰、チューリングマシンを参照した部分再帰、停止問題について説明。チューリングマシンモデルも掲載。第9章末の参考文献には、古い本のほとんど（1952年から1967年まで、Martin Davis、FC Hennie、H. Hermes、SC Kleene、M. Minsky、T. Radoなどの著者を含む）とさまざまな技術論文が記載されている。Busy-Beaver Programsの注記を参照。
• Busy Beaver Programs は Scientific American の 1984 年 8 月号と 1985 年 3 月号の 23 ページに記載されています。Booth の参考文献では、このプログラムが Rado, T.(1962)、On non-computable functions、Bell Systems Tech. J. 41 に由来するとされています。Booth はまた、第 9 章の 3、4、5、6 の問題で Rado の Busy Beaver Problem を定義しています (396 ページ)。
• David Bolter 著『Turing's Man: Western Culture in the Computer Age』、ノースカロライナ大学出版局、チャペルヒル、1984 年。一般読者向け。古い可能性があります。さらに別の (非常に単純な) チューリング マシン モデルが含まれています。
• Sven Köhler、Christian Schindelhauer、Martin Ziegler、「On approximating real-world halting issues」、pp.454-466 (2005) ISBN 3540281932 Springer Lecture Notes in Computer Science、volume 3623: 停止問題の決定不能性とは、すべてのインスタンスに正しく答えられるわけではないが、「一部」、「多く」、または「ほとんど」のインスタンスには正しく答えられる可能性があることを意味します。一方では、一定の答え「はい」は、無限に頻繁に正しく、無限に頻繁に間違っています。この質問を合理的にするには、解決できるインスタンスの密度を検討します。これは、検討中のプログラミング システムに大きく依存することがわかります。 
• 機械倫理の論理的限界と致死的な自律兵器への影響 - 「停止問題は道徳的なロボットが存在しないことを意味するのか?」で議論された論文

• ループスヌーパーをスクープする - 停止問題の決定不可能性の詩的な証明
• アニメーション映画 - 停止問題の決定不可能性の証明を説明するアニメーション
• 2 千年紀で 2 番目に重要な定理の 2 分証明 - わずか 13 行の証明
• haltingproblem.org - 停止問題を説明する人気のビデオとドキュメント。