停止問題の解決不可能性についてのチューリングの証明

Up: 不完全性定理のLisp, Mathematicaによる記述

停止問題の解決不可能性についてのチューリングの証明

G. J. Chaitin Turing's Proof of the Unsolvability of the Halting Problem の例をMathematicaとCommon Lispで書き直した

ラッセルのパラドックス:自分の髭を剃らない村中すべての男の髭を剃る床屋

チューリングの定理:任意のプログラムが停止するかどうかを判断できるようなアルゴリズムは存在しない


Lispの場合

ElispにあるfsetをCommon Lispでも定義しておく(その都度(setf (symbol-function 'a) b)と書いてもいい)。

(defun fset (a b) (setf (symbol-function a) b))

第2章に「letを使わなければ、与えられた値、たとえばLISPプログラム計算量を持つ、最小式のサイズが、環境に左右されない」とある。よくわからないがそのとおりにした。

与えられた式が値を持つかどうかによってtまたはnilを返すような関数(haltQ)があるとする。

関数turingはまず入力xに対しz=(x 'x)をつくる(xを展開してからquoteがつくことに注意)。そしてzが停止するなら停止しない、zが停止しないなら停止する。turingにturing自身を作用させると、止まらない時に限り止る関数を作れる。まずは止まらないとした場合(ifの条件がnilになっている)、

> (setq turing
      '(lambda (x)
         ((lambda (haltsQ)
           ((lambda (z) (if (funcall haltsQ z) (eval z) nil))
            (print `(,x ',x))))
          '(lambda (sExp) nil))))
(LAMBDA (X) ((LAMBDA (HALTSQ) ((LAMBDA # #) (PRINT `#))) '(LAMBDA (SEXP) NIL)))
> (fset 'turing turing)
(LAMBDA (X) ((LAMBDA (HALTSQ) ((LAMBDA # #) (PRINT `#))) '(LAMBDA (SEXP) NIL)))
> (turing turing)

((LAMBDA (X)
   ((LAMBDA (HALTSQ)
      ((LAMBDA (Z) (IF (FUNCALL HALTSQ Z) (EVAL Z) NIL)) (PRINT `(,X ',X))))
    '(LAMBDA (SEXP) NIL)))
 '(LAMBDA (X)
    ((LAMBDA (HALTSQ)
       ((LAMBDA (Z) (IF (FUNCALL HALTSQ Z) (EVAL Z) NIL)) (PRINT `(,X ',X))))
     '(LAMBDA (SEXP) NIL)))) 
NIL

次に止まるとした場合(ifの条件がtになっている。大量に出力してしまうからprintは使えない)、

> (setq turing
      '(lambda (x)
         ((lambda (haltsQ)
           ((lambda (z) (if (funcall haltsQ z) (eval z) nil))
            `(,x ',x)))
          '(lambda (sExp) t))))
(LAMBDA (X) ((LAMBDA (HALTSQ) ((LAMBDA # #) `(,X ',X))) '(LAMBDA (SEXP) T)))
> (fset 'turing turing)
(LAMBDA (X) ((LAMBDA (HALTSQ) ((LAMBDA # #) `(,X ',X))) '(LAMBDA (SEXP) T)))
> (turing turing)
Error: An allocation request for 128 bytes caused a need for 3407872
       more bytes of heap. This request cannot be satisfied because you
       have hit the Allegro CL Trial heap limit.  If you wish to
       purchase Allegro CL please contact Franz Inc. at sales@franz.com
       or by calling (510) 548-3600.
[condition type: STORAGE-CONDITION]

次のように書けば自己限定的

((LAMBDA (X)
   ((LAMBDA (HALTSQ)
      ((LAMBDA (Z) (IF (FUNCALL HALTSQ Z) (EVAL Z) NIL)) (PRINT `(,X ',X))))
    '(LAMBDA (SEXP) NIL)))
 '(LAMBDA (X)
    ((LAMBDA (HALTSQ)
       ((LAMBDA (Z) (IF (FUNCALL HALTSQ Z) (EVAL Z) NIL)) (PRINT `(,X ',X))))
     '(LAMBDA (SEXP) NIL))))

Mathematicaの場合

> turing =
    Function[{x},
      Function[{haltsQ},
          Function[{z}, If[haltsQ[z], ReleaseHold[z], False]]
            [Print[x[Hold[x]]]]]
        [Function[{sExp}, False]]];
> turing[turing]
Hold[Function[{x}, 
      Function[{haltsQ}, 
          Function[{z}, If[haltsQ[z], ReleaseHold[z], False]][
            Print[x[Hold[x]]]]][Function[{sExp}, False]]]][
  Hold[Hold[
      Function[{x}, 
        Function[{haltsQ}, 
            Function[{z}, If[haltsQ[z], ReleaseHold[z], False]][
              Print[x[Hold[x]]]]][Function[{sExp}, False]]]]]]
False
> turing =
    Function[{x},
      Function[{haltsQ},
          Function[{z}, If[haltsQ[z], ReleaseHold[z], False]]
            [x[Hold[x]]]]
        [Function[{sExp}, True]]];
> turing[turing]
- $IterationLimit::"itlim": "Iteration limit of \!\(4096\) exceeded."
- $IterationLimit::"itlim": "Iteration limit of \!\(4096\) exceeded."
Hold[Function[{z$}, If[Function[{sExp}, True][z$], ReleaseHold[z$], False]][
    Hold[Function[{x}, 
          Function[{haltsQ}, 
              Function[{z}, If[haltsQ[z], ReleaseHold[z], False]][
                x[Hold[x]]]][Function[{sExp}, True]]]][
      Hold[Hold[
          Function[{x}, 
            Function[{haltsQ}, 
                Function[{z}, If[haltsQ[z], ReleaseHold[z], False]][
                  x[Hold[x]]]][Function[{sExp}, True]]]]]]]]