日々の流転

λ. 人類が滅びるとしたら(滅びるに決まってるけど)、それは理性故にだろう。…とか最近よく思う。

λ. Gyve

そういえば、Gyveって最近どうなってるんだろう?　今度試してみたいところだ。

λ. conservative

もちろん、僕は保守的な人間ですよ。ええ、保守的ですとも。

λ. エージェント指向

各オブジェクトにスレッドを内蔵して、勝手にほげほげ〜　という程度なら、スレッドを扱えるオブジェクト指向言語のユーザなら、誰でも一度くらいは試したことがあるんじゃないかと思う。でも、エージェント指向ってその程度のモノじゃないでしょ?　最近あんまし話題を聞かないけどさ。

λ. ぎゃーっす

ラッセルの「西洋哲学史」読みてー

λ. Gimp-Ruby

アイコンをRubyちゃんにしようかな。

λ. 瀬名秀明の博物館

瀬名秀明のウェブサイトがあるって初めて知った。

λ. 呑み

というわけで、いつものメンバーで飲み会。つうか、あれは酔ったうちに入らないと思われ。

λ. MIB見た。今度は2を映画館に見に行こう。

λ. ITスキル標準人材育成研修　

というのがあって丸の内で日立の人と一緒に研修などするわけですが、今日がその一日目。僕がとっているのはデータベースコースというやつで、今日はSQLや正規化とかについて簡単な復習。

昼食を講師の吉田先生におごってもらった。感謝。

17時で終了。その後、豊田さんと横浜の紅雲餃子房でご飯を食べて、本屋とゲーセンで時間をつぶす。やっぱジョイスティックは難しい。パッドならあんな負け方は絶対に……

λ. Ruby 1.8.0 リリース!

リリースおめでとうございます。いやー、めでたい。

λ. 研究会

清木研にはかわいい娘が多いと吉本さんに聞いて、来期は清木研に行こうかと心が揺れております。

λ. "Inductive, coinductive, and pointed types", Brian T. Howard

を読んだ。"Algebraically Bounded"とか、ちと良く知らない概念が出てきたので後で調べよう。

• http://www.cis.ksu.edu/~bhoward/ONR/papers.html

【2006-09-21追記】 algebraically bounded について、この論文では「inductive and coindutive types are canonically isomorphic」とちゃんと書いてあった。ってか以前に一回確認してるはずだが、今また確認しているのは何故だろうorz

λ. rubyとかgtkとかgnomeとかっぽい集まり

に行ってきた。むとうさん、須藤さん、kitajさん、かくたにさん、ashieさん、zoeさんの面々ににお会いした。 みんな色々な意味で凄杉だった。

• よたらぼ(2006-08-04)
• 帰ってきた今日のなんでやねん(2006-08-06)

λ. アルゴリズム勉強会(第一回)

• 資料
• アルゴリズム勉強会2006 (access limited)

λ. 関数型プログラミングの世界へようこそ (本物のプログラマはHaskellを使う　第1回)

「カンバン方式」を例として出しているのが、shelarcyさんっぽい。

λ. Lightweight Language Spirit

講演や発表それ自体も面白かったが、それ以上に色々な人とお会いすることが出来たのが楽しかった。 そういう意味では休憩時間が長めにとってたったのが非常に良かったと思う。

久しぶりにお会いしたsyd_sydさんの紹介で、OCaml-Nagoyaの小笠原啓さん、今井宜洋さんにお会いした。 浜地さんはRHG読書会で見かけたことはあったけど、マトモに話すのは初めて。 “Lambda the Ultimate” T-シャツ が目立っていた 日記を書く[・ _ゝ・]はやみずさん にもお会いした(Lambda the Ultimate の関係者かと思ったw)。 他にも色々な人にお会い出来た。 野中さんにも久しぶりにお会いしたかったけど、お会いできず残念。それから、sshiさんやTheoriaさんのような方にもお会いしたかったなぁ。

基調講演

和田先生の基調講演。 そういえば、生の和田先生を見るのは初めてだ。

「denotational semantics で書いてあるけど動く Scheme」がどういう意味なのかちょっと困惑したのだけど、多分「基本的な意味領域とその領域に対する基本的な操作をまず実装し、処理系全体を統語領域から意味領域への(帰納的に定義される)関数の形で記述した」というだけなのだと思う。 昼休みのときに「再帰はどうるんだろう?」みたいな話もあったけど、不動点をとる部分も基本的な操作として実装されているのだろう。

