日々の流転

λ. 筋肉痛。

λ. 今日の逃避 with finite-set.rb

原さんにfinite-set.rbを教えてもらったので、それを使ってちょっと逃避。

でも、ダサいなぁ、これ。あと、epimorphicかつmonomorphicなだけじゃisomorphicの十分条件じゃないんだっけ? 射が写像ならこれで十分だったと思うけど……

CPL(Categorical Programming Language)は遠い……

λ. Savile Row

「背広」って"Savile Row"から来ているらしい。ホントかしら。

λ. 圏論

initial object, terminal object, product, sum の定義。

λ. スケート

ヤグディンすげー

λ. イラク攻撃

やっぱフランスとロシアの利権をある程度保証してでも国連決議を通したほうが良かったんでないですかね? それから、日本の米国支持の行動は、本当に日本の国益にかなうのか私にはよくわからんので何とも言えないのですが、「対イラク・米大統領最後通告　ブッシュ大統領の演説」みたいな演説を見ると、やっぱムッとしてしまう。

λ. 携帯電話

「sakai-mobile@tom.(以下略)」で私の携帯に転送されるのでよろしく。> 某方面

λ. algebraic datatype を宣言するキーワード

「type」よりは「data」か「datatype」の方がいいな……と思うのは私がHaskellユーザだから?

λ. 夕食

池上さんと湘南台のソンブンでタイ料理。いやー、楽しかったです。Rubyの事だけでなく数学の事や研究の事や、他にも色々話してきました。

λ. Wrap GObjects in Python

草野さんの日誌(2003-03-18)より

λ. 週末

明日と明後日は IP unreachable な予定。探さないで下さい(笑)。

λ. Linear Logic complements Classical Logic - Vaughan Pratt

だいぶ前にどこかのメーリングリスト*1で、「古典論理と線形論理は共に二重否定をキャンセル出来るという特徴を持っていて、ある意味で双対になっている*2」という話を見かけたのをふと思い出して検索してみた。結局そのメールは見つからず、この論文が見つかった。

内容は興味深いのだけど、たとえが多くて、僕にはいまいち良くわからない。

へぇ(3)。順序数を対象、順序数を集合としてみたときの関数を射とするような圏は、普通の集合の圏と同値なのか。これは、選択公理を仮定すれば von Neumann cardinal assignment を使って言えるのかな?

それから、CABA (complete atomic boolean algebra) というのがあって、その圏は集合の圏の双対圏になっているというのも初めて知った。completeってのはmeetとjoinが(有限集合に限らず)任意の部分集合に対して定義されてるって意味だろうけど、atomic ってのはどういうことを意味してるのだろう?

http://plato.stanford.edu/entries/boolalg-math/ によると、アトムとは false*3 ＜ x ＜ a を満たすような x が存在しない a のこと。ブール代数が atomic であるのは、任意のxについて、false ＜ x ならば、あるアトム a が存在して a ≦ x を満たすということ。なるほど、なるほど。でも、この定義は代数的でないので、CABA homomorphism が満たすべき性質が良くわからないな。アトムであることを保存するとかそんな感じか。 まあいいや。細かいところはおいておくとして、反変冪集合関手 Pow: Set^op→CABA と hom_CABA(-,2): CABA^op→Set によって、CABAとSet^opは圏同値になってるんだろう。きっと。

【2006-02-08 追記】 檜山さんが「反対圏の実現」というエントリで Set と AtomfulLat が反変圏同値ということを示していたのを見て、もう一度考え直したところ、上記は CABA homomorphism の条件以外は正しかった。CABA homomorphism は単にCABAの間の complete boolean algebra homomorphism で良いみたい。すると、CABA に「アトムが十分ある」ことと、CABA homomorphism が「アトム被覆性」を満たすことは証明でき、つまり CABA ならば AtomfulLat であることが言える。あとは檜山さんのと本質的に同じ構成になる。本質的に同じといっても、檜山さんの説明が代数を前面に出した説明だったのに対して、私は頭の中では(Locale と Frame の双対性を念頭に置いて)空間的なイメージで考えていたので、個人的な印象はちょっと違うけど。

…とりあえず、あとでちゃんと計算しよう。

関連リンク

• http://d.hatena.ne.jp/bonotake/20060208/1139373344

λ. 自衛隊動画

カッコ良すぎ。すばらしい。STAR.GAZER.1208. (2005-03-18) と ひろぶろ より。

【2006-06-14追記】 このリンク先は消えてしまったが、以下で見れるようだ。

• http://www.geocities.jp/isharejp/Japan_self_defense_force.html
• http://www.geocities.jp/isharejp/Japan_self_defense_force1.html

【2006-11-27追記】 YouTubeには他のバージョンも色々あった。 「YouTube軍事動画まとめ：日本国」を参照。

λ. エネミーライン

を観た。

λ. バンディッツ

を観た。

λ. ゴッドファーザー PART III

を観た。

λ. 「Haskell の call/cc 重大な設計ミスか！？」

PPL2007の「合成モナドのためのcall/ccに対する改善の提案」(米澤拓央 (筑波大学))って、どういう話だったのだろうか。ちょっと気になる。

λ. 飲み会

店員さんの裾が高めの浴衣と素足に萌え。

λ. 書き換え系について少し勉強 (「潜在帰納法と書き換え帰納法の比較」 by 小池広高 and 外山芳人)

私はどうも項書き換え系の話についてよく分かっていなくて、こないだも随分的外れなことを言ってしまった気がするので、ちょっと勉強してみようと思った。 何か短い入門的なテキストがあると良いのだけど、とりあえず手元にあった「潜在帰納法と書き換え帰納法の比較」(by 小池広高 and 外山芳人)というのを読んでみる。 以下は単なる感想で、内容の解説はない。

帰納的定理

まず、項書き換えシステムでは、帰納的定理とは任意の基底頂上で成立する等式のことを「帰納的定理」と呼ぶ。 さらっと片付けられているが、ここで少し悩んでしまった。

最初にちょっと悩んだのは、何で単に「定理」ではなくわざわざ「帰納的定理」と呼ぶのか。 任意の基底項上で成立するということはつまり始モデル(initial model)で成り立つということだけど、始モデルで成り立つ等式であっても新たな要素(junk)が加わったモデルでは成り立たない可能性があるので、帰納的定理は普通の意味での定理になっているとは限らないからか。

それから、次に悩んだのは何故「帰納的」という言葉を使うか。 ググってみると、始モデルにおける定理だからという話と、証明に一般に項の構造に関する帰納法が必要となるからという説明があるようだ。 両者は表裏の関係といっても良いので、これも納得。

潜在帰納法と書き換え帰納法

「潜在帰納法」は名前からして隠蔽代数(hidden algebra)における帰納法みたいなものだと勝手に思いこんでいたが、そうではなかった。

潜在帰納法(inductionless induction)も書き換え帰納法(rewriting induction)も、いずれも証明したい等式を追加した書き換え系が、(始モデルにおいて)元の書き換え系と同等であることを示すことによって、証明したい等式が元の書き換え系における帰納的定理であることを示す方法。

とりあえず、定義を確認して証明を一通り追いかける。 項書き換え系に詳しくないので結果については「へー」と思うだけなのだが、項書き換え系ではではこういう議論の仕方をするのね。面白い。

退行

弱正規化性、強正規化性、合流性は馴染み深い概念だけど、退行(Retrogresse)についてはまだイメージがわかないなぁ。