日々の流転

λ. 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軍事動画まとめ：日本国」を参照。