対角線論法による計算不可能性の証明

計算基礎論第3回課題

課題5

関数comp

Sプログラムのコードかどうか判定する

関数t-comp

Sプログラムのコードかつ無事終了することを判定する

関数dを考える

dはt-comp(x,x) = 0 のとき 1

dはt-comp(x,x) ≠ 0 のとき 0

t-compの計算不可能性の証明と同様の流れをcompに対しても行う

compの場合は理想的なdを計算するプログラムを作れない

comp(x,x)は停止しないから

dが未定義のとき1としても、対角線で未定義が来た時矛盾を導けない

t-compは実行が停止するかどうかの判定を有限時間で判定するが、compはそれをする必要がない

課題6

eq-execが計算可能と仮定する

eq-execを計算するプログラムが存在

eq-exec?とする

ex-exec?はhalt?を計算する

例えば無限ループ確定のプログラムを用意すると、halt?が計算できることになる

halt?の計算不可能性と矛盾