コゥゼン代数もっと - (保存用) 檜山正幸のキマイラ飼育記メモ編

これらの続き。

いやいやいや、コゥゼン代数やっぱり非常に便利だわ。コゥゼン代数（Kozen algebra）は僕の命名で、コゥゼン自身は termset algebraと呼んでいる。実は、termset algebra を少し変形している。

まず、(0, 1; ∪, ∩, +, -; ⊆) という指標を考える。指標だけではなくて、集合束でモデル化できる順序代数の公理を入れる。記号「-」は差集合で、足し算 x + y は x∩y = 0 のときだけ x∪y を意味する部分演算。その他は標準的な解釈。この指標と計算法則（公理）は、すべての集合束からなるモデル圏で特徴付けられるとする。今、計算法則を具体的には書き下さないけど。

σは、(0, 1; ∪, ∩, +, -; ⊆) の部分指標で、公理も必要なだけ選んだものだとする。実際に使うのは、(0; ∩, +; ⊆) とか。定数、演算は減らすがモデルは変えない。また、定数0と順序関係⊆を外すことはできないとする。よって、最小のσは (0; ⊆) となる。最小のσの場合は、最小元を持つ順序集合の公理しか残らないが、それでもモデルは集合束。等号は明示してないが、常に入っていて、(x⊆y ∧ y⊆x) ⇔ x = y だとする。

今までΣと書いてきたものをΠ（パイの大文字）にする。同じシグマでは紛らわしいのと、productのpからの連想。Πはランク付きアルファベットで、Π₀, Π₁, Π₂, ... のように直和分解される。直感的には、Π_kはk引数の関数記号の集合。特にΠ₀は定数記号の集合と解釈できる。

k≧1 に対しては、Π_kに属する記号はk項の擬積記号と呼ぶ。なぜに擬積かというと、積に似てるがちょっと違う演算だから。単調性（順序との協調性／一貫性）、分配法則、非退化性（零が吸収元）などは積と似ている。しかし、結合律、可換律、単位律（単位の存在）などはまったく成立しない（少なくともon-the-noseでは成立しない）。

法則に関して言うと：

[単調性]すべてのfに対して、x≦y ならば f(..., x, ...) ≦ f(..., y, ...)

これは、∪や+の分配法則に替えてもよい。

[分離性] f(x1, ..., xn) = g(y1, ..., ym) ならば、f=g （したがって、n = m）。かつ、すべてのiで xi = yi。

これは大事。エルブラン性と呼ぶのがよいと思う。

[非退化性] f(x, ..., x) = 0 ⇔ どれかのiでxi = 0。

これは0が、どんな擬積に対しても吸収元となっていること。

さらに強い条件を課すこともある、つうか、現実にはずっと強い条件が必要だが、代数系としてはこのくらいの定義でいいと思う。