2008-12-31 [長年日記]
λ. 「クリーニ代数入門」 by 古澤 仁 and 高井 利憲
二年前からの積読消化。 ちょっと前 に Topology via Logic の12章 Spectra of rings を読み返して、そこでquantaleに関係して「Conway [71] defines the notion of “standard Kleene algebra”, which is essentially the same as a quantale」と書かれていて、そういえばと思って読み始めたもの。 クリーニ代数に関しては「正規表現を公理化した代数らしい」というくらいの知識しか無かったんだけど、これは応用も沢山あり面白い。
ちょっとビックリしたのは、min-plus代数とトロピカル代数が同じもので、これがクリーニ代数の一例であること。 min-plus代数についてはPPL2008での発表 Modal μ-calculus on min-plus algebra N∞ で聞いていたし、トロピカル代数については檜山さんが時々日記に書いていた*1のを読んでいた。 どちらもちゃんと理解出来てはいない話だったのだけど、繋がってたのね……
min-plus代数を使って最短経路問題を解く話は面白かったので、自分でも試しに書いてみた。KleeneAlgebras.hs
また、自由代数に関しては、代数のクラスCが等式またはホーン節で定義される場合には集合からの自由生成が可能という話は、等式以外から自由生成することなんて考えたことが無かったので、「へぇ」と思った。
あと、KAT-MLという対話的定理証明器があるそうなので、遊んでみたい。