(オプション) 決定不可能性 (Undecidability) と計算可能性理論との関連

決定不可能性とは、任意の入力に対して必ず停止し、正誤を返すアルゴリズムが存在しない問題の性質である。停止問題はその代表例で、プログラムと入力を与えたとき、実行がいつか停止するかをすべての場合に判定する一般手続きは存在しない。

仕組みと確認

対象問題を形式化し、別の決定不可能な問題からの帰着や対角化によって、万能判定器があると矛盾することを示す。決定不可能性と、決定可能だが計算量が大きいこと、単に実装が未完成なことを分ける。

ソフトウェア工学との接続

一般のコードを完全に判定できないからといって、静的解析やテストが無意味になるわけではない。入力・状態・言語機能を制限し、健全だが不完全な解析、抽象解釈、モデル検査、実行時監視を組み合わせる。

限界と注意点

決定不可能性は特定の一般問題に対する理論的限界であり、個別のプログラムが解析不能という意味ではない。検証対象、停止条件、偽陽性・偽陰性、近似の前提を明示する。