あどけない話

インターネットに関する技術的な話など

Lisper のためのチューリングマシンの停止性問題

停止性問題を読んでも、意味が分からなかった Lisper のために、Lisp のコードで停止性を解説してみる。使用する Lisp としては、SchemeCommon LispEmacs Lisp を検討したが、Emacs Lisp が一番よいと分かったので、Emacs Lisp を使う。

名前を使った概略

halt-p というプログラムは、入力としてプログラム p とデータ d を取る。Lisp なので、p も d も S 式である。halt-p は、p と d を検査し、p に d を与えたときに、停止するか否かを有限時間で判断する。停止するなら t、停止しないなら nil を返す。

machine というプログラムは、入力 x に対して以下のような動作をする。

  • (halt-p x x) が t なら、(machine x) を呼び出すことで同じ作業を繰り返す
    • つまり、x に x 自身を与えたときに、停止すると判断した場合
  • (halt-p x x) が nil なら、nil を返して停止する
    • つまり、x に x 自身を与えたときに、停止しないと判断した場合

では、machine に machine を与えたときはどうなるだろう?

halt-p は、入力に関わらず、必ず t を返す場合:

(defun halt-p (p d) t)
(defun machine (x)
  (if (halt-p x x) (machine x) nil))
(machine 'machine) → 停止しない

machine というプログラムに、machine を与えたときは停止すると、halt-p が判断したにも関わらず、(machine 'machine) は停止しない。

halt-p は、入力に関わらず、必ず nil を返す場合:

(defun halt-p (p d) nil)
(defun machine (x)
  (if (halt-p x x) (machine x) nil))
(machine 'machine)nil を返して停止する

machine というプログラムに、machine を与えたときは停止しないと、halt-p が判断したにも関わらず、(machine 'machine) は停止する。

という訳で、矛盾が導けた。「それだけ?」と思うかもしれないが、チューリングマシンの停止性問題とは、単にこんなものである。つまり、プログラムを走らせる前に、そのプログラムが無限ループに陥るか否かをあらかじめ知る一般的な方法はないということ。「当たり前だ」と思うかもしれないが、あなたが「当たり前だ」としか感じれない素地を作ったのがすごいのだ。

この証明は分かりやすいが、たくさんつっこみどころがあるので、以下ではそれを解決して行く。

ちゃんと自分自身を与える

問題の一つ目は、machine に 'machine というシンボルを渡しているところ。ちゃんとプログラム自体を渡したい。Emacs Lisp のシンボルには、プログラムとデータが別々に束縛されているので、以下のように両方に同じ S 式を束縛することで、この問題を解決できる。

停止するはずなのに停止しない場合:

(defun halt-p (p d) t)
(set 'machine
     (lambda (x) (if (halt-p x x) (machine x) nil)))
(fset 'machine machine)
(machine machine) → 停止しない

停止しないはずなのに停止する場合:

(defun halt-p (p d) nil)
(set 'machine
     (lambda (x) (if (halt-p x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)nil を返して停止する

halt-pをインライン化する

次に問題なのが、名前を使っていることである。名前を定義したりする機能は、公理の一部と考えていいのだろうか? よくわからないので、名前を消すことにする。

まず、halt-p をいう名前を消そう。そのためには、halt-p をインライン化すればよい。

停止するはずなのに停止しない場合:

(set 'machine
     (lambda (x)
       (if ((lambda (p d) t) x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)

停止しないはずなのに停止する場合:

(set 'machine
     (lambda (x)
       (if ((lambda (p d) nil) x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)

自己言及

次は、machine という名前を消すべきである。しかし、machine という名前は、再帰するために使われているので、消すのは厄介だ。名前なしで再帰するための技として、Yコンビネータが知られている。その本質は、自己言及である。

詳細は述べないが、以下のように自分自身に自分自身を適用すると、全体として同じものが返るS式が知られている。

((lambda (x) `(,x ',x)) '(lambda (x) `(,x ',x)))((lambda (x) `(,x ',x)) '(lambda (x) `(,x ',x)))

この技を使って、名前なしで再帰する。

名無しでループ

以下では、自己言及した値を y としている。これを eval すれば、再帰できる。また、プログラムにデータを適用した形になっているので、halt-p に相当するラムダ式の引数が一つになっている。(halt-p は、引数を使わないのでどうでもいいとも言える。)

停止するはずなのに停止しない場合:

(set 'machine
     (lambda (x)
       (let ((y `(,x ',x)))
	 (if ((lambda (p) t) y) (eval y) nil))))
(fset 'machine machine)
(machine machine) → 停止しない

停止しないはずなのに停止する場合:

(set 'machine
     (lambda (x)
       (let ((y `(,x ',x)))
	 (if ((lambda (p) nil) y) (eval y) nil))))
(fset 'machine machine)
(machine machine)
(machine machine)nil を返して停止する

evalだけの世界

machine という名前も不要なので、使わずにやってみよう。

停止するはずなのに停止しない場合:

((lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) t) y) (eval y) nil)))
 (lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) t) y) (eval y) nil))))
→ 停止しない

停止しないはずなのに停止する場合:

((lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) nil) y) (eval y) nil)))
 (lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) nil) y) (eval y) nil))))nil を返して停止する

これで、S式とevalだけで、チューリングマシンの停止性問題を説明できた。

(let で y という名前を付けているじゃんと突っ込みたい人は、let が lambda への糖衣構文だということを勉強しましょう。)