不完全性定理の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 さんへのメールより)
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+ は, 公理と呼ばれる S 式たちと, 推論規則と呼ばれるルールたちから成ります.
lisp+ において, 次の条件を満たす S 式 (□_1 □_2 … □_n) を, S 式 □_n への到達経路と呼びます. 条件は, 各 □_k が次のいずれかを満たすことです:
一般に, S 式 □ への到達経路が存在するとき, □ は lisp+ において到達可能であると言います. lisp+ はプログラミング言語ではないことに注意しましょう. lisp+ は, S 式を評価したり実行したりするものではありません.
※ 邪念が浮かばないように, 本来の用語「証明列」「証明可能」をさけて俺用語にしました.
以下, [到達可 □] と書いたら, 「□ を lisp インタプリタで評価して得られる S 式が, lisp+ において到達可能」 と読んでください. たとえば以下はどれも同じ主張です.
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+ は無矛盾だとします. つまり, 以下が両方同時に成り立つことは決してないとします.
さらに, 以下が両方同時に成り立つこともないとします. (ω無矛盾性)
これらの前提のもとでは次のアとイが同値になります.
実際, もしアなら, その到達経路 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】
前に組み立てた 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] だったとしましょう. これは [到達可 (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 上で実行できます.
という希望に合う 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))
Keyword(s):
References:[不完全性定理]