top  Index  Search  Changes  RSS  Login

howm wiki - IncompletenessTheorem.rev Diff

  • Added parts are displayed like this.
  • Deleted parts are displayed like this.

!!この文書について

[[不完全性定理のLisp, Mathematicaによる記述|http://www.iba.k.u-tokyo.ac.jp/~yabuki/tip/lisp/unknowable/unknowable.html]]

[[ゲーデルの証明|http://www.iba.k.u-tokyo.ac.jp/~yabuki/tip/lisp/unknowable/godel.html]]
が理解できませんでした(is-unprovable なんて「実装」できるわけないやん).
そこで,
「こんな解釈なのかなあ?」というメモを晒してみます.
口調は解説風ですが山勘で書いているだけですから,
つっこみをお待ちしています.
(理解のあやしさは, 同趣旨の[[モナド]]と比べてもずっとひどいです)

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

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

(2010.11)
『数学ガール/ゲーデルの不完全性定理』
(結城浩, ソフトバンククリエイティブ, ISBN: 9784797352962)を
流し読みしたのと, S さんに言及していただいたのとがたまたま重なったので,
[[旧版|IncompletenessTheorem]] から書き直してみました.
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|http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-26.html]]
のソース.
[[Gauche|http://www.shiro.dreamhost.com/scheme/gauche/index-j.html]]
上で実行できます.

* ラムダ式がそのまま表示される
* いちいち 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 に出てくると, あらが気になって冷める. でもむしろ専門どまんなかだと, めくじらたてずに適当に楽しめる. これも一種の[[不気味の谷現象|http://ja.wikipedia.org/wiki/%E4%B8%8D%E6%B0%97%E5%91%B3%E3%81%AE%E8%B0%B7%E7%8F%BE%E8%B1%A1]]やんね.
* この文書は, 谷の手前(素人側)で「ルミナス」を楽しく読める程度の素人が書いたものです.

{{comment}}
----
{{toc}}