「クリーニ代数と圏論」の続きっぽい話。昨日よりさらに思いつくまま。
トレース付き圏とクリーネ代数
復習： 零対象と双積を持っていて、ベキ等律 Δ;∇ = id が成立し、双積に関してトレースを持つ圏Cがあれば、各エンドセットC(A, A)にクリーネ代数の構造を入れることができます。今言った条件を満たす圏になにか名前があればいいのですが、合意された名前はないようです。「クリーネ圏」という言葉はあるのですが、この条件とは違う、つうか人によって違った意味で使っていたりして安定した用語法じゃないみたい。
「圏全体の構造→エンドセットの代数構造」の逆向きも言えます。つまり、エンドセットの代数構造から圏の構造を構成することができます。次のように仮定します：
C = (C, ×, 1, σ) が双積をモノイド積とする対称モノイド圏だとします。各エンドセットがクリーネ代数になっているとします。さらに、エンドセットの半環構造は外側の圏Cから自然に導入されるものと一致しているとします。なので、追加の構造はクリーネスターです。定義が完全に等式的であり、ベキ等律 Δ;∇ = id も要求してないので、クリーネスターよりコンウェイスターと呼ぶほうがいいかも知れないですが。
このセッティングで、クリーネスター（コンウェイスター）から圏論的不動点演算子（コンウェイダガー）を作ることができます。f:A×X→X に f†:A→X を対応させる演算が不動点演算子＝コンウェイダガーですね。カザネスク／ステファネスク／ハイランド／長谷川の定理により、直積に対する不動点演算子からトレースを定義できるので、「エンドセットのスター演算→圏全体のトレース」という構成ができるのです。
ここらの事は、昨日も引用した次の記事にだいたいは書いてあります。
テストの代数は絞り出せない？
前節で仮定したような圏 (C, ×, 1, σ) からテストの代数をうまく抜き出すのはけっこう難しいと思います。対象Aに対するエンドセット C(A, A) は半環なので、このなかでブール代数（またはハイティング代数）になっているような部分半環を取り出せばいいのですが、そのためには色々と条件を付けます。この条件が、どうもご都合主義的な気がするのです。
人為的な条件を付けないで、“自然に”テストの代数（ブール代数またはハイティング代数）が出てくるには、外の圏 (C, ×, 1, σ) の構造が弱すぎるんじゃないかと思っています。双積以外に、もう一つのモノイド積が必要なんじゃないかと。
関係圏もベクトル空間の圏も、双積とは別なテンソル積を持っています。双積とテンソル積の2つのモノイド積を持ち、ひょっとするとトレースも2つあるような圏が必要なのかも知れません。
よくわからんけど。
テストの代数を天下りにくっ付ける
「よくわからんけど」じゃショーガナイので、テストの代数を絞り出すのはあきらめて、テストを天下りに与えることにします。
圏の対象Aごとに、A上の「テストの代数」P(A)が割り当てられているとします。対象が集合で、P(A)は集合Aの「ベキ集合のブール代数」と思うと理解しやすいかも。ブール代数より弱い構造でもいいけど、P(A)が可換半環であることは仮定します。P(A)は論理計算の場なので、足し算を∨、掛け算を∧で書くことにします。
対象A, Bごとに三項演算 P(A)×C(A, B)×P(B)→C(A, B) があるとします。p∈P(A), f∈C(A, B), q∈P(B) に対して、三項演算の結果は p・f・q と書きます。そのインフォーマルな意味は、プログラムfに対して、事前条件pと事後条件qを付加したものが p・f・q ということです。
P(A)には足し算の単位（falseに相当）と掛け算の単位（trueに相当が）があるので、それは 0, 1 と書くことにします。p・f・1 を単に p・f と書き、1・f・q も単に f・q と略記することにします。(p∧q)・f = p・(q・f) とか、1・f = f とか、これらを三項にしたものとか、そういう等式は仮定するとします。要するに、テスト付きクリーネ代数を作るための等式は最初から公理にしてしまう、ということです。
ドットで表した演算をガードと呼ぶことにします。p・f ならpによるプレガード、f・q はqによるポストガードです。p・f・q は両側をガードしていることになります。これは、実行文fに対するホーア式 p{f}q と似たようなものです。
ガード演算は圏の結合（composition）と整合する必要があるので、次の条件も仮定します。
- (f・q);g = f;(q・g)
- (f・q);(r・g) = (f・(q∧r));g
これらを組み合わせると、(f・q);(r・g) = f;((q∧r)・g) も出ます。順次実行「;」、論理AND「∧」、ガード「・」が、ある程度は置き換え可能であることを示しています。論理OR「∨」と足し算「+」は、非決定性の分岐を表します。クリーネスターは任意回の繰り返しです。
ドメイン付きクリーネ代数との関係に触れておくと、p・f = f が成立するときpはfのドメインで、f・q = f ならqはfのコドメインです。圏論の域／余域と紛らわしいですが、今出したドメイン／コドメインは域／余域とは別物です。ドメイン＝余像、コドメイン＝像 とか呼ぶといいかも。
型を使いたい
まーともかく、テストの代数とガード演算が、ある程度は「テスト付きクリーネ代数の大域的な定義」になっていそうです。大域的と言っているのは、単一の代数ではなくて、圏全体の構造としての定式化という意味です。外側に圏があるということは、たくさんの対象を一緒に考えることであり、対象を型とみなして型概念を導入できることです。
単一のクリーネ代数やテスト付きクリーネ代数の不満は、複数の型が使えないことなので、圏全体の構造として再定式化してみたわけです。もちろん、特定の対象に注目すればもとの定義が再現することは必要です。もっと細部を詰めないといけませんね。
テストの代数を天下りに与える方式はどうもスッキリしないのですが、外の圏がもっと豊かな構造を持つなら、テストの代数も自然に出現するだろう、と期待もしてます。
