top  Index  Search  Changes  RSS  Login

不完全性定理.改

この文書について

不完全性定理のLisp, Mathematicaによる記述ゲーデルの証明 が理解できませんでした(is-unprovable なんて「実装」できるわけないやん). そこで, 「こんな解釈なのかなあ?」というメモを晒してみます. 口調は解説風ですが山勘で書いているだけですから, つっこみをお待ちしています. (理解のあやしさは, 同趣旨のモナドと比べてもずっとひどいです)

※ lisp と言いつつ文法が scheme 風なのは, 私の趣味

S 式の組み立て方は, 不完全性定理のLisp, Mathematicaによる記述ゲーデルの証明 から丸ぱくりです. その際, lisp としてより自然になるよう, 省ける quote は取り除きました. ただし, 気の効いた処理系だとかえって見にくいので, 50 行ほどの即席 lisp もどきインタプリタ (後述)をでっちあげて実行しています.

(2010.11) 『数学ガール/ゲーデルの不完全性定理』 (結城浩, ソフトバンククリエイティブ, ISBN: 9784797352962)を 流し読みしたのと, S さんに言及していただいたのとがたまたま重なったので, 旧版 から書き直してみました. lisp+ がプログラミング言語でないことを明確にしたのが主な修正です.


まえおき

(1) lisp インタプリタ
(2) lisp を含む(インタプリタをエミュレートできる)ような体系
(3) その体系に関して, 特定の条件を満たす系列が存在するかの議論
をしっかり区別した上で, これらの間をいかに「またぐ」か
が醍醐味のように今は感じています.

S 式を見ると, ついつい「その式の値」というものが何かあるように
思ってしまう lisp 感覚は, (2)(3) の理解を妨げるかも.
たとえば (unprovable-p …) のような S 式が真か偽かの値を持つように
錯覚したり…
自分の旧版もそこがまずかったと思います.

(S さんへのメールより)


「やばい S 式」の組み立て

eval した結果が自分自身と同じになるようなうまい S 式を作れることは有名です. 実際,

((lambda (x) (list x x)) (lambda (x) (list x x)))

という S 式はそうなっています.

