決定可能性理論：計算可能性、決定不能性、半決定可能問題

形式的な概念と基本例

形式的には、有限の対象の集合、たとえば有限アルファベット上の文字列の集合を考える。ある集合が決定可能であるとは、任意の対象を与えられたとき、その集合に属する対象をちょうど受理し、属さない対象をちょうど拒否して、いずれの場合にも停止するチューリング機械、またはそれと同等のアルゴリズムが存在することをいう。古典的な決定可能な例には、正規言語や文脈自由言語への所属判定、および一定の制限された理論で表現される多くの算術的性質がある。これに対し、自然に現れる決定不能問題の例も存在する。最もよく知られる停止問題は、任意のプログラムが最終的に停止するかを問うが、すべての入力について正しく機能するアルゴリズムは存在しない。

半決定可能性（再帰的可算集合）

決定可能と決定不能の中間には、半決定可能（再帰的可算ともいう）な集合という概念がある。集合が半決定可能であるとは、その構成員を列挙するアルゴリズム、または集合に属する入力を与えられた場合には最終的に停止して受理するアルゴリズムが存在することである。集合に属さない入力に対しては、そのアルゴリズムは永久に実行を続けることがある。半決定可能集合は、肯定的な事例を検証できるという考え方を捉える。答えが「はい」であれば有限時間で確認できる一方、「いいえ」という答えは、その手続きでは証明できない場合がある。停止集合は半決定可能であるが、決定可能ではない。

歴史と基礎

決定可能性に関する問いは、数学を形式化しようとした20世紀初頭の試みとともに重要性を増した。ダフィット・ヒルベルトは、論理的妥当性を判定する一般的手続きの可能性に関する決定型の問題を提起した。1930年代にアロンゾ・チャーチとアラン・チューリングが行った研究は計算を形式化し、その限界を示した。チャーチはラムダ定義可能性を導入し、チューリングはチューリング機械モデルを導入した。そして両者は独立に、特定の決定問題が機械的には解けないことを証明した。これらの結果は、ヒルベルトの決定問題に厳密な否定的回答を与え、計算可能性理論の基礎を確立した。

用途、重要性、実践上の含意

決定可能性理論は、論理学と計算機科学の多くの領域を支えている。これは、アルゴリズムで解ける問題と、本質的に解けない問題とを区別し、自動定理証明、プログラム検証、データベース理論、形式言語の設計に対する見通しを導く。ある仕様のクラスについて検証可能性が決定可能であると分かれば、ツールを構築する根拠となる。逆に、決定不能性は、制限された形式体系や近似的方法を採用する動機となる。計算量理論は決定可能性を基礎とし、さらに資源の必要量に応じて可解な問題を分類する。

主要な区別と注目すべき事実

• 決定可能と半決定可能：決定可能な問題には、すべての入力で停止して正しい「はい」または「いいえ」を返すアルゴリズムがある。半決定可能な問題では、「はい」となる事例についてのみ停止が保証される。
• 多対一還元と次数：還元の概念は決定問題の相対的な難しさを比較し、解くことのできない問題の階層へとつながる。
• 実践上の要点：決定不能であることは、すべての個別事例が難しいことを意味しない。多くの特定の事例は解ける、あるいは容易である。これは、すべての事例を扱う単一のアルゴリズムが存在しないことを示すにすぎない。

入門的な解説および詳細な参考資料としては、一般的な計算可能性に関する文献や概説を参照されたい。入門的概説、講義ノートと例、歴史的概観、応用とツール。