停止問題

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

問題の形式的な記述の重要な部分は、コンピュータとプログラムの数学的定義であり、通常はチューリングマシンを用いて定義されます。この証明は、プログラムが停止するかどうかを判定する可能性のある任意のプログラムfに対して、 f が誤った判定を下す「病的な」プログラムgが存在することを示します。具体的には、 gとは、何らかの入力とともに呼び出されると、自身の情報源とその入力をfに渡し、 f がgが行うと予測する動作とは逆の動作をするプログラムです。gにおけるfの振る舞いは決定不能性を示し、これはあらゆるケースにおいて停止問題を解く プログラムf が存在しないことを意味します。

背景

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

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

while (true) continue

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

print "Hello, world!"

停止します。

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

プログラミングの結果

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

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

場合によっては、これらのプログラマは最小電力則を適用し、意図的に完全にチューリング完全ではないコンピュータ言語を使用します。多くの場合、 Rocqのように、すべてのサブルーチンが必ず完了することを保証する言語がこれにあたります。

よくある落とし穴

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

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

停止問題は、線形有界オートマトン（LBA）や有限メモリを持つ決定性機械においては理論的に決定可能である。有限メモリを持つ機械は有限個の構成を持つため、その上で実行される決定性プログラムは最終的に停止するか、以前の構成を繰り返すことになる。^{[ 4 ]}

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

しかし、それぞれが2つの状態を持つ100万個の小さな部品を持つコンピュータは、少なくとも^{2100万通りの}状態を持つことになる。^{[ 5 ]}

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

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

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

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

歴史

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

タイムライン

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

停止問題の起源

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

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

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

関連する問題は、シンボル S _i "に関する単純なチューリングマシン Z の印刷問題です。

デイヴィスの定式化の前身となる可能性のあるのは、クリーネの1952年の声明であり、文言のみが異なる：^{[ 19 ] [ 20 ]}

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

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

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

形式化

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

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

セットとしての表現

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

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

停止問題を表します。

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

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

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

実証概念

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

def g () -> None : if halts ( g ): loop_forever ()

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

厳密な証明のスケッチ

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

${\displaystyle h(i,x)={\begin{cases}1&{\text{if }}{\text{ program }}i{\text{ は入力 }}x,\\0&{\text{otherwise.}}\end{cases}}}$

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

f ( i , j )		私
		1	2	3	4	5	6
j	1	1	0	0	1	0	1
	2	0	0	0	1	0	0
	3	0	1	0	1	0	1
	4	1	0	0	1	0	0
	5	0	0	0	1	1	1
	6	1	1	0	0	1	0
	f ( i , i )	1	0	0	1	1	0
	g ( i )	あなた	0	0	あなた	あなた	0

計算可能な関数fの取り得る値を2次元配列に並べたもの。オレンジ色のセルは対角線を表す。f ( i , i ) とg ( i ) の値は下部に表示されている。Uは、関数gが特定の入力値に対して未定義であることを示す。

証明は、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 で停止する」は、プログラムによって実装される部分関数の特性ではありません。これは、部分関数を実装するプログラムの特性であり、非常に決定可能です。

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

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

近似値

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

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

これらの問題を回避するために、プログラムの「サイズ」に関するいくつかの制限された概念が開発されてきた。稠密ゲーデル番号付けは、各計算可能関数が 1 から n までの各インデックスのシーケンスで正の分数として現れるようにプログラムに番号を割り当てます。つまり、ゲーデル化 φ が稠密である場合と、すべての に対して、となる が存在する場合が同じです。たとえば、非自明なプログラムにインデックスを割り当て、その他のすべてのインデックスにエラー状態を割り当てる番号付けは稠密ではありませんが、構文的に正しいBrainfuckプログラムの稠密ゲーデル番号付けは存在します。^{[ 33 ]}稠密ゲーデル番号付けが最適と呼ばれるのは、他の任意のゲーデル番号付けに対して、1-1 の全再帰関数と、すべての、およびに対してとなる定数が存在する場合です。この条件は、すべてのプログラムのインデックスが、他の任意のゲーデル番号付けでのインデックスとそれほど大きくないこと^{[ 34 ]} 3つ目のサイズの概念は、バイナリ文字列で動作するユニバーサルマシンを使用し、入力プログラムを記述するために必要な文字列の長さを測定する。ユニバーサルマシンUとは、他のすべてのマシンVに対して、全計算可能関数hが存在し、 となるようなマシンである。最適マシンとは、コルモゴロフの計算量不変性の上限を達成するユニバーサルマシンである。つまり、すべてのマシンVに対して、すべての出力xに対して、長さnのVプログラムがxを出力する場合、最大で長さxを出力するUプログラムが存在するようなcが存在する。^{[ 35 ]}${\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}$

