Ex. 4.15
証明
(1) (halts? try try) が true ならば、(try try) は無限ループする。これは、(halts? try try)がtrueということと矛盾する。
(2) (halts? try try) が false ならば、(try try) は停止する。これは、(halts? try try)がfalseということと矛盾する。
なので、このような halts? を書くことは不可能である。
halts?が書けないということの意味は、プログラムが無限ループするか、しないかは各々のプログラムごとに地道に判定するしかないということ。
あと、もう一つ教訓がある。それは、halts? のように仕様がはっきりしていても、プログラム不可能な場合があるということ。
...しかし、"任意のpについて...正しく決める" なんていう仕様が、 はっきりした仕様といえるかどうかは疑問ではある。
あと実際の場では、メモリ制限や速度制限でプログラムできないのというは、なんとなく気付くが、論理的にプログラム不可能というのはちょっと気付かないかもしれない。