Language Update

弾さんの発表 で「Perl6はとりあえずポロロッカ星人のみなさんにまかせて」とあったが、元ネタがわからず悔しかった。ポロロッカといったら、これしか思い浮かばんかったよ。

正規表現のtrieを用いた最適化の話は「これまでやってなかったんかい」と思った。しかし、それにしても、Perlは相変わらずキモイなぁ(笑

Rubyは「ありゃ、いつのまにこんな計画になったんだっけ!?　これ今年中に全部やるなんて正気か?」と思ったら、案の定なオチ。笑った。

shinhさんの発表していたIoは、BNFが5行*1で「おぉー」と思った。 それから、引数があるときだけ実行が遅延されるとか、その邪悪さっぷりが素敵。

昼休み

久しぶりにお会いした上野さんに、SML#のことを色々と教えてもらっていた。 私はSML#のランク1多相について誤解していた。 それとデータ表現とインタオペラビリティの話。 あと、「重要なのはsyntaxではなくsemanticsと実装技術。でもそれだけじゃなかなか使ってもらえない」という話でハードウェア記述言語のBlueSpecを連想。 BlueSpecの文法は元々は拡張Haskellだった(参考: Bluespec -- Designer's Perspective)のをマーケティングの観点から拡張Verilogだか拡張SystemCだかに変えたが、SML#の文法はMLであり続けるのだろうか。

普通にお昼を食べていたら、次の「オレ様言語の作りかた」には遅刻してしまい、少し残念。

飲み会

何か良くわからない集まりだ(笑　ここでも色々な人にお会いできて楽しかった。

某氏が線形論理の入門に良い文献を探していたが、照井先生の「線形論理の誕生」等はどうだろうか。

λ. cwaでのユニット型の解釈

Categories with attributes (cwa) で cwa の簡単な説明を書いたので、今度は cwa で幾つかの基本的な型を扱ってみることに。 まずは一番簡単と思われるユニット型を。

構成規則と導入規則

通常扱う構成規則と導入規則は以下のような形になっている。

---------------
Γ ├ Unit set
Γ ├ () : Unit

これだと任意のΓについて考えなければならず面倒くさいが、実際のところはそれらの解釈はΓが空である場合からweakeningによって得たものと等しくなければならないので、Γを空の場合に限定した以下の規則を考えることにする。

--------------
├ Unit set
├ () : Unit

これはそれぞれ Unit ∈ Fam(1) と () ∈ Tm(1, Unit) で解釈される。 Γが空でない場合は、weakening -[!_Γ] を使って Unit[!_Γ]∈Fam(Γ) と ()[!_Γ]∈Tm(Γ, Unit[!_Γ]) で解釈できる。

除去規則

お次は除去規則で、通常の除去規則はこんな形をしている。

Γ, x : Unit ├ P set
Γ ├ M : P[x:=()]
Γ ├ N : Unit
--------------------------------
Γ ├ elim(P,M,N) : P[x:=N]
Γ ├ elim(P,M,())=M : P[x:=()]

ただ、これも少し扱いにくいので、少し変えて、以下のような規則を考える。

Γ, x : Unit ├ P[x] set
Γ ├ M : P[()]
---------------------------------------------
Γ, x : Unit ├ elim(P,M)[x] : P[x]
Γ ├ elim(P,M0)[()] = M : P[()]

これの解釈は、 任意の P ∈ Fam(Γ・Unit[!_Γ]) と M ∈ Tm(Γ, P[()[!_Γ]]) に対して、 elim(C,M) ∈ Tm(Γ・Unit[!_Γ], P) が存在し、 elim(C,M)[()[!_Γ]] = M ∈ Tm(Γ, P[()[!_Γ]]) が成り立つということになる。 図で書くと以下のような感じになる。

λ. 江ノ島花火大会

エンドレスエイトで延々と「夏は夏らしく夏じみたことを」と言っているのを見て、なんとなく夏っぽいことをしようと思ったりして、なんとなく花火を見に行くなどしてみた。 といっても、人ごみの中には行きたくなかったので、遠くからだけど。しかし、花火の写真を撮るのは難しいな。

hanabi.mp4