昨日の記事「テスト付きクリーネ代数とその使い方」において、デクスター・コゥゼン（Dexter Kozen）のテスト付きクリーネ代数（Kleene Algebra with Test; KAT）は幾分使いにくい所があると書きました。それで、圏論的に書きなおそうと試してみました。やってみたら、なんか色々と面白いことがあるので書いておきます。
テスト付きクリーネ代数はメイヤー加群の特殊なモノのように思えます。それで、一般的なメイヤー加群に条件をつけて特殊化していって、テスト付きクリーネ代数を絞り出してみました。テスト付きクリーネ代数に至る中間で興味深い構造が出てきたりもします。それとは別に、舞台となる圏に比較的ゆるい条件を付けて、そこでテスト付きクリーネ代数を再現する方向もあります。
内容：
実例と計算方法
これから書くことは、実例を確認しながら、紙（ナプキンペーパーとか）の上で計算をしながら試したことです。が、それらを述べると量的に大変なので省略します。
ひとつだけ； 僕が使っていた例題。それは、次の2つのプログラムの同値性を厳密に示す、という問題です。
if (p)
if (q)
A
else
B
else
C
if (p and q)
A
elseif (p and not q)
B
elseif (not p)
C
[追記 date="2012-06-02"]例題コードの三番目の分岐が elseif (not q) となっていました。僕の意図からすると間違い（たぶん、書き落とした）なので、if (not p and not q) に直しました。not p and not q を not(p or q) にするとかは別な問題です。[/追記][さらに追記 date="2013-08-23"]2013/08/18 21:58の「通りすがり」さんの指摘「三番目の分岐は、意図からすると、elseif (not p) だったのではないですか？」で再び修正。[/さらに追記]
「厳密に」の度合いによりますが、なるべく厳密にと頑張ってやると、驚くほどたくさんの法則を使うことになります。「常識」とか「直感（or 直観）」とか言って、我々が暗黙に使っている法則がいかに多いかを再認識させられます。
計算はもっぱら絵算（pictorial/graphical/diagrammatic calculation）を使いました*1が、（そうしたいなら）等式的推論に書き換えることが出来ます。最初から等式的にやるのは僕には無理ですけどね。
ブール値が作用している圏
白紙からテスト付きクリーネ代数を組み立てる試みのがけっこう面白いので、先にこれを説明します。Bはブール代数 B = {{0, 1}, ∧, ∨, ¬} とします。否定（¬）を考えないときはブール半環と呼びます。Bの乗法モノイド {{0, 1}, ∧, 1} を B∧ と書くことにします。モノイド B∧ は、いわゆる一元体 F1 と同じモノです。
次のことは、定義を知っていれば出てくる事実です。
- 零対象を持つ圏では、ホムセットに自然な（自明な）B∧作用を入れられる。
- したがって、零対象を持つ圏は、B∧加群*2の圏で豊饒化されている（と考えてよい）。
- 圏が零対象を持ち、ホムセットにベキ等な足し算が定義されているなら、ホムセットに自然なB作用（半環作用）を入れられる。
- したがって、零対象を持ち、ベキ等可換モノイドの圏で豊饒化されている圏*3は、半環B上の加群の圏で豊饒化されている（と考えてよい）。
考えている圏Cが、対象としてB∧やBを含み、指数により自己豊饒化されている状況では次も成立します。
- Cが、モノイドB∧上の加群の圏で豊饒化されている事は、Cのすべての対象にB∧加群構造が入っている事と同じ。
- Cが、半環B上の加群の圏で豊饒化されている事は、Cのすべての対象にB加群構造が入っている事と同じ。
上記のような性質を持つ圏Cの具体例としては、点付き集合（pointed sets）の圏PtSet、関係の圏Relなどがあります。圏PtSetに足し算はないので、係数域はモノイドB∧ とします。圏Relはベキ等な足し算（関係の合併）があるので、係数域を半環Bと考えることができます。モノイドの演算も半環の演算（足し算と掛け算）も、全部ベキ等なことに注意してください。
今述べた状況というのは、要するにブール値（falseとtrue、あるいは0と1）が圏C全体に一様に作用している、ということです。Cの任意の射fに対して、左作用 0・f, 1・f と、右作用が f・0, f・1 が具合よく定義されているわけです。なお、これらのことは、End(1)が圏全体に作用することを利用しても出てきます。
関係圏から作る加群の圏
話を具体的にするために、圏Relを舞台として、BはRelの対象と考えます（正確には、Relをベースとする半環の圏の対象）。
まず注意事項：圏Relでは、集合の直積と直和が2つのモノイド積を与えますが、圏Relの直積は集合の直和となることに注意しくてださい。圏Relで考えた集合の直積は、圏の直積でも直和でもなく、指数を与えるようなテンソル積となります。このことは、次の記事を参照しくてください。
圏RelのホムセットにB作用を入れるのは簡単ですが、よりハッキリと、圏Relの任意の対象Aに対して、Bの左作用 αA:B×A→A があるとします。αA の具体的な定義は、Relの射を集合値写像と考えて次のとおり：
- a∈A に対して、αA(0, a) = {}
- a∈A に対して、αA(1, a) = {a}
Relには零射が存在するので、それを θA,B:A→B in Rel と書くことにすると：
- αA(0, -) = θA,A
- αA(1, -) = idA,A = ΔA
右作用もありますが、今は使いません。モノイド圏 (Rel, ×, 1) は、タプルの順序入れ替えσA,Bにより対称モノイド圏なので、左作用と右作用を交換するのは容易です。
上記の構成をすると、圏Relを半環B上の加群の圏とみなせます。
- (Rel as B-modules) = Module(Rel, B) where B∈|Semiring(Rel)|
半環B上の加群の圏とみなしたRelも、（混乱の恐れがなければ）同じ記号Relで表します。
クエリー射とテスト射
B加群の圏とみなしたRelのなかで、p:A→B×A という形の射が、コピーΔと破棄!（1への射）で余モノイドとみなしたBに関して余加群になっているとき、pをクエリー射と呼ぶことにします。ブール値を取るメイヤーのQueryに対応します*4。
B×A 上には、B左作用（左スカラー乗法）αA:B×A→A があるので、クエリー射pと左作用αAを結合して、p;αA:A→A が作れます。p~ := p;αA と置いて、p~ をクエリー射pに対応するテスト射と呼びましょう。テスト射はもちろん、テスト付きクリーネ代数のテストに対応します。
クエリー射p, q:A→B×A に対して、論理AND p∧q を定義できます（定義には、若干の注意が必要です）。(p∧q)~ = p~;q~ という等式を証明できます（これは自明ではない、絵算の使いどころ）。定義から、p~ はA上の自己射（endomorphism）なので、任意の f:A→B に対して、p~;f を作れます。これを p・f と書くと、先の等式は、(p∧q)・f = p・(q・f) というテスト付きクリーネ代数の公理を再現します。
僕の勘違いがないなら、テスト付きクリーネ代数で出来ることは、この枠組ですべて出来るはずです。特定の対象を固定する必要はなくて、圏全体でクエリー射やテスト射が使えるので、（対象を型とみなせば）型付き計算とも相性が良い方法になっています。
メイヤー加群との関係
メイヤー加群（メイヤーオートマトン）は、双モイドMと余モノイドVとを組み合わせたメイヤー代数(M, V)上の加群Aです。単なる対象とみなしたVも、モノイドとみなしたM上の加群構造を持ちます。よって、スカラー乗法（左作用として書く）は、a:M×A→A と a':M×V→V があります。
V = M' = (Mからモノイド構造を忘れたモノ) とすると、Mの左作用 a':M×M'→M' は、Mの乗法を使って定義できます。M'もa'もMがあればタダで作れるので、余モノイドVを別に与える必要はありません。このように、双モノイドMだけから、V = M' として作ったメイヤー加群を、簡約メイヤー加群（reduced Meyer module）とでも呼びましょう。
双モノイドMとして、ブール代数の論理ANDを乗法として、コピーΔと破棄!で余モノイド構造を入れたモノを取り、この双モノイドの上に簡約メイヤー加群を作ると、テスト付きクリーネ代数とほぼ同じ（まったく同じか？）構造ができます。これらのことから、テスト付きクリーネ代数はプリミティブな概念ではなくて、より基本的な下部構造の上に構成されるモノらしい、と感じるわけです。