部分計算可能関数（アルゴリズム）について考察する。各 について、サイズ metric が最大 であるすべてのプログラムにおけるエラー率を考察する。その際、終了に失敗するか、「分からない」という答えを返すか、誤った答え（つまり停止して を出力するか、停止せずに を出力する）を生成する各プログラムをカウントする。稠密ゲーデル化と最適機械の場合、その動作は以下のように記述できる。^{[ 33 ] [ 35 ]}${\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より大きい。^{[ 35 ]}${\displaystyle \inf _{A\,{\textrm {正直}}}\liminf _{n\to \infty }\epsilon _{n}(A)}$

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

ゲーデルの不完全性定理

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

定理の弱い形式は、停止問題の決定不能性から次のように証明できる。^{[ 36 ]}自然数についてのすべての真の一階論理ステートメントの健全な (したがって一貫性のある) 完全な有効公理化があると仮定する。次に、これらすべてのステートメントを列挙するアルゴリズムを構築できる。これは、自然数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を反復すると、常に停止し、さらに、その答えは真になります(健全性により)。つまり、停止問題を判定するアルゴリズムが得られます。このようなアルゴリズムは存在し得ないことがわかっているため、自然数に関するすべての真の一階述語論理ステートメントの健全かつ完全な有効公理化が存在するという仮定は偽でなければなりません。

一般化

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

すべての入力で停止

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

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

部分的な解決策を認識する

停止問題に対して、ある入力に対しては正しい答えを返す一方で、他の入力に対しては全く答えを返さないプログラムは数多く存在します。しかし、「プログラムpが与えられたとき、それが部分停止ソルバーであるか」という問題（ここで述べた意味で）は、停止問題と同じくらい難しい問題です。これを理解するために、PHSR（「部分停止ソルバー認識器」）というアルゴリズムがあると仮定しましょう。PHSRは、停止問題を次のように解くことができます。入力プログラムx がyで停止するかどうかをテストするには、入力 ( x , y )に対して真を返し、他のすべての入力に対して発散するプログラムpを構築します。そして、PHSRを使って p をテストします。

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

非可逆計算

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

Oracleマシン

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

参照

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

注記

1. マコーネル、スティーブ (2004). Code Complete (第2版). ピアソン・エデュケーション. p. 374. ISBN 978-0-7356-3697-2。
2. Huang, Han-Way (2009). HCS12 / 9S12: ソフトウェアとハ​​ードウェアのインターフェイス入門. p. 197. ... プログラムが特定のループに陥った場合は、... 何が問題なのかを突き止めます。
3. Simon, David E. (1999). 『組み込みソフトウェア入門』p. 253.したがって、ハードリアルタイムシステムでは、常に同じ時間で実行されるサブルーチン、または明確に識別可能な最悪のケースを持つサブルーチンを記述することが重要です。
4. ミンスキー 1967、p. 24。イタリック体は原文のまま
5. ミンスキー 1967、25ページ。
6. Hodges 1983 、p. 83; Davis 1965、p. 108のDavisの解説
7. 絶対的に解決不可能な問題と相対的に決定不可能な命題 - 予測の説明、デイビス 1965 年、340 ～ 433 ページに再録
8. ミンスキー 1967 .
9. リード 1996、188～189頁。
10. ホッジス 1983、91ページ。
11. ホッジス 1983、91ページ;ペンローズ 1989、34ページ。
12. リード 1996、198ページ。
13. リード 1996、199ページ。
14. Davis 1965、p. 5ffに再録
15. 教会 1936年。
16. Entscheidungsproblemに関する覚書、デイビス1965年、110ページに再録
17. デイビス 1965、289ページ以降。
18. Davis 1965、p. 115に再録
19. ルーカス 2021 .
20. クリーネ 1952、382ページ。
21. ロッサー「ゲーデルの定理とチャーチの定理の証明の非公式解説」デイビス社 1965年223頁
22. デイビスからコープランドへの手紙、2001年12月12日、コープランド2004の脚注61、40ページ
23. コープランド 2004、40ページ。
24. チューリング全集のテキスト検索： Good (1992)、 Gandy & Yates (2001)、 Ince (1992)、 Saunders (1992)。同様に、 Hodges (1983)の索引には「停止」や「停止問題」という言葉は含まれていない。
25. Davis 1958、pp. vii–viii。
26. デイビス 1958年、70～71頁。
27. ムーア＆メルテンス 2011、236-237頁。
28. Strachey, C. (1965年1月1日). 「不可能プログラム」 .コンピュータジャーナル. 7 (4): 313. doi : 10.1093/comjnl/7.4.313 .
29. Daylight, Edgar G. (2021年4月16日). 「停止問題とセキュリティの言語理論的アプローチ：技術史家からの賞賛と批判」(PDF) . Computability . 10 (2): 141– 158. doi : 10.3233/COM-180217 . S2CID 233329507. 2021年8月26日閲覧. 
30. ペンローズ 1989、57–63頁。
31. コープランド 2004、15ページ。
32. Hamkins, Joel David; Miasnikov, Alexei (2006年10月1日). 「漸近確率1の集合上で停止問題は決定可能」(PDF) . Notre Dame Journal of Formal Logic . 47 (4). doi : 10.1305/ndjfl/1168352664 . S2CID 15005164. 2022年11月5日閲覧. 
33. ケーラー, スヴェン; シンデルハウアー, クリスチャン; ジーグラー, マーティン (2005). 「実世界停止性問題の近似について」 .計算理論の基礎. コンピュータサイエンス講義ノート. 第3623巻. pp.  454– 466. doi : 10.1007/11537311_40 . ISBN 978-3-540-28193-1。
34. リンチ、ナンシー（1974年10月）「停止問題への近似」（PDF） . Journal of Computer and System Sciences . 9 (2): 143– 150. doi : 10.1016/S0022-0000(74)80003-6 .
35. Bienvenu, Laurent; Desfontaines, Damien; Shen, Alexander (2016年4月5日). 「停止問題と最適マシンのための汎用アルゴリズムの再考」. Logical Methods in Computer Science . 12 (2): 1. arXiv : 1505.00731 . doi : 10.2168/LMCS-12(2:1)2016 . S2CID 14763862 . 
36. Aaronson, Scott (2011年7月21日). 「チューリングマシンによるロッサーの定理」 . Shtetl-Optimized . 2022年11月2日閲覧。
37. 例えば、 Sipser 2006、 Davis 1958、 Minsky 1967、 Hopcroft & Ullman 1979、 Börger 1989
38. Börger 1989、121ページ。
39. アブドゥラ＆ジョンソン 1996、p. 92.

参考文献

• チャーチ、アロンゾ (1936). 「初等数論の解けない問題」.アメリカ数学ジャーナル. 58 (2): 345– 363. doi : 10.2307/2371045 . JSTOR  2371045 .
• コープランド、B・ジャック編（2004年）『チューリングのエッセンス：コンピューティング、論理学、哲学、人工知能、人工生命における重要な著作、そしてエニグマの秘密』オックスフォード：クラレンドン・プレス、ISBN 0-19-825079-7。
• デイヴィス、マーティン(1965). 『決定不能なもの、決定不能な命題、解決不能な問題、そして計算可能な関数に関する基本論文』 ニューヨーク: レイヴン・プレス.チューリングの論文はこの巻の3番目です。ゲーデル、チャーチ、ロッサー、クリーネ、ポストによる論文も含まれています。
• デイヴィス、マーティン（1958）『計算可能性と解決不可能性』ニューヨーク：マグロウヒル。。
• ロジャース、ハートレー（ジュニア）（1957年）『再帰関数の理論と実効計算可能性』マサチューセッツ工科大学
• クリーネ、スティーブン・コール(1952).メタ数学入門.ノースホランド. OCLC  523942. OL  52444455M .第13章「計算可能関数」では、チューリング機械の停止問題の解けない性質について議論されています。チューリングの用語「循環のない非停止機械」とは異なり、クリーネは「停止する」、つまり停止する機械と呼んでいます。
• ルーカス、サルバドール (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 0-13-165563-9。第8章、セクション8.2「停止問題の解決不可能性」を参照してください。
• ムーア、クリストファー、メルテンス、ステファン (2011). 『計算の本質』 . オックスフォード大学出版局. doi : 10.1093/acprof:oso/9780199233212.001.0001 . ISBN 978-0-19-923321-2。
• リード、コンスタンス（1996年）ヒルベルト著、ニューヨーク：コペルニクス、ISBN 0-387-94674-8。1970年に初版が出版された本書は、1880年代から1930年代にかけてのドイツの数学と物理学の興味深い歴史書です。数学者、物理学者、エンジニアに馴染みのある数百人もの人物が登場します。明示的な参考文献がなく、脚注もほとんどないため、本書の印象は薄れていますが、リードは、ヒルベルトを個人的に知る人々への多数のインタビュー、そしてヒルベルトの書簡や論文を情報源としたと述べています。
• シプサー、マイケル(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. 2003年10月7日時点のオリジナルよりアーカイブ。チューリング, AM (1938). 「計算可能数について、そして計算問題への応用。訂正」 .ロンドン数学会報. s2-43 (1). Wiley: 544– 546. doi : 10.1112/plms/s2-43.6.544 . ISSN 0024-6115 . 2003年10月7日時点のオリジナルよりアーカイブ。 これは、チューリングがチューリング マシンを定義し、停止問題を定式化し、それが ( Entscheidungsproblemと同様に) 解決不可能であることを示す画期的な論文です。
• ペンローズ、ロジャー（1989年）『皇帝の新しい心：コンピュータ、心、そして物理法則について』（1990年訂正再版）オックスフォード：オックスフォード大学出版局。ISBN 0-19-286198-0。第2章「アルゴリズムとチューリングマシン」を参照。やや複雑すぎる説明（より良いモデルについてはデイビスの論文を参照）だが、チューリングマシンと停止問題、そしてチャーチのラムダ計算について綿密な説明がなされている。
• ホップクロフト, ジョン・E. ;ウルマン, ジェフリー・D. (1979). 『オートマトン理論、言語、計算入門』（第1版）. アディソン・ウェスレー. ISBN 81-7808-347-7。第7章「チューリングマシン」を参照してください。本書は「言語」の機械解釈、NP完全性などを中心に扱っています。
• ホッジス、アンドリュー（1983年）『アラン・チューリング：謎』ニューヨーク：サイモン＆シュスター、ISBN 0-671-49207-1。彼の証明に至る歴史と議論については、「真理の精神」の章を参照してください。
• エゴン・ベルガー (1989)。計算可能性、複雑さ、論理。アムステルダム: 北オランダ。ISBN 0-08-088704-X。
• 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日). Mathematical Logic . Elsevier. ISBN 978-0-08-053592-0。
  • インス, DC編 (1992). 『機械知能』 ノースホランド. ISBN 978-0-444-88058-1。
  • サンダース, PT編 (1992年11月26日).形態形成. エルゼビア. ISBN 978-0-08-093405-1。

さらに読む

• c2:停止問題
• アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセル、『プリンキピア・マテマティカ』、ケンブリッジ大学出版局、1962年。パラドックスの問題について、著者は、集合がその「決定関数」のいずれにおいてもオブジェクトにならない問題について論じており、特に「序論」第1章24ページの「形式論理で生じる困難」、第2章1章37ページ以降の「悪循環原理」、および第2章8章60ページの「矛盾」で取り上げている。
• マーティン・デイヴィス、「計算とは何か」『Mathematics Today』、リン・アーサー・スティーン著、ヴィンテージ・ブックス（ランダムハウス）、1980年。チューリングマシンについて書かれた素晴らしい小論文で、おそらく専門家ではない人にとってはこれまでで最も優れた論文と言えるでしょう。デイヴィスは、チューリングマシンをポストの計算モデルに基づいて、はるかに単純なモデルに簡略化しています。チャイティン証明についても論じています。エミール・ポストとジュリア・ロビンソンの短い伝記も収録されています。
• エドワード・ベルトラミ著『ランダムとは何か？ 数学と人生における偶然と秩序』、コペルニクス：シュプリンガー・フェアラーク、ニューヨーク、1999年。数学に興味のある非専門家にとって読みやすく、読みやすい。難しい内容は最後にまとめられている。チューリングマシンモデルも掲載されている。チャイティンの貢献についても論じている。
• アーネスト・ネーゲルとジェームズ・R・ニューマン共著『ゲーデルの証明』（ニューヨーク大学出版局、1958年）。非常に難解な主題を扱った素晴らしい著作。数学に興味のある非専門家向け。96 ～97ページと脚注でゲンツェンの証明について論じている。付録ではペアノの公理について簡潔に解説し、形式論理への入門として読者に優しく解説している。
• Daras, Nicholas J.; Rassias, Themistocles M. (2018).現代の離散数学と解析：暗号、情報システム、モデリングへの応用. スイス、シャム：Springer International Publishing. ISBN 978-3-319-74324-0。第 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プログラム」の注記を参照。
• 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 ページ)。
• デイヴィッド・ボルター著『チューリングの人間：コンピュータ時代の西洋文化』ノースカロライナ大学出版局、チャペルヒル、1984年。一般読者向け。年代が古い可能性があります。さらに別の（非常に単純な）チューリングマシンモデルが含まれています。
• Sven Köhler, Christian Schindelhauer, Martin Ziegler,実世界停止問題の近似について, pp.454-466 (2005) ISBN 3540281932Springer Lecture Notes in Computer Science 第3623巻：停止性問題の決定不能性とは、すべてのインスタンスが正しく答えられるわけではないが、「一部」、「多く」、あるいは「ほとんど」のインスタンスが正しく答えられる可能性があることを意味します。一方で、一定の答え「はい」は無限に正解となる可能性があり、また無限に不正解となる可能性もあります。この問いを合理的にするために、解けるインスタンスの密度を考えてみましょう。これは、対象となるプログラミングシステムに大きく依存することがわかります。
• 機械倫理の論理的限界と致死的自律兵器への影響- 「停止問題は道徳的なロボットが存在しないことを意味するのか?」で議論された論文

外部リンク

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