日々の流転

λ. 久しぶりに清々しい朝。

λ. 昼飯

藤沢のサボテンで友人と。

λ. Hilbert ワークショップ

に行くのをすっかり忘れてた。うぐぅ。

λ. sonotenoメーリングリスト

そういえばsonotenoメーリングリストに少し前にsubscribeしたのだ。「その手の」ことの話題を流すためのものらしい。

λ. [RAA:CPL]

とりあえず公開してみたり。型推論の部分とその周辺が酷いことになっているし、きっとバグもまだありますが、それなりには遊べます。

λ. 借りた本

『二つの約束　下』

ダニエル・スティール (Danielle Steel) [著], 天馬 龍行 [訳]

λ. FOAF Walker

山けんさんという方の作った FOAF Walker というツールで自分や他人のFOAFファイルを眺めて遊んでみる。FOAF Walker はちょっと癖があるけど、なかなか楽しいツールだと思う。

自分を中心とする100ノードほどを表示してみると、自分の周りが疎なのがちょっと面白くない。みんなFOAFしようよ〜 (笑)

λ. Guarded Induction on Final Coalgebras. Duško Pavlović

guarded (co)induction に対して圏論的なモデルを構成しているのだが……結構複雑だな。もっとシンプルなものを期待していたので驚いた。これはこれで興味深いけど、とりあえず深入りしないことにしよう。

それと、興味深く思ったのは、以下のような視点というか考え方。

In fact, the most interesting conceptual distinctions often begin to surface only when the symmetry starts breaking down. Going back to monads and comonads, recall, e.g., how the free algebras for a monad form an algebra classifier (the clone), whereas the cofree coalgebras for a comonad do not seem to either classify or “coclassify” anything meaningful. And indeed, the former turns out to be the foundation of a rich mathematical theory, capturing algebraic varieties by functorial semantics, whereas the latter remains a symptom of the fundamental fact that this theory does not have a dual: coalgebras for comonads on toposes tend to form toposes again, rather than “covarieties”.

私も含めて圏論ユーザは双対性を圏論を強力な武器と認識していて、双対性が利いてくるような状況には興味を示すけど、双対性が役に立たないような状況には比較的興味を示さないことが多いです。でも、そういう状況でこそ見えてくる興味深い点というのもあるんだなぁ。反省、反省。

• <URL:http://www.kestrel.edu/home/people/pavlovic/coalgebra.html>
• <URL:http://dx.doi.org/10.1016/S1571-0661(04)00056-8>
• citeseer:pavlovic98guarded.html

分からなかった点など

• p.3 で　tree induction, stream induction, labelled tree induction と呼んでいるのは何を指している?　inductionという言葉をどういう意味で使っているのか正確な定義が知りたい。
• p.7 の F=P_Σ のときの、prefixing operations が変な気がする。Σの部分集合の個数だけあるのでは?
• p.6 の 「But !: γ is surely an epi, because it is split by fix (be it unique or not). So ∂ induces a unique prefix η1, and η1 induces a unix fixpoint fix.」という部分が良く分からない。epiだと何故uniqueに?

λ. (ttweb) agdaを使ってみる

メモ。置換公理から分出公理を証明したり等。

λ. iKnow!の「旅を楽しもう！（レストラン＆ホテル）」を完了

iKnow!で2008-12-19に始めたコース「旅を楽しもう！（レストラン＆ホテル）」が終わった。

次は「旅をもっと楽しもう！（観光＆買い物）」をやろうと思っていたけど、新年キャンペーンで「iKnow!でGabaマンツーマン英会話を体験してみよう」というのをやっているようなので、そっちをやることにする。 Gaba特製フレーズブック抽選プレゼントというのもあるみたいだし。