(define foo '((lambda (x) (list x x)) (lambda (x) (list x x))))
(equal? (eval foo) foo)
; ==> #t

この foo は次のようなしかけで組み立てられています.

(define w (lambda (x) (list x x)))
(w 'hoge)
; ==> (hoge hoge)
(define foo (w w))
; ==> ((lambda (x) (list x x)) (lambda (x) (list x x)))

それを少しひねれば, (eval bar) が (u bar) と等しくなるような bar も組み立てられます. u は何か好きな関数です.

(define uw (lambda (x) (u (w x))))
(define bar (w uw))
; ==> ((lambda (x) (u (w x))) (lambda (x) (u (w x))))

たとえば,

(define u (lambda (x) (list 'unreachable? x)))
(u '(hoge fuga))
; ==> (unreachable? (hoge fuga))

のような u なら,

(uw 'hoge)
; ==> (unreachable? (hoge hoge))
(eval bar)
; ==> (unreachable? ((lambda (x) (u (w x))) (lambda (x) (u (w x)))))
(u bar)
; ==> (unreachable? ((lambda (x) (u (w x))) (lambda (x) (u (w x)))))
(equal? (eval bar) (u bar))
; ==> #t

後ほど不完全性定理を示すときにこれを使います.

なお, bar の中に u や w が残るのが気にくわなければ, べたに書き下しても構いません.

(define bar2
        '((lambda (x) (list 'unreachable? (list x x)))
          (lambda (x) (list 'unreachable? (list x x)))))
(equal? (eval bar2) (u bar2))
; ==> #t

体系 lisp+

lisp+ という体系を考えます. lisp+ は, 公理と呼ばれる S 式たちと, 推論規則と呼ばれるルールたちから成ります.

  • 公理の例: (equal? □ (car (cons □ △)))
  • 推論規則の例: S 式 □ と S 式 (imply? □ △) が既出なら, S 式 △ を得ることができる

lisp+ において, 次の条件を満たす S 式 (□_1 □_2 … □_n) を, S 式 □_n への到達経路と呼びます. 条件は, 各 □_k が次のいずれかを満たすことです:

  • □_k は公理である
  • □_1, □_2, …, □_{k-1} が既出だとして, 推論規則により □_k を得ることができる

一般に, S 式 □ への到達経路が存在するとき, □ は lisp+ において到達可能であると言います. lisp+ はプログラミング言語ではないことに注意しましょう. lisp+ は, S 式を評価したり実行したりするものではありません.

※ 邪念が浮かばないように, 本来の用語「証明列」「証明可能」をさけて俺用語にしました.

以下, [到達可 □] と書いたら, 「□ を lisp インタプリタで評価して得られる S 式が, lisp+ において到達可能」 と読んでください. たとえば以下はどれも同じ主張です.

  • S 式 (= (+ 1 1) 2) は lisp+ において到達可能である
  • [到達可 '(= (+ 1 1) 2)]
  • [到達可 (list '= '(+ 1 1) (- 5 3))]

到達可能性

lisp インタプリタでの評価結果が t になる S 式は, lisp+ において到達可能です. つまり, lisp で (eval x) が t なら [到達可 x] です. 実際, lisp インタプリタでの評価ステップをそのままなぞることによって, lisp+ での到達経路が得られます (そうできるような公理や推論規則が設定されている前提にします). ……【ポイント1】

r が z への到達経路になっているかどうかは, lisp プログラムで 機械的に判定できます. この判定関数を reach? と名づけます.

(define (reach? r z)
  r の各要素について
  ・公理か?
  ・あるいは, それより前の要素から推論規則で得られるか?
  をチェック.
  さらに, r の最後の要素が z と等しいかもチェック)

lisp インタプリタで (reach? r z) が t になることと, lisp+ において r が z への到達経路であることとは同値です.

ところで, lisp+ は, lisp にはない exist? という組込関数を持ちます. exist? に関しては, 「存在するか?」に相当するような公理・推論規則が lisp+ で設定されていることにしましょう. これを使って

(define (reachable? z)
  (exist? (lambda (r) (reach? r z))))
(define (unreachable? z)
  (not (reachable? z)))

と定めます. マクロではないので, たとえば S 式 (= (+ 1 1) 2) について何か言いたいなら クォートが必要です:

(reachable? '(= (+ 1 1) 2))

無矛盾性

話の前提として, 体系 lisp+ は無矛盾だとします. つまり, 以下が両方同時に成り立つことは決してないとします.

  • [到達可 z]
  • [到達可 `(not ,z)]

さらに, 以下が両方同時に成り立つこともないとします. (ω無矛盾性)

  • x の値が何であっても常に [到達可 `(f ,x)]
  • [到達可 '(exist? (lambda (y) (not (f y))))]

これらの前提のもとでは次のアとイが同値になります.

  • ア. [到達可 z]
  • イ. [到達可 `(reachable? ',z)]

実際, もしアなら, その到達経路 s をもってくると (reach? s z) が lisp インタプリタで t になるはずです. すると前述の【ポイント1】により, [到達可 `(reach? ',s ',z)] です. そこから, lisp+ の公理と推論規則を使って [到達可 `(exist? (lambda (r) (reach? r ',z)))] となるので イが言えます. 反対に, もしアでないとしたら,

(define (f r)
  (not (reach? r z)))

と定めたとき lisp インタプリタで (f x) が常に t になるはずです. するとやはり【ポイント1】により, [到達可 `(f ,x)] です. 一方, イは [到達可 '(exist? (lambda (y) (not (f y))))] と言いかえられますから, ω無矛盾性よりイは決して起きないことが結論されます.

系として, 次のア'とイ'も同値なことに注意しましょう. ……【ポイント2】

  • ア'. [到達可 (eval x)]
  • イ'. [到達可 `(reachable? ,x)]

不完全性定理

前に組み立てた S 式 bar は, lisp インタプリタ上で (eval bar) と (u bar) とが等しくなっていました. この値を baz と名づけます.

bar
; ==> ((lambda (x) (u (w x))) (lambda (x) (u (w x))))
(define baz (eval bar))
; ==> (unreachable? ((lambda (x) (u (w x))) (lambda (x) (u (w x)))))

さらに, baz に not をつけた S 式も用意しておきます.

(define not-baz (list 'not baz))
; ==> (not (unreachable? ((lambda (x) (u (w x))) (lambda (x) (u (w x))))))

さて, 本節の目標は以下を示すことです.

  • ウ. [到達可 baz] ではない
  • エ. [到達可 not-baz] でもない

まずウから示します. もし仮に [到達可 baz] だったとしましょう. これは [到達可 (eval bar)] と [到達可 (u bar)] とを同時に意味します. 先ほどの【ポイント2】により, 前者からは [到達可 `(reachable? ,bar)] が得られます. しかし後者から [到達可 `(not (reachable? ,bar))] でもあるので, 無矛盾性に反します. よって [到達可 baz] ではありえません.

次にエを示します. もし仮に [到達可 not-baz] だったとしましょう. これは [到達可 `(reachable? ,bar)] を意味するので, 前述の【ポイント2】から [到達可 (eval bar)], つまり [到達可 baz] となってしまいます. すると baz と not-baz が共に到達可能なので, やはり無矛盾性に反します. よって [到達可 not-baz] でもありえません.


付録: 即席インタプリタ

「やばい S 式」の組み立てに使った即席 metacircular interpreter のソース. Gauche 上で実行できます.

  • ラムダ式がそのまま表示される
  • いちいち funcall を書かなくてよい

という希望に合う lisp/scheme 処理系が手元になかったので, でっちあげました.


;;; 即席インタプリタと,
;;; それを使った不完全性定理の証明(…に出てくる「やばい S 式」の組み立て).
;;; gosh を起動して, 以下をそのままコピー&貼りつけで OK

;;; インタプリタ

(define (mc lis)
  (for-each (lambda (expr)
              (display (format "~a~%; ==> ~a~%" expr (mc1 expr))))
            lis))
(define (mc1 expr)
  (mc-eval expr *mc-global-env*))

(define (mc-eval expr env)
  (let ((proc (cond ((symbol? expr) mc-eval-symbol)
                    ((eq? (car expr) 'define) mc-eval-define)
                    ((eq? (car expr) 'lambda) mc-eval-lambda)
                    ((eq? (car expr) 'quote)  mc-eval-quote)
                    (else mc-eval-funcall))))
    (proc expr env)))

(define (mc-eval-symbol expr env)
  (mc-get expr env))
(define (mc-eval-define expr env)
  (let ((symbol (cadr expr))
        (val (mc-eval (caddr expr) env)))
    (mc-put! symbol val env)
    val))
(define (mc-eval-lambda expr env)
  expr) ;; 環境? 何それ :p
(define (mc-eval-quote expr env)
  (cadr expr))
(define (mc-eval-funcall expr env)
  (let ((func (mc-eval (car expr) env))
        (args (map (lambda (arg) (mc-eval arg env)) (cdr expr))))
    (mc-apply func args env)))

(define (mc-apply func args env)
  (cond ((procedure? func) (mc-apply-procedure func args env))
        (else (mc-apply-lambda func args env))))

(define (mc-apply-procedure func args env)
  (apply func args))
(define (mc-apply-lambda func args env)
  (let ((vars (cadr func))
        (body (caddr func))
        (local-env (mc-make-env env)))
    (for-each (lambda (v a) (mc-put! v a local-env)) vars args)
    (mc-eval body local-env)))

(define *mc-global-env* '(()))
(define (mc-make-env parent-env)
  (cons '() parent-env))
(define (mc-get symbol env)
  (cdr (assoc symbol (apply append env))))
(define (mc-put! symbol val env)
  (set-car! env (cons (cons symbol val) (car env))))

(for-each (lambda (p) (mc-put! (car p) (cdr p) *mc-global-env*))
          `((list . ,list) (equal? . ,equal?) (eval . ,mc1)))

;;; 動作確認

;(mc1 '(quote a))
;(mc1 '(define x 'a))
;(mc1 'x)
;(mc1 '(list 'b 'c))
;(mc1 '(lambda (x y) (list x y)))
;(mc1 '(define f (lambda (x y) (list x y))))
;(mc1 '(f 'b 'c))
;(mc1 '(equal? (list 'b 'c) (list 'b 'c)))
;(mc1 '(eval '(f 'b 'c)))

;;; 不完全性定理

(begin
  (newline) (display "---- begin mc-interpreter ----") (newline)
  (mc '(
        ;; 練習
        (define w (lambda (x) (list x x)))
        (w 'hoge)
        (define foo (w w))
        (equal? foo (eval foo))
        ;; 本番
        (define u (lambda (x) (list 'unreachable? x)))
        (u '(hoge fuga))
        (define uw (lambda (x) (u (w x))))
        (uw 'hoge)
        (define bar (w uw))
        (define baz (uw uw))
        ;; 確認
        (equal? baz (eval bar))
        (equal? baz (u bar))
        ((lambda (x) (u (w x))) (lambda (x) (u (w x))))
        ;; 補足
        (define not-baz (list 'not baz))
        (define bar2
                '((lambda (x) (list 'unreachable? (list x x)))
                  (lambda (x) (list 'unreachable? (list x x)))))
        (equal? (eval bar2) (u bar2))
        ))
  (display "---- end mc-interpreter ----") (newline))

  • この方面の楽しいほら話で, 「ルミナス」という短編 SF がありました. グレッグイーガン(山岸真訳)『ひとりっ子』(ハヤカワ文庫SF, 2006年, ISBN: 978-4150115944)収録.
  • 自分の専門に近い話が SF に出てくると, あらが気になって冷める. でもむしろ専門どまんなかだと, めくじらたてずに適当に楽しめる. これも一種の不気味の谷現象やんね.
  • この文書は, 谷の手前(素人側)で「ルミナス」を楽しく読める程度の素人が書いたものです.
(Please LogIn to post comments.)

Last modified:2010/11/17 21:25:42
Keyword(s):
References:[不完全性定理]