Hatena::Groupbugrammer

蟲!虫!蟲!

Esehara Profile Site (by Heroku) / Github / bookable.jp (My Service)
過去の記事一覧はこちら

なにかあったら「えせはら あっと Gmail」まで送って頂ければ幸いです。
株式会社マリーチでは、Pythonやdjango、また自然言語処理を使ったお仕事を探しています

 | 

2011-10-16

[]Lispによる「不完全性定理についてのゲーテルの証明の一部」の一部について、Pythonで記述できることの証明 06:04

 恐らく中二病を患っている皆様でしたら、自己言及とかパラドックスとかが好きだと思われます。

 以前にLispの人達は、不完全性定理の主張が記述できるという話をしています。

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

 「プログラミング言語なんてどれも同じと思っている人は下の3つをJavaC++で書いてください」とは、とても不穏な発言ですね。また、このサイトでこんな言葉が引用されています。

ミンスキー「ゲーデルLispを思いついておくべきだった。もし彼がLispを思いついていたならば彼の不完全性定理証明はもっと簡単なものになっただろう」(ホフスタッター「メタマジック・ゲーム」)

 とはいえ、この時代は恐らく、言語の選択肢としてJavaC++Lisp(あれ?Perlは?)くらいしかなかった時代の話だと考えても差し支え無い気がする。時代は代わり、LL言語としてRubyPythonといったものが現れ始めました。Rubyは詳しく無いので、わかりませんが、少なくともPythonは自己言及に強い言語とでも呼べるでしょう。Pythonはlambdaを搭載して、ますますLispっぽくなっていますね。(ただ、Pythonicという評価からはlambda使うべきなの?みたいな話がされていて……なんだよ、Pythonicって!!)

 つうわけで、初級の不完全性定理についてのゲーデルの証明の一部Pythonで書き直すという作業をやってみましょう。

準備体操

 要するに、自分自身を実行できるプログラムを作ればいいということらしい。

 Pythonは異様に簡単。

def f(x):
    return "f(" + x._name_ + ")"

 ちなみに、lambdaは名前として"<lambda>"という関数を持っているため、上記のようなアプローチは使えない。何かいい方法でもあるのかな。取りあえず、このように実装してやることによって

>>>f(f)
'f(f)'
>>>f(f) == eval(f(f))) 
True

 となる。ポイントは、__name__が自分の名前を保持しているということで、これによって、引数関数(あくまでも関数。例えばString型を与えたらErrorを返す)を参照することが出来る。そして、その名前は自分の内部でも使用可能である。

 そのあたりの話に関しては、前のエントリで書いたので参考にしてください。

『思想の中の数学的構造』の「生成の概念」をPythonでプログラミングしてみる - 蟲!虫!蟲! - #!/usr/bin/bugrammer

ゲーテルの定理について

「表現に名前を対応させるが、表現の中で名前を扱うことができるためにレベルが縮退する」というのが以下の方法の本質である。(中略)

 xが妥当な証明でないならFalseを返し、妥当な証明なら証明された定理を返すような関数 valid-proofQ があるとする(これは難しくないはず)。すべてのxについて valid-proofQ[x] がyと等しくないとき、yは証明不可能である。このことを主張する述語をis-unprovableとする。

 この文章をPythonにするならどのように考えるべきか。

 まずこのサイトの文章を読む感じだと、そもそも「妥当な証明か否か」を検証する関数valid-proofQは定義されていない。ただ、そのような実装があると仮定している。そして、それが証明不可能であるということを主張する述語?があるとしている。

  • 証明不可能かどうかを判定する仮関数 valid-proofQが存在する。
  • 証明不可能であるという表現=データ構造が存在する。

 そのまま愚直に書くならば次のようになるだろう。

("is_unprovable",eval(g(g)))

 わざわざタプルに書き直したのは、表現というのは、恐らく「そのように判定された」という意味だと考えることにしたからだ。さて、このように結果が出力されたとして、評価にかけてみる。

def g(x):
    return '("is_unprovable",eval(g(' + x.__name__ + ')))'
修正(2011.10.16)

これタプルじゃなくて文字列だ……。なので、正確にはこうする。

def g(x):
    return ("is_unprovable","eval(g(" + x.__name__ + "))")
で、
g(g) == eval(g(g)[1][5:-1]

が正しいような気がする。

修正以前の文章

 次にパースする。

>>> "(".join(g(g).split("(")[2:])[:-2]
'g(g)'

 これを、文字列のようにevalする。

>>> g(g) == eval("(".join(g(g).split("(")[2:])[:-2])
True

 上記のサイトでは次のように書いてある。

g[g]は証明可能であろうか。証明可能だという結論はg[g]の主張と矛盾する。よってg[g]は証明可能ではない。しかしこれはg[g]の主張である。よって、g[g]は証明不可能だが真である

 もしこの証明を鵜呑みにするならば、上記もまた証明不可能であり、真である。

ただ、これは主張であって「証明」ではない気はする

 とはいえ、これはあくまでも「プログラム的に書けばこういう風に記述できる主張であって、実際の証明は別だよ」というのは覚えておいたほうがいいのかな。実際、俺自身が数学証明というのをあまり理解していないし、それで進みすぎるとソーカル事件(でたらめな論文を送りつけたら、とある人文科学系の学術雑誌に通ってしまったという事件。詳しくは検索してください)になってしまうので、この辺で手を引いておくといいかなと。

 この「Lispによる不完全定理の記述」って何だ?という話を考えたければ、次の文章を読めばいいのかしら。

 Lisper のためのゲーデルの不完全性定理 - あどけない話

 k16’s note: Lisperのためのゲーデルの不完全性定理の反証不可能性について考えてみた

 howm wiki - 不完全性定理.改

だからたぶんチャイティンの元記事は、不完全性定理のフレーバーをLispならS式で表せるぜ、という話であって、それは、不完全性定理のフレーバーを自然言語ならうそつきのパラドクスで表せるぜ、という話と大きく違わないのではないかと思った。

 あとは元の本である『知の限界』を手に入れたらいいのかしら。変則的プログラムのネタには困らなさそう。

prajnaprajna2011/10/19 21:11知の限界は、オンラインで公開されています。(http://www.cs.auckland.ac.nz/CDMTCS/chaitin/unknowable/index.html)。日本語よりは読みやすいと思いますので、是非。

nisemono_sannisemono_san2011/10/26 01:54お返事送れましたー。うれしい情報をありがとうございます。
さっそく読んでみますね!

 |