停止性問題
任意のコードについて、それが停止するか永遠に動き続けるかを判定するアルゴリズムは存在するか。アラン・チューリングが1936年に示した答えは「不可能」で、決定不能性の古典的な証明である。
証明の手法は背理法だ。Halt(P,I)が存在すると仮定し、Halt(P', P')を実行してその逆を行うP'を構成すると矛盾が生じる。実務上の帰結として、静的解析は無限ループや未定義動作などを完全には検出できず、常にヒューリスティックと上限に頼ることになる。ライスの定理はこれを一般化し、プログラムのあらゆる非自明な意味的性質は決定不能だと述べる。