これは圏です(はてな使ったら負けだとおもっていた)

きっと何者にもなれないつぎの読者につづく。

「カウンセラーのパラドックス」の解題――自己言及ぺろぺろ

先日(と云ってももう2週間以上も前だけれど)上げた『凄腕すぎたカウンセラーのはなし ——または、カウンセラーのパラドックス - はてな使ったら負けだと思っている』と云う記事の真意、みたいなのを解説したいと思います。

先に述べてしまうと、嘘つきのパラドックスラッセルのパラドックス不完全性定理といったものに着想を得たものでした。なので、以下ではそれとどういう関係があるのか、と云う話になっていくんですが、なにぶん数学好きな学部二年の書いた文章ですので誤りや誤解などがあるかもしれません。それに、あくまで"着想"であって、正確な解説と云う訳ではありません。なので、面白そう!と思ったひとは自分で調べてみると面白いです。
また、読まれておかしなところに気付かれたら是非ご指摘ください。

では、以下本編です。

ラッセルのパラドックス

論理とかに詳しい方は気付かれたと思いますが、これの元ネタになっているのは『床屋のパラドックス』と云う奴です。これがどういうのかと云うと、

ある街の床屋は、自分で自分の髭を剃らない人だけの髭を剃るそうです。
では、この床屋自分の髭を剃るのでしょうか?

と云う奴です。自分で髭を剃るとすると、『自分で剃らない人だけ剃る』と云う前提に反しますし、剃らないとすると前提から剃らなくてはいけなくなって矛盾します。

このパラドックスは、いわゆる素朴集合論におけるラッセルのパラドックスとの説明として良く使われます。ラッセルのパラドックスと云うのは、

S = {x | x ∉ x}*1

なる集合Sを考えたとき、果して S は S に含まれるのか否か?と云う問題です。

これも先程の床屋のパラドックスと同様に、S∈S とも S ∉ Sとも決定出来ず、たったこれだけの式から素朴集合論の矛盾が導かれてしまって、当時の人々を大いに悩ませました。集合論はあらゆる数学の基礎を成しているので、こいつは大問題だったんです。

そこで、「取り敢えず集めれば集合」みたいな自由な感じだった素朴集合論を捨てて、どこからどこまでが集合なのか、と云うことをしっかり決めよう、と云う運動が起こりました。そうして産み出されたのが、公理的集合論と呼ばれる集合論たちです。たち、と云うのは幾つか種類があるらしいので*2。大雑把に云うと、世の中には『集合』と『クラス』の二種類があって、その内なにかの要素になれるのは集合だけ、と云うような取り決めがあります。で、そういった諸々の公理から、『そもそも集合Sなんて存在しねーんだよ!!』と云う結論が出るようになりました。ヨカッタネ!


で、件のカウンセラーのパラドックスでは、『自分のことが良くわかっている』と云うのが『自分自身を要素に持つ』と云う命題に対応していたわけです。

ゲーデル不完全性定理と嘘つきのパラドックス

前述のラッセルのパラドックスと云うのは、理解するのに色々な比喩が考えだされていて、他にもグレリングのパラドックス『「自己形容的でない」は自己形容的か?』、市長市のパラドックス『自分の治める市に住んでいない市長だけが住む市の市長は何処に住む?』、図書目録のパラドックス『自分自身の書名が含まれていない図書目録を集めた図書目録は自分自身の書名を載せるべき?』、など色々あります*3。僕が好きなのは市長市です。


で、そんな比喩が既に沢山あるのに、なんであんまり違いがわからないような、『カウンセラーのパラドックス』とか云うのを今更考案したのかと云うと、この比喩は微妙にゲーデル不完全性定理の比喩にもなってるんじゃね!?と云うことに気付いたからです。

ゲーデル不完全性定理と云うのは大雑把に云うと、

無矛盾で算術が使えるくらい強い体系だと、

  1. その体系内では肯定も否定も出来ないような命題が存在する
  2. 自身の無矛盾性もそんな命題のひとつ

と云うような感じです。具体的には、算術が使えると或る種の自己言及が出来て、

俺は証明出来ない!!!

と主張する命題が作れちゃうんだそうです。

で、この命題はその体系内だと確かに証明出来ないんですが*4、その体系の外側からみると、正しいと云うことがわかります。
何でかと云うと、結局その体系内では証明出来ていないので、それは正にこの命題自身が主張していることだからです。

