- 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}}