停止性問題の解決不可能性

任意のプログラムの停止性を判定できる関数 eval-halt?を作れると仮定し、矛盾することを示してみる。下のような矛盾の導き方を対角線論法と言う。

このturingという関数は、一引数関数 xを受け取り、「(x x)を実行せよ」というプログラムをeval-halt?で判定する。

それが停止すると判定されたらループに入り、停止しないと判定されたら停止する。

(define (loop) (loop))
(define (turing x)
  (if (eval-halt? `(',x ',x))
      (loop)
      "done"))

このtという式は、「(turing turing)を実行せよ」というプログラムになっている。

(define t `(',turing ',turing))

ここで、eval-halt?を部分的に定義してみる。

eval-halt?が任意のプログラムの停止性を判定できると仮定すると、上のプログラム tに対しても停止性を判定し、#t か #fを返すはずである。

そこで、tに対して#t を返す場合と#fを返す場合の両方の可能性について考えてみる。

t以外に対しては何を返すか定義しない。それでも以下の議論はうまくいく。

(eval-halt? t) で #f と判定された場合、実際には (eval t) は停止してしまう。これは矛盾である。

(define (eval-halt? x)
  (if (equal? x t)
      #f
      "undefined"))
> (eval-halt? t)
#f
> (eval t)
"done"

そこで、(eval-halt? t) で #t と判定されるように修正すると、今度は (eval t) はループしてしまう。これも矛盾である。

(define (eval-halt? x)
  (if (equal? x t)
      #t
      "undefined"))
> (eval-halt? t)
#t
> (eval t)
*** INTERRUPTED IN loop, (stdin)@55.19
1> ,d

結局、undefined の部分をどのように実装しても、この事態は避けられないので、任意のプログラムの停止性を判定する eval-halt? なるプログラムは作れないことがわかった。


一覧 前へ 次へ