で、これはカウンセラーのパラドックスだと『自分で考えてもわからなかったから、師匠に相談にいった』くだりに対応するわけです。


なんで一つの比喩でラッセルのパラドックスゲーデル不完全性定理も説明出来るのかと云うと、この二つの根を辿っていくと、嘘つきのパラドックス*5と呼ばれるものに辿り着くからです。それは、

クレタ人のエピメニデスが、「クレタ人はみんな嘘つきだ!」といった

と云うパラドックスです。エピメニデスが正直者なのか嘘つきなのか考えようとすると泥沼にはまってしまいます。

……が、この命題を良く考えると実はパラドックスになっていない*6ので、より簡潔で本質的な表現は下のようになります。

「この文章は偽である」と云う文章は真か偽か?


ラッセルのパラドックスゲーデル不完全性定理も、この嘘つきのパラドックスと同じ様に自己言及の形を持っています。ラッセルのパラドックスの場合は「そんな自己言及はそもそも出来ないよ!」と云うのが結論で、他方で不完全性定理の場合は「真偽に関しての自己言及は上手くいかないけど、証明可能性については言及出来るよ!」と云う発見が核になっているわけです。

こういった具合に、根本となる原理の部分は同じ(結論はちがいますが)であったため、一つの比喩でそれなりに両方ともの雰囲気が醸せたのかな、と。


と云う訳で、何か結論があるわけじゃないですが、以上でした。

*1:自分自身を要素に持たない集合全体の集合、と読みます

*2:ZF(C)、BGといったのはきいたことがあるのですが、他にもNFUとかいろいろあるらしいです

*3:それぞれどうやってパラドックスに陥るのかは読者への課題とします。

*4:証明は読者への課題とします!

*5:クレタ人のパラドックスとも呼ばれます

