非交替的な積を持つ圏達 - 檜山正幸のキマイラ飼育記 (はてなBlog)

デカルト作用圏やフレイド圏は随分と役に立つなー、と実感。リアルな（現実をうまく写す）計算モデルを簡単に作れるようになりました。

さてところで、デカルト作用圏（Cartesian effect category）、バイノイド圏（binoidal category）、プレモノイド圏（premonoidal category）、フレイド圏（Freyd category）などに共通する構造はどんなものでしょう。いずれも、モノイド圏（特にデカルト圏）を拡張した形をしています。モノイド圏をベースにしながら、交替律（interchange law）を満たさない積を導入しています。

評価順序の後先が影響する計算を定式化するには、非交替的（non-interchangable）な積を持つ圏が必要になります。そこで、非交替的な積を持つ圏を一般的に考えてみます。

まず前提となる状況として、圏Kと、Kの広い部分圏Cがあります。C上には、交替律を満たす積が指定されているとして、それを「×」（掛け算）と書きます。積×に対する単位対象や、結合律、単位律の構造同型や一貫性はまだ仮定しません。単にC上に交替的積があるというだけです。

バイノイド構造

ここで、`× と ×' という2つの対応を考えます。

`× : K×C→K
×' : C×K→K

ちょっと混乱しそうですが、K×C の「×」は圏の直積です（圏の直積と圏のなかの掛け算のどちらであるかは文脈で判断してください）。圏のなかで定義された演算`×と×'は次を満たすとします。

C×Cに制限すると、`×も×'も×に一致する。u, v∈C ならば、u `× v = u ×' v = u × v *1。
f, g∈K、u, v∈C に対して、(f `× u);(g `× v) = (f;g)`×(u;v)
f, g∈K、u, v∈C に対して、(u ×' f);(v ×' g) = (u;v)×'(f;g)

`×も×'も、K全域では定義されていません。定義されている範囲に限定すれば交替律が成立しています。ここでは、`×を左バイノイド積（left binoidal product）、×'を右バイノイド積（right binoidal product）と呼びます。通常のバイノイド積より少しだけ一般化されてますが、大差ありません。(K, C, `×, ×') をバイノイド構造（binoidal structure）と呼ぶことにします。バイノイド構造には左右2つの積が含まれます。

次に、`×と×'を使って、左順次積（left sequential product）「|×」と右順次積（right sequential product）「×|」を定義します。順次積は後付けで定義できるので、バイノイド構造に最初から入っている必要はありません。

f |× g := (f '× id);(id ×' g)
f ×| g := (id ×' g);(f '× id)

|× と ×| は K×K で定義されます。しかし、交替律を満たすことは保証されていません。

Kの射kが中心射（central morphism）であるとは次を満たすことです。

任意のKの射fに対して、f |× k = f ×| k かつ k |× f = k ×| f 。

バイノイド圏とバイノイド関手

バイノイド構造 (K, C, `×, ×') をバイノイド圏（binoidal category）とも呼びます。気分としては、記号と用語の乱用をして「Kはバイノイド圏とする」のように言いたいときに用語「バイノイド圏」を使いましょう、ってことです。作用圏（effect category）の用語を借用して、ここでは、Cをバイノイド圏Kの純部分圏（pure subcategory）と呼びます*2。

純部分圏は広い部分圏でなくてはならないので、最小の純部分圏は|K|に離散圏の構造を入れたものです。本来のバイノイド圏の定義は、C = |K|（離散圏）としたものです。

2つのバイノイド圏 K = (K, C, `×, ×') と L = (L, D, `●, ●') があるとき、K からL へのバイノイド関手（binoidal functor）は、関手 F:K→L と2つの自然変換φ、ψの組み合わせ (F, φ, ψ) で定義できるでしょう。

φ_A,B: F(A) `● F(B) → F(A `× B)
ψ_A,B: F(A) ●' F(B) → F(A ×' B)

次の条件を満たす必要があります。

関手Fは、純射を純射に移す。つまり、u∈C ならば F(u)∈D 。
φとψの成分は、すべて中心同型射である。

プレモノイド圏とプレモノイド関手

バイノイド圏は、純部分圏と左右2つの積を持ちますが、積に関する計算法則は何もありません。モノイド圏と同様に、結合法則と左右の単位法則が成立するとき、プレモノイド圏（premonoidal category）と呼びます。

結合法則、左単位法則、右単位法則を記述するために、構造同型射 α_A,B,C:(A×B)×C → A×(B×C)、λ_A:I×A→A、ρ_A:A×I→A が中心同型射として指定されており、モノイド圏と同じ一貫性条件*3を満たすとき、それらの全体がプレモノイド圏を定義します。積が部分的にしか定義されてない、あるいは（順次積を考えると）交替律を満たさないところを除けば、プレモノイド圏とモノイド圏は同じ法則性を持ちます。

CとDがプレモノイド圏のとき、バイノイド関手に η:F(I)→I という変換を加えた、(F, φ, ψ, η) がモノイド関手と同じ一貫性条件*4を満たせば、プレモノイド関手（premonoidal functor）になります。

フレイド圏

どうしてプレモノイド圏のような概念を考えるのか？その理由のひとつは、モノイド圏の上で定義されたモナドをよりよく理解するためだと思います。ベースの圏がモノイド圏ならば、モナドのクライスリ圏にもやっぱり“積”が欲しくなります（かなり切実な要求！）。モナドがベースの積に関するテンソル強度（tensorial strength）を持てば、クライスリ圏に積を入れることができます。が、これはモノイド積（交替積）になるとは限りません。交替律の成立を要求すると、モナドは可換モナドとなりますが、これは条件がきつすぎて応用範囲を狭めてしまいます。例えば、ストレージ更新モナドは扱えません。

結局、交替律を断念して実用性を取る判断となります。そこでプレモノイド圏が出てくるのでしょう。プレモノイド圏は、交替律が使えないので不便ではありますが、プログラムの挙動により近いので、まー、不便さは我慢して注意深く計算するしかないですね。この「注意」は、評価順序に依存するプログラムを扱うときの注意と同じです。

さて、モナドのクライスリ圏では、モナド単位を使って、ベースの圏Cからクライスリ圏Kへの関手 J:C→K を作れます。多くの実用的なケースでは、Jが埋め込みになっています。(C, K, J:C→C) という組み合わせを、モナドの定義とは独立に定式化したものがフレイド圏です。

(C, K, J:C→K) がフレイド圏（Freyd category）であるとは：