アローの3文字演算子と対角付きプレモノイド圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)

アロー（Arrows; http://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf）は、2000年前後にヒューズ（John Hughes）によって導入されたプログラミング手法／計算モデルです。これって面白いような、面白くないような？僕にとってアローは微妙な概念なんですが、それはともかく、アトキー（Robert Atkey）の "What is a Categorical Model of Arrows?" によれば、アローはフレイド圏やその変種と同等なようです。

アローやその拡張では、アスキー文字を3つ続けた中置演算子が使われます。>>>、***、&&& です。これらの演算子の意味を考えてみたら、アトキーの言うフレイド圏では不足があります。対角（diagonals）という構造を入れないと、うまく説明できません。

内容：

フレイド圏
対角構造
対角付きフレイド圏と対角順次積

フレイド圏

フレイド圏と、そのもとになるバイノイド圏、プレモノイド圏については、「非交替的な積を持つ圏達」で説明しています。簡単に復習すると： CとKが圏で、J:C→K が関手のとき、(C, K, J) がフレイド圏（Freyd category）であるとは次のことです。

Cはデカルト・モノイド圏である。
Kはプレモノイド圏である。
|C| = |K| で、Jはidentity-on-objects関手である（対象Xについて J(X) = X）。
関手Jは、厳密プレモノイド関手である。

「非交替的な積を持つ圏達」では、次のような記号で各種の積を表しました； ×、`×、×'、|×、×|。これらに対して、アスキー文字2文字または3文字の代替表現を定義しておきます。

もとの記法	アスキー記法	意味
×	**	バイノイド圏の対象に対する積
`×	\|*	バイノイド圏の左バイノイド積
×'	*\|	バイノイド圏の右バイノイド積
\|×	\|**	バイノイド圏の左順次積
×\|	**\|	バイノイド圏の右順次積

プレモノイド圏はバイノイド圏に構造と条件を足したものなので、プレモノイド圏でも同じ記法を使います。アローの記号「>>>」は、プレモノイド圏の図式順結合のことです。フレイド圏 (C, K, J) において、Kの結合と積には、今定義したアスキー文字2,3文字の演算子記号を使うことにします。

「非交替的な積を持つ圏達」より簡略化して、(|*):K×|K|→K、(*|):|K|×K→K、(**):|K|×|K|→|K| とします。f:A→B, g:C→D in K として次が成立します。

A *| id_B = id_A |* B = A ** B
f |** g = (f |* C)>>>(B *| g) （左順次積の定義）
f **| g = (A *| g)>>>(f |* D) （右順次積の定義）

「|*」と「*|」では、縦棒があるほうに一般の射、アスタリスクのほうに対象が置かれます。ちなみに、TeXでは、\ltimes（左縦棒）と \rtimes（右縦棒）です。記号の使用例は http://ncatlab.org/nlab/show/premonoidal+category とか。

アローの書き方だと、次のようになります。

first(f) := f |* C
second(g) := A *| g
f *** g := f |** g

通常、プレモノイド圏Kには対称σの存在も仮定するので、secondは不要です（firstとσから定義可能）。同様に、|** とσを組合せて **| を定義できます。

対角構造

フレイド圏 (C, K, J) で解釈すると、アローの記号「>>>」はKの結合、「***」はKの（左）順次積だということが分かりました。それでは「&&&」はどう解釈されるのでしょうか。Kが対称プレモノイド圏というだけでは、うまく解釈できません。

Kに対角構造を入れましょう。対角は誰が言い出した概念か分かりませんが、セリンガーの次の論文には対角の定義が載っています。

Title: Categorical Structure of Asynchrony
Author: Peter Selinger
URL: http://www.mathstat.dal.ca/~selinger/papers/catasynch.pdf

セリンガーの対角は対称モノイド圏に対して定義されていますが、対称プレモノイド圏でも問題はなさそうです。

K = (K, `×, ×', ×, I, α, λ, ρ, σ) が対称プレモノイド圏だとします。α, λ, ρ は結合律、左右の単位律の構造同型射、σは対称同型射です。K上の対角構造は、|K|でインデックスされた射の族 Δ_A, ◇_Aで、次のような条件を満たすものです。

Δ_A:A→A×A
◇_A:A→I
(A, Δ_A, ◇_A) は、K内で（Aを台とする）対称コモノイド（余可換余モノイド）となる。

さらに、次の一貫性条件も仮定します。（以下は可換図式を推論図風に書いたもので、上段と下段が同じ射になります。）

   ◇_I:I→I
  ------------[ = ]
   id_I:I→I


   ◇_A×◇_B:A×B→I×I  I
  -------------------------[ = ]
   ◇_A×B:A×B→I


   △_A×△_B:A×B→(A×A)×(B×B)  (A×B)×(A×B)
  ----------------------------------------------[ = ]
   △_A×B:(A×B)→(A×B)×(A×B)

(A×A)×(B×B) $\stackrel{\sim}{=}$ (A×B)×(A×B) という同型を作るとき、対称σ_A,Bが必要になります。

Δ_A, ◇_Aが自然変換であることは要求しません。Δ_AをAの対角射（diagonal morphism）、◇_AをAの弱終射（weak terminal morphism）と呼びます。Iはプレモノイド積の単位ですが、終対称とは限りません。AからIへの射は、◇_A以外にイッパイあるかもしれません。

対角構造を持つプレモノイド圏を、対角付きプレモノイド圏（premonoidal category with diagonals）と呼びます。

セリンガーは、対角付き圏Kがトレースを持つ場合に、単位Iとトレースから弱始射（weak initial morphism）□_A = Tr_A(Δ_A) : I → A という射も定義しています。が、今はトレースは考えません。

対角付きフレイド圏と対角順次積

(C, K, J) がフレイド圏のとき、Cはデカルト・モノイド圏だったので、必ず自明な対角構造（デカルト積の対角とほんとの終射）を持ちます。Kも対角構造を持つと仮定して、関手Jは対角構造を厳密に保存するとします。つまり、次の条件を追加します。

J(Δ_A) = Δ_J(A) : J(A)→J(A)×J(A)
J(◇_A) = ◇_J(A) : J(A)→I

Jは、対角付きプレモノイド圏のあいだの厳密な構造保存関手となります。CもKも対角付きで、Jが対角保存のとき、(C, K, J) を対角付きフレイド圏（Freyd category with diagonals）と呼ぶことにします。

対角付きフレイド圏のなかで考えることにして、Kの射 f:A→B, g:A→C に対して対角順次積 f &&& g は次のように定義できます。 f *** g = f |× g は順次積です。

f &&& g := Δ_A >>> (f *** g)

C内では、順次積は射のデカルト積 f×g ですから、対角順次積は Δ;(f×g) となります。これは、通常のデカルト・ペアリング <f, g> に他なりません。つまり、アロー記法での f &&& g は、デカルト・ペアリングのプレモノイド版だったわけです。