*6:証明は読者への課題t(ry

凄腕すぎたカウンセラーのはなし ——または、カウンセラーのパラドックス

ある街に、凄腕のカウンセラーが住んでいました。

その街に住む、自分のことがよくわからないぞー、ってなってしまった人が、カウンセラーのところに相談にいくと、たちどころに問題を見抜いて、解決してくれるのです。
なんでそんなことが出来るのかと云うと、そのカウンセラーさんは「自分のことがよくわからないひとリスト」と云うのをもっていて、そのひとたちのことを既に徹底的に調べていて、よくわかっているからなのでした。
プライバシーの侵害だ!と云う声もあるかもしれません。でも、そこはカウンセラーさんも職業人で、カウンセリング以外には使いませんし、だいいち自分のことをよくわからないひとは遅かれ早かれカウンセラーさんのところに来るので、結局は自分の患者であるのと同じことです。

それだけ情報収集能力があると不安かもしれません。しかし、自分のことをよくわかっている人達は満ちたりている人達で、カウンセラーさんのところに相談しにくる必要がないのでそもそもカウンセラーさんも集めません。自分の仕事で手一杯です。それに、自分のことをよくわかっているのだから、カウンセラーさんが自分のことを調べていたらすぐにわかって、提訴されてしまいます。あぁこわいこわい。だからそんなひとのことは何も知りません。


そんな訳で、カウンセラーさんは自分の特技を上手く生かして、街の人達を助けて今日も繁盛しているのでした。


そんなある日。ひとりの患者さんがいいました:
「いやあ、先生は本当に何でもわかってるんですねえ。御自分のこともよぉくご存知なんでしょう?凄いなあ……」

その場では「いえいえ、それほどでもないですよ……」と流したカウンセラーさんでしたが、後で思い返してみて困ったことになってしまいました。「はて、本当に私は自分のことをよくわかっているのだろうか?」

「もし、私が自分のことを良くわかっているとすると、ポリシーから私は自分のことをよくわからない筈だ。じっさい、今もよくわかっているかこうして考えている。しかし、これは矛盾だ!自分のことを知っている筈なのに知らないことになってしまった。と云うことは良くわかっていないんだな……」
カウンセラーさんはこの悲しい現実を受け止めつつも、まあ、仕方ないか、と思おうとしました。しかし、ここでまた引っ掛かってしまいました。


「では、私は自分のことを良くわかっていないんだな。とすると、またポリシーより私は既に自分のことを徹底的に調べてよくわかっていないといけない。おかしい、これはこまったぞ……」


そんなこんなで、カウンセラーさんは苦悩のドン底に落ちてしまいました。いったいこのジレンマをどう解消すればいいのか……。
こんなことをずっと考えている内に、段々と眠れない夜が続き、遂には診療所をお休みにしてしまう始末です。
そうこうしている内にも、悩める人達はまだそこら中にいます。かつて治療してもらった患者さんたちは、少しでも早い恢復を祈って花や差し入れを診療所の前に差し入れていきます。「はやく元気になってください」と手紙を認めるひとも多かったようです。

しかし、幾ら励ましの声を聞き、幾ら差し入れの山を見ても、カウンセラーさんの悩みは解決しません。嗚呼、どうすれば……。

後日談

それから更に何日かが過ぎ、カウンセラーさんは思い付きました。「そうだ!都会のカウンセラーに相談にいこう!」

都会のカウンセラーはカウンセラーさんの師匠に当たる人です。長いこと会っていませんが、腕は確かで、修行時代はいつも的確なアドバイスをくれていました。
あのひとならきっと、この状況を打破してくれる!その希望を胸に、カウンセラーさんは師匠に会いに遠路はるばる都会へと向かいました。


* * *


「……と云う訳なんです。師匠、何か素晴しい解決はないものでしょうか」
「ああ、それなら簡単だよ。」
「えっ、本当ですか?」
「ああ。君は自分のことをよくわかっているか、わかっていないんだろう?」
「ええ、そのとおりです。」
「じゃあ、君は自分のことをよくわかっていないことになるね。だって、そんなこともわかってないんだから・・・。」

OS X で早稲田学内ネットワークから SSH & GitHub を使用する方法

早稲田学内ネットワークから GitHub に接続したり SSH 使ったりするには汎用プロクシを使う必要がある訳ですが、汎用プロクシは Snow Leopard に対応していませんね。これはひどい

メールはまあ Gmail とかを使っていればブラウザから確認出来る訳ですが、 ssh や Git はそういう訳にもいきません。
自分なりにその解決策を見付けたので、ここにメモしておきます。


Proxy のアドレスなどは早稲田のものに準拠して書いてますが、多分他の大学やらなんやらの環境の人もその辺りを弄れば使えるのではないでしょうか。

まず connect を入れる

よくわかんないんですが、connect.c と云うのを入れると、 SOCKS Proxy 越しに ssh に繋げるみたいです。やったね!

Homebrew を使っているひとは簡単に、

$ brew install connect

で入ります。使っていないひとは connect.c を直接落としてきて、指示に従って

$ gcc connect.c -o connect -lresolv

コンパイル出来るので、パス通ってるところに置けばよいです。

ssh の設定

次に、ssh の設定です。
~/.ssh/config に以下の内容を追記します。

Host github_wsd
  User ユーザ名
  HostName ssh.github.com
  Port 443
  ProxyCommand connect -H www-proxy.waseda.jp:8080 %h %p

この例では github_wsd と云う名前で github とのやりとりを出来る様になります。

git の設定

最後に利用したい Git の設定です。GitHub を利用したいレポジトリ内で次を実行します。

$ git remote add origin_wsd git@github_wsd:ユーザ名/Project名.git

これだけ。git は ssh で繋ぐときのアカウント名は git で共有鍵でユーザの識別をしている模様。GitHub を日常的に使っているのなら共有鍵は既に設定されているのでこのままで大丈夫なのです。

で、あとは、いつもと同じ様に

$ git push origin_wsd master

などとして使うことができる。やったね!

PFIサマーインターンに参加していました

8/1〜9/30 の二ヶ月間、株式会社プリファードインフラストラクチャー(通称 PFI)でインターンに参加して来ました。
報告記事を書かなくては……と考えている内に大分時間が経ってしまってこんな時期になってしまいました。

採用まで

夏休み特に予定がなかったので、何か今までとは違ったことに挑戦しようと思っていたところ、Twitter上で id:pi8027 さんが言及しているのを見掛けて、面白そうだと思って応募したのでした。
履歴書を埋めるのが中々の一苦労で、プログラミングコンテストなども余り実績がないし、開発したものもそんなに大規模なものはない。特に苦労したのが『受賞歴』の欄で、仕方がないので高校時代の演劇での受賞歴とTOEICの点数を書くと云う暴挙に。昔現実逃避に問題を解きまくっていた名残かHaskell ゴルフのランキングで4位だったので、ちゃんと書けた実績としてはそれぐらい。

せめて、と思って志望動機の欄に Haskell への愛を書き連ねて、送信。何かが間違っている気がする。


その後、書類審査は奇跡的に通過していたので、面接へ。
ちょっと書類で Haskell 愛を強調しすぎて居たので、志望動機を真面目に答えようとする……も、気付くと「一番大きいのは Haskell が開発で使えること」「Haskellは使えないという固定観念を打ち殺してやりたい」などと力説している。「他の人達とは別の言語でやりとりすることになりますが、どうですか?」と問われ「ええと……C++は出来ませんが Ruby なら出来ます……」と自分の失言に気付き何とか軌道修正を図ろうとする。だって好きなんだもん……

その後、問題へ。fmfm、花札シャッフルか……と、素直に Haskell で書く。しっかり動いている様に見える……あれ?テストケースを通過していない!?
余裕があった筈が焦る。結果的には返す値を間違えていたと云うショーモナイバグで、何とか時間内に修正出来たものの、やっちまったなぁ……という感じである。
その後、「数学科に行きたいと云うことでしたが、それじゃあこの発展問題を考えてみてください」と、カードの枚数が何万枚に増える、と云う条件での出題。飽く迄参考で解けなくても構わない、と云うことだったんですが、ここでもテンパってしまう。取り敢えず漸化式で考えるんだろうなあ、と云うことはわかる。もうその時点で解けている様なものなんですが、何故か一般項を出そうと考えて泥沼に嵌りタイムアウト

この分じゃあ多分落ちてるだろうなぁ……などと思いつつ帰途についたのでした。夏休みなにしよう……


……と思っていたら、

この度は、ご面談に来ていただきありがとうございました。
選考の結果、「採用」と決まりました。よろしくお願いします。

何故か採用!!

奇蹟は重なるものだなぁ……と。これはきっと Haskell 枠で合格したんだ!と前向きに捉えることにしました。 Haskellばんざい!!!

インターン前半

最初の週は大学の講義があったため、初日の顔合せは午前中だけ参加、と云う形に。
会議室で自己紹介。他のインターン参加者は T京大学やT島大学の修士課程・博士課程であることが早晩明らかになり、大学一年の自分が参加してしまって良かったのだろうか……明らかに場違いだどうしよう……などと恐れ戦く。

しかし、ここで引いてしまっては意味がない!!と「Haskell を使っています」「メタがすき」「実際の開発に触れてみたい」「分散処理と自然言語処理に興味があります」「Haskell は unemployed *1 じゃない、私は採用された、 I employed だ!!!」と良くわからないことを喋くり散らす。

なんとかその場を乗り切った後は、環境の setup をして、お昼ごろにやってきたメンターの id:tanakh さんとインターンの課題について打ち合わせをする。

自然言語処理・分散処理、と云うことを考えると、膨大なデータ量があって解析のしがいがありそうな Twitter をテーマに何かサービスをつくろう、と云うことになる。その後二、三日程度の話し合いの結果、「樹形な tweet の自動まとめ生成サービス」をつくろう、と云うことに決定。


インターン同期生の大野さんもついったー関連のサービスを作ろうとしているようだったので、今後の方針についてメンターの方々も交えて話し合い。結果、当面の間僕は Twitter のクローラを作成し、大野さんは in_reply_to で接続されたグラフを生成する方法を模索することに。


あとの資料に書きましたが、中々沢山のついーとを一気に取得すると云うのは大変で、大量のデータを分担して取得して、それを同時に処理しなくてはいけないので、なかなか良い経験になりました。
Haskell はこの辺りの並行処理の機構が充実していて非常に書き易かったです。部分的に Ruby で書かれている部分があるのですが、 MessagePack-RPC を使うことで簡単に Haskell - Ruby 間でも通信することが出来てとても便利でした。MessagePack ++

PFIセミナー

インターン参加者はどんな話題でも良いのでセミナーで発表をすることになっています。

色々迷った挙げ句、僕は "Metaprogramming in Haskell" と云う題目で発表することにしました。下がその発表資料。

スライド中で使われた例は GitHub にあります。コンパイルタイム『交響曲第五番 運命*2』など斬新な試みが沢山!


しかし、PFIHaskell を使っている方は tanakh さんと nushio さんくらいだったので、もう少し基本的な説明をしてからでないとわかり辛かったかもしれません……。反省です。
一週間近く関連する論文などを読み耽ってスライドを書いていたので作業が滞ってしまう事態に……力を入れすぎましたね……。

後半

クローラはひとまず完成と云うことで、後半は自動まとめ生成サービス logtter の制作に。
Haskell には fgl と云う優れたグラフ用ライブラリがあって、辺や連結部の抽出は割と楽に出来ました。

問題は、どうやって発言同士を繋げるかで、なかなか難しい。単語抽出も、MeCab などを使うより、単語辞書を用意して trie 木に突っ込み、連続最大一致部分を探すのが効率が良かったりして、この辺りは色々と相談に乗っていただきました。

この辺のヒューリスティックスは単純でも思ったより効果があったりするんだなぁ……と感心すること頻り。まだまだ全然初歩だけですが、こういったアルゴリズムやデータ構造をもっと勉強せねば……と。trie 木が本当に速くてびっくりしました。


ところが、終盤に差し掛かったときから クローラ が暴走する様に。その原因究明と解決の模索に一週間半ほど費してしまって、予定が押してしまい、logtter の方に殆んど時間が割けず……

とりあえず、それなりに繋がったグラフが吐ける状態までもっていき、HTML出力部を大急ぎで作成して最終発表と云う運びになりました。

最終発表 & 総括

そうこうしている内最終発表。緊張の余り RedBull を三本も呑んでしまう。日頃でも最大二本くらいまでだったのですが、これで僕も一人前かもしれません。

以下が最終発表資料。

最終発表の模様は PFI Intern 2010 Final Presentation 1PFI Intern Final Presentation 2 にあるようです。

資料でも再三再四強調していますが、今回のインターンを通して『Haskell は実用言語である』と云う仮説は真実である、という確信が持てました。その証拠に、logtterの 実に95%は Haskell (残りは Ruby) で書かれていますし、近々100%になる予定です。
今後もPFIでアルバイトさせて頂けることになったので、logtter をひとまず完成させてデプロイするところまで行く予定です。Twitter でも思った以上の方々に logtter に興味を持って頂けたようで、大変嬉しい限りです。


今回のインターンを通して、プログラマとして大きな成長をすることが出来たと思います。Haskell での開発ノウハウもそうですし、プロの現場に触れてプログラマとしての考え方、ソフトウェアを売るということ、そう云ったものを少しでも学ぶことが出来ました。


今回のインターンで学んだもうひとつのことは、RedBull の偉大さです。僕は、炭酸が飲めません。苦手というのではなく、飲めないんです。小さいころから。ですから RedBull にははじめ大きな抵抗感があったのですが、飲んでいる内に、RedBull は違う、これは素晴しい飲み物である、と云うことが段々と腑に落ちて来ました。はじめの内は一日一缶程度と云う入門者でしたが、後半では一日に二缶飲む様になり、多い時で漸く三本飲むようになってきました。これは偏に今回のインターンのお陰です。もしインターンに参加しなければ、また、インターンの職場がPFIの様な常に冷蔵庫に RedBull が二十本以上常備されているような環境でなければ、僕は RedBull の素晴しさに触れることもなく一生を終えていたに違いありません。炭酸が飲めなかった僕が「こいつ酒の前にRedBullの味覚えやがった」と CTO ことちくわさんに云われるまでになることはなかったのではないでしょうか。RedBull gokgok!


そんなこんなで、最初は長く感じられた PFI サマーインターンでしたが、実際はあっと云う間で、足りないくらいでした。同時に、これだけ中身の詰まった二ヶ月間はなかなか無かったです。


来年以降もインターンは行われる様ですので、気になる人は是非是非参加しましょう!

*1:http://soup.johl.io/post/23925622/Why-Haskell-Community-unemployed

*2:音源は別途ダウンロードのこと

copy_term

色々さまよった結果、swiplのMLに辿り着き、些か機能的な違いはあれど、copy_term/2を使えば良さそうと云うことはわかった。詳しくは明日調べよう。

と思ったけど、やっぱりちゃんと動かない。わからん!

変数凍結のしかたがわからない

Prologの技芸第二版を片手にPrologの勉強をしているのだけど、


P.197 で紹介されている

% occurs_in(Sub, Term) :- Sub は項 Term の部分項である.
occurs_in(X, Term) :-
	freeze(X, Xf), freeze(Term, Termf), subterm(Xf, Termf).

のプログラムが動かない。処理系はSWI-Prologをつかっている。
エラーを見たところ、freezeの挙動が、TAOP で紹介されているものと違うっぽい。


TAOP では、『freeze(X,Xf)は変数Xの凍結されたものXfを生成する』みたいなことを書いてあって、でも調べると今のfreezeはfutureみたいなことをやってるようで、TAOPの freezeに代わるものってあるんですかね……