たけをさん（id:bonotake）から随分と古いネタにトラックバックがありました。クリーネ代数とかテスト付きクリーネ代数とか -- 昔から話題にしているけど、今でも考えているネタですね。で、割と思いつくままにナニヤラ書いてみます。
[追記]ミスを直しました。修正箇所は取り消し線の所です。[/追記]
クリーネ代数ってイマイチ
クリーネ代数（Kleene algebra）やテスト付きクリーネ代数（kleene algebra with tests）は役に立つんだけど、「イマイチだなー」と以前から言っているわけです。その理由は、単一のクリーネ代数のなかだと「型」という概念がうまく扱えないのですよね。クリーネ代数を状態遷移のモデルと考えると、同じ状態空間内の状態遷移は定式化できるけど、異なる状態空間に飛び移る遷移は扱えません。
そんな理由で、クリーネ代数をポンと天下りに与えるアプローチは好きではなくて、圏論の枠内で、自然にクリーネ代数が出現するような方法がいいなー、と思っています。圏の構造から、集合論的な代数系を作り出すのときは、だいたい次のような手順になります。
- 圏に構造を与える。
- 圏の構造から、ホムセットに代数構造（や順序構造）を導入する。
- エンドセットに注目すると、より豊かな構造が入ることがある。
以下にクリーネ代数が圏からどのように出現するのかを概略示します。
圏から半環へ
クリーネ代数を自然に生み出す圏とはどのようなものでしょう。まず、半環（semiring）という代数構造を圏から定義してみます。
圏Cは次の構造を持つとします。
- 零対象を持つ。
- 双積を持つ。
順番に説明します。
零対象（zero object）とは、始対象であり終対象でもある対象です。始対象は0、終対象は1と書く習慣があるので、始対象が終対象でもあると、0 = 1 という奇妙な等式が成立することになります。とはいえ、基点付き集合（pointed set）やベクトル空間の圏には零対象があるので、そんなに珍しいわけでもありません。
記法の都合で、零対象は1と書くことにします。ゼロなのにイチとはこれいかに？ 0 = 1 だからドッチでもいいんです。任意の対象A, Bに対して、A→1 と 1→B が一意に存在するので、これらを結合して、θA,B:A→B という射が決まります。これを、AからBへの零射と呼びます。零射の存在により、ホムセットC(A, B)は基点付き集合の構造を持ちます。
直積と直和（余積）が一致するとき、それを双積（biproduct）と呼びます。特定された一意対応として (A, B)|→A×B と (A, B)|→(A + B) があるとき、A×B と A + B のあいだに標準的な同型がある、ということです。この標準的な同型により、A×B = A + B とみなすことができます。あるいは、A, Bに対して、直積でもあり直和でもある対象が一意的に定まっていると仮定してもいいです。以下では、双積を直積の記号「×」で表します。零対象1と双積×を持つ圏 (C, 1, ×)は、対象対称モノイド圏になります。
ΔA:A→A×A を直積に伴う対角、∇A:(A + A)→A を直和に伴う余対角とします。A×A = A + A だったので、∇:A×A→A と書いても同じですね。実は、∇は足し算を実現する射です。f, g:A→B に対して、Δ;(f×g);∇ が定義できますが、これが f + g です。このように定義された、ホムセットC(A, B)上の演算+は、実際「足し算」と呼ぶにふさわしいものです。
エンドセットC(A, A)では、圏の結合（composition）により掛け算を入れることができて、C(A, A)は半環（semiring）となります。圏Cの構造により、エンドセットに集合論的代数構造を入れることが出来たわけです。
上記の状況が起きている典型的な例は、関係圏Relと（適当なスカラー体上の）ベクトル空間の圏Vectです。関係圏の双積は集合の直和である点に注意してください。「Alloyの矢印記法と、モノイド閉圏としての関係圏」を参照。
ベキ等性と順序
Cは零対象と双積を持つ圏だとします。前節の議論から、任意の対象のエンドセットは半環構造を持つことになります。クリーネ代数の方向に近付けるために、もう少し条件を付け加えます。
対象Aに対する対角ΔAと余対角∇Aはこの順に結合できますから、次の等式は意味があります。
- ΔA;∇A = idA
idA×A = idA×idA なので、上記の等式（実際は同型だが）は、ΔA;(idA×idA);∇A = idA とか書けます。射の足し算の定義から、これは idA + idA = idA ですね。ラフな書き方をするなら、1 + 1 = 1 です。fを両辺に掛ける（結合する）と、f + f = f、そうです、足し算のベキ等性です。
零対象と双積を持つ圏が、Δ;∇ = id を満たすなら、エンドセットはベキ等半環（ISR; idempotent semiring）となります。ホムセットはベキ等な足し算（可換モノイド演算）を持つことになります。
ベキ等な足し算があると、f≦g ⇔ f + g = g と定義して関係≦を導入できます。≦が順序関係になることはすぐに確認できます。つまり、圏Cが零対象と双積を持ち、Δ;∇ = id を満たすなら、ホムセットは順序構造を持ちます。自動的に順序豊饒化されます。
トレースとクリーネスター
クリーネ代数では、「ベキ等な足し算」と「掛け算」（可換とは限らないし、ベキ等性も仮定しない）以外に「クリーネスター演算」が存在します。クリーネスターの圏論的対応物は何でしょうか？ それはトレースです。
圏Cが零対象（1と書く）と双積（×と書く）を持つなら、(C, ×, 1, σ)は対称モノイド圏となります。ここで、σは、2つの射影π1, π2を使って σA,B = <πA,B2, πA,B2>:A×B→B×A と定義される対称（置換操作）です。
対称モノイド圏におけるトレースについては、次の記事などで述べています。
モノイド積が双積で与えられるときは、f:A→A のクリーネスターf*を次のように定義できます。
- f+ =
Tr(Δ;f;∇)Tr(∇;f;Δ) - f* = idA + f+ = Δ;(idA×f+);∇
このf*はクリーネスターとして期待される性質を持っています。f*は等式的（equational）に定義されています。伝統的なクリーネスター、クリーネ代数は不等式（順序）を使って定義されるので、これはコンウェイスター（Conway star）と呼んだほうがいいのかも知れません。等式と不等式の差がどの程度のものか、僕はハッキリとは把握してません。
トレースが、再帰、繰り返し、不動点、結び目などと関係することは次の記事で言及しています。
Testsはどうなるのか
テスト付きクリーネ代数のテストとは、論理式、条件、命題、真偽値などと同じ意味です。なんらかの論理計算の体系です。テストの代数としては、通常はブール代数を仮定します。しかし、もっとゆるくハイティング代数がふさわしいときもあるでしょう。
テストの代数を外側の圏から導くのはけっこう難しい気がします。エンドセットのなかで乗法的にベキ等（f;f = f）な射をテストとする案がありますが、これだけだと乗法の可換性が出てこないでしょう。エンドセットの順序を使って、p≦id である自己射pをテストと考えることもできます、これは割と良さそうです。
圏の対象Aごとに最初からテストの代数を付けてしまう、という方法もあります。ブール代数やハイティング代数の圏から出発して、それを係数とする多元環や両側多元環を考えるアプローチもあるかも知れません。テストを位相空間の開集合とみなすとか、トポスの部分対象分類子とみなすとか、そんなんもアリそうです。
テスト付きクリーネ代数とは、論理の代数とプログラムの代数を一緒に考えることなので、多様な定式化があるし、何が最適かの判断は難しいですね。他に、行列計算や半環圏との関係なんてのも面白そう。ですが、今日はこのへんで。
