決定不能性と停止問題

停止問題は、与えられたプログラムが与えられた入力に対して最終的に停止するかどうかを問うものであり、チューリングが、いかなるアルゴリズムもすべてのケースに対してこれに答えることはできないと証明したことは、決定不能な問題の創始的な例である。

Definition

決定問題は、いかなるアルゴリズムもすべての入力に対して正しく答えることができない場合に決定不能である。任意のプログラムが任意の入力に対して停止するかどうかを決定する停止問題は、自己言及的な対角線論法によって証明された、典型的な決定不能問題である。

Scope

このトピックでは、停止問題の決定不能性を確立する対角線論法、決定可能、認識可能、および共認識可能な問題の区別、プログラムのすべての非自明な意味的特性が決定不能であることを示すライス（Rice）の定理、ならびに論理学、数学、および計算機科学における自然な決定不能問題のカタログについて扱う。

Core questions

• なぜ、すべてのプログラムが停止するかどうかを決定できる単一のアルゴリズムは存在しないのか？
• 問題が決定可能であることと、単に認識可能であることの違いは何か？
• なぜ、プログラムの振る舞いの本質的にすべての興味深い特性は決定不能なのか？
• 決定不能性は、停止問題から他の問題にどのように波及するのか？

Key theories

停止問題の決定不能性

停止を決定するアルゴリズムが存在すると仮定すると、停止しないと予測された場合にのみ停止するプログラムによって矛盾が生じるため、そのようなアルゴリズムは存在しない。

ライス（Rice）の定理

プログラムによって計算される関数のすべての非自明な特性、つまり、振る舞いに基づいて一部のプログラムには当てはまり、他のプログラムには当てはまらないものはすべて決定不能であり、停止結果をすべての意味的特性に一般化する。

Clinical relevance

停止問題、およびライス（Rice）の定理によれば、プログラムのすべての非自明な振る舞い特性が決定不能であるため、無限ループを完全に検出したり、任意の正確性を検証したり、すべてのプログラムを完全に分析したりできるツールは存在しない。したがって、静的アナライザや検証ツールは、近似を行うか、誤検知を受け入れるか、またはその範囲を制限する必要がある。

History

チューリングは、カントール（Cantor）とゲーデル（Gödel）に触発された対角線論法を用いて、1936年に停止問題と論理学における決定問題の決定不能性を確立した。ライス（Rice）は1953年にその広範な一般化を証明し、その後数十年にわたり、ディオファントス方程式に関するヒルベルトの第10問題を含む多くの自然な問題が決定不能であることが示された。

Key figures

• Alan Turing
• Henry Gordon Rice
• Emil Post
• Alonzo Church

Seminal works

• turing1937
• sipser2013

Frequently asked questions

なぜプログラムを実行して停止するかどうかを確認できないのですか？

実行しても、実際に停止した場合にのみ停止したことがわかります。もし永久に実行されるのであれば、有限の待機時間ではそれが明らかになることはありません。停止問題は、すべてのプログラムと入力に対して有限時間内に常に正しい答えを出す方法を要求しますが、チューリングはそのような方法が存在しないことを証明しました。

決定不能性はプログラム分析を絶望的にするのでしょうか？

いいえ、しかし完璧な分析が不可能である理由を説明しています。ツールは、安全であることを証明できないものをすべて警告する保守的な方法、制限されたクラスのプログラムを正確に処理する方法、または敵対的または病的なケースでは失敗する可能性があることを認めつつ、多くの実用的なケースを解決する方法で対処しています。