8.5
残念なこと
281
構文上の性質には、ライスの定理は当てはまりません。なぜなら、それは副次的な実装詳細
であって、プログラムの外部から見える振る舞いを変えずにリファクタリングで取り除けるた
めです。これに対して「このプログラムは入力を反転したものを出力するか」といった意味上
の性質は、ライスの定理の範疇であり、決定不能です。
ライスの定理は、プログラムが実行時に何をするのかに関する決定不能な問題が、非常にたくさん
あることを私たちに教えてくれます。
8.5
残念なこと
決定不能性というのは不都合なものです。停止性問題は残念なことに、私たちがすべてを手に入れ
ることはできないことを示しています。私たちは万能なプログラミング言語が持つ制約のない能力を求
めていますが、それと同時に、無限ループに陥らずに結果を生成するプログラムを書くこと、少なくと
も、長時間実行するタスクに含まれるサブルーチンが停止するプログラムを書くこと(「8.1.4 万能シ
ステムは永久にループできる」にあるコラム「長時間実行する計算」を参照)も求めています。ところ
が、その両方を同時に得ることはできないのです。
この失望については、2004年の有名な論文に物悲しくまとめられています。
停止性問題のために、言語設計は
2
つに分かれます。プログラミング規律に関して、私たちは次のど
ちらかを選択しなくてはなりません。
A.
安全性
-
すべてのプログラムが停止することがわかっている言語。
B.
万能性
-
次のようなプログラムが書ける言語。