関手と自然変換：コゥゼンの記号法

デクスター・コゥゼン（Dexter Kozen）は、クリーネ代数の研究者として有名ですが、その他の分野でも面白いアイディアを色々導入している計算科学者です。

コォゼンは、明らかに圏論が使えそうな状況でも（わざと？）使ってなかったりするので、圏論嫌いなのかなと思っていました。が、圏論に関する論文も書いています。コォゼンの計算法は、グロービュラー図やストリング図を駆使する絵算派とは対極的で、テキスト記号で頑張るやり方です。そのコォゼンが、関手と自然変換の計算をベクトル空間のスカラー乗法に例えていました； 紹介します。

F, Gなどを関手、α, βなどを自然変換として、関手の反図式順結合を「・」で表します。関手Fと自然変換αの結合を次のように定義します。

• (α・F)_X := α_F(X)

「・」の左右を入れ替えると定義が変わります。

• (F・α)_X := F(α_X)

記号「・」を次の3つの意味でオーバーロードしている点に注意してください。

1. 関手の結合
2. 関手が右から作用する、関手と自然変換の結合
3. 関手が左から作用する、関手と自然変換の結合

オーバーロードされた記号「・」を一種の乗法とみなすと、結合律が成立します。

1. (α・G)・F = α・(G・F)
2. G・(F・α) = (G・F)・α

ここで、一時的な記号法として、自然変換の縦結合（vertical composition）を「+」で表します。念のため定義を書いておくと：

• (β + α)_X := β_X・α_X （「・」は関手の結合）

さて、この記号法で次の“分配律”が成立します。（縦結合に「+」はさすがにひどいので、実際には白丸記号を使っていますが。）

1. (α + β)・F = α・F + β・F
2. G・(α + β) = G・α + G・β

要するに、「関手をスカラー、自然変換をベクトル」とみなして、スカラー乗法の性質が成立するというわけです。ただし、スカラーの足し算は存在しません。掛け算だけがあるスカラーなので、モノイドの線形作用に似てるといったほうがより適切かもしれません。

絵算派の僕としては、以上のことは、2-圏や二重圏の交替律（interchange law）をグロービュラー図／タイル図に描けば明らかな事実なので「そりゃそうだろう」とも思うのですが、「ベクトル空間のスカラー乗法に似てる」とおぼえておくのは悪くはないですね。