停止性問題を読んでも、意味が分からなかった Lisper のために、Lisp のコードで停止性を解説してみる。使用する Lisp としては、Scheme、Common Lisp、Emacs 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 への糖衣構文だということを勉強しましょう。)
