日記 (2020 年 4 月 16 日)

4 月 15 日の続き。前回は、アローの形式化として型システム Arrow を定義した。今回は、この型システムに対応する圏として知られている Freyd 圏の定義を行う。

Freyd 圏を定義する準備として、まずはバイノイダル圏と前モノイダル圏を定義する。これらは通常のモノイダル圏の定義を弱めたもので、 Power–Robinson†1 によってプログラミング言語の表示的意味論を記述するために導入されたものである。ここでは、カルテシアン閉圏 󰒚 に対して 󰒚-豊穣圏の文脈で定義を行う。なお、 󰒚-豊穣圏 󰒛 の射対象は [-,-] で表す。

定義 2.1.

カルテシアン閉圏 󰒚 および 󰒚-豊穣圏 󰒛 を考える。 󰒛 の対象 A,B に対し、 󰒚-豊穣関手 -⋉B:󰒛→󰒛 および A⋊-:󰒛→󰒛 がそれぞれ定まっていて、対象について A⋉B=A⋊B が成り立っているとする。このとき、 󰒛 を「バイノイダル圏 (binoidal category)」という。

バイノイダル圏 󰒛 の対象 A,B に対し、定義より A⋉B と A⋊B は等しいので、以降はこれを A⋈B と書くことにする。

モノイダル圏とバイノイダル圏との違いについて述べておこう。ここでは、簡単のため 󰒚=Set として、一般の豊穣圏ではなく通常の圏を考える。モノイダル圏 󰒛 では、演算が 2 変数関手 ⋈:󰒛×󰒛→󰒛 として定まっているので、 2 つの射 f:A→A󰎘,g:B→B󰎘 に対して射 f⋈g:A⋈B→A󰎘⋈B󰎘 が存在し、可換図式 A⋈BA󰎘⋈BA⋈B󰎘A󰎘⋈B󰎘f⋈idid⋈gf⋈idid⋈g の共通の合成になっている。しかし、バイモノイダル圏 󰒛 では、演算が 2 変数関手として定まっているわけではなく、片方の変数をそれぞれ動かす 2 種類の関手が定まっているだけなので、 f⋉id や id⋊g という射しか考えることはできず、変数を同時に動かす f⋈g という射は必ずしも存在しない。さらに、上の図式も一般には可換にならない。

これは、プログラミング言語の次のような特徴を反映したものであると解釈できる。計算に副作用を許す場合、 2 つの計算 f,g を行う順序を変えると、最終的な結果が異なる可能性がある。例えば、 f,g がともにコンソールにログを出力するような計算である場合、 f,g の順序を逆にして実行すれば、最終的にコンソールに出力されるログも逆になる。したがって、 f を行った後に g を行う計算 (上の図式では右→下の順での合成に対応する) と g を行った後に f を行う計算 (上の図式では下→右の順での合成に対応する) が、必ずしも同一の計算になるとは限らない。バイノイダル圏では、片方の変数のみを動かす関手を 2 つ用意することによって、この特徴を圏論側でも実現したのである。

別の計算との実行順序を変えても全体の計算が変わらないような計算には、特別な名前が付いている。

定義 2.2.

カルテシアン閉圏 󰒚 および 󰒚-豊穣バイノイダル圏 󰒛 を考える。 󰒚 の対象 X および 󰒛 の対象 A,A󰎘 に対し、 󰒚 の射 f:X→[A,A󰎘] をとる。任意の 󰒛 の対象 B,B󰎘 に対し、図式 X×[B,B󰎘][B,B󰎘]×X[A,A󰎘]×[B,B󰎘][B,B󰎘]×[A,A󰎘][A⋈B,A󰎘⋈B]×[A󰎘⋈B,A󰎘⋈B󰎘][A⋈B,A⋈B󰎘]×[A⋈B󰎘,A󰎘⋈B󰎘][A⋈B,A󰎘⋈B󰎘]f×idid×f(-⋉B)AA󰎘×(A󰎘⋊-)BB󰎘(A⋊-)BB󰎘×(-⋉B󰎘)AA󰎘 X×[B,B󰎘][B,B󰎘]×X[A,A󰎘]×[B,B󰎘][B,B󰎘]×[A,A󰎘][B⋈A,B⋈A󰎘]×[B⋈A󰎘,B󰎘⋈A󰎘][B⋈A,B󰎘⋈A]×[B󰎘⋈A,B󰎘⋈A󰎘][B⋈A,B󰎘⋈A󰎘]f×idid×f(B⋊-)AA󰎘×(-⋉A󰎘)BB󰎘(-⋉A)BB󰎘×(B󰎘⋊-)AA󰎘 がともに可換であるとき、 f は「中心的 (central)」であるという。なお、水平なラベルのない射は標準的な同型射であり、残りのラベルのない射は合成を表す射である。

これだけでは少し分かりづらいので、 󰒚=Set かつ X=1 の場合を考え、通常の圏の言葉で定義を言い直しておこう。まずこの場合は、 Set の射 f:1→[A,A󰎘] は 󰒛 の射 f:A→A󰎘 と同一視できる。この同一視のもと、射 f:A→A󰎘 が中心的であることは、任意の射 g:B→B󰎘 に対して、 A⋈BA󰎘⋈BA⋈B󰎘A󰎘⋈B󰎘f⋉BA⋊gf⋉B󰎘A󰎘⋊gB⋈AB⋈A󰎘B󰎘⋈AB󰎘⋈A󰎘B⋊fg⋉AB󰎘⋊fg⋉A󰎘 が可換であることと同値になる。これは、定義の前に述べた通り、 f と他の計算は順序を逆に実行しても同じ結果になるということを意味している。

定義 2.3.

カルテシアン閉圏 󰒚 および 󰒚-豊穣バイノイダル圏 󰒛 に対し、

󰒛 の対象 ⊤ が定まっている。
各対象 A,B,C に対して、中心的な 4 種類の 󰒚 の射 αABC: 1 → [(A⋈B)⋈C,A⋈(B⋈C)] λA: 1 → [A,⊤⋈A] ρA: 1 → [A,A⋈⊤] σAB: 1 → [A⋈B,B⋈A] が定まっており、これらがそれぞれ同型な 󰒚-豊穣自然変換を定める。

という構造が定まっており、モノイダル圏と同様の一貫性条件 (五角形図式と三角形図式に対応するもの) を満たすとする。このとき、 󰒛 を「対称前モノイダル圏 (symmetric premonoidal category)」という。

対称前モノイダル関手は、対称前モノイダル圏の構造を全て保つ関手である。 Freyd 圏を考える上では、全ての構造を (同型ではなく) 等号として保つ場合のみを考えれば十分なので、その場合のみの定義を述べる。

定義 2.4.

カルテシアン閉圏 󰒚 をとる。 󰒚-豊穣対称前モノイダル圏 󰒛󰎘,󰒛 の間の 󰒚-豊穣関手 J:󰒛󰎘→󰒛 に対し、

J⊤=⊤ が等号として成り立つ。
J は対称前モノイダル圏に定まる 2 種類の演算を等号として保つ。すなわち、任意の 󰒛󰎘 の対象 A,B に対して、 J(A⋈B)=JA⋈JB が成り立ち、さらに任意の 󰒛󰎘 の対象 A󰎘,B󰎘 に対して、図式 [A,A󰎘][JA,JA󰎘][A⋈B,A󰎘⋈B][JA⋈JB,JA󰎘⋈JB]JAA󰎘JA⋈B,A󰎘⋈B(-⋉B)AA󰎘(-⋉JB)JA,JA󰎘[B,B󰎘][JB,JB󰎘][A⋈B,A⋈B󰎘][JA⋈JB,JA⋈JB󰎘]JBB󰎘JA⋈B,A⋈B󰎘(A⋊-)BB󰎘(JA⋊-)JB,JB󰎘 がともに可換である。
J は対称前モノイダル圏に定まる 4 種類の構造射を等号として保つ。例えば λ については、任意の 󰒛󰎘 の対象 A に対して、図式 ⊤[⊤,⊤⋈A][⊤,⊤⋈JA]λAλJAJ⊤,⊤⋈A は可換である。それ以外の種類の構造射についても同様の可換図式が成り立つ。

が全て成り立つとき、 J を「厳密対称前モノイダル関手 (strict symmetric premonoidal functor)」という。

さて、カルテシアン閉圏 󰒚 に対し、 󰒚 自身はカルテシアン閉性によって 󰒚-豊穣圏と見なせる。さらに、 󰒚 は直積によって 󰒚-豊穣対称前モノイダル圏の構造をもつ。以降はこの構造を利用して、 Freyd 圏は以下のように定義できる。

定義 2.5.

カルテシアン閉圏 󰒚 および 󰒚-豊穣対称前モノイダル圏 󰒛 をとる。 󰒚-豊穣厳密対称前モノイダル関手 J:󰒚→󰒛 が、 2 条件

J は対象上恒等写像である。すなわち、 󰒚 と 󰒛 の対象は同一であり、任意の 󰒚 の対象 A に対して、 JA=A が等号として成り立つ。
J の射の像は全ての中心的である。すなわち、任意の 󰒚 の対象 A,A󰎘 に対して、 󰒚 の射 JAA󰎘:A⇀A󰎘→[A,A󰎘] は中心的である。

を満たすとする。このとき、 (󰒚;󰒛,J) を「豊穣 Freyd 圏 (enriched — category)」という。

Freyd 圏の気持ちを軽く述べておこう。 Freyd 圏を構成する 2 つの圏のうち、 󰒚 は通常の関数が住む圏で、 󰒛 は副作用のある計算が住む圏である。副作用のある計算は順序を変えると結果が変わる可能性があるので、 󰒛 の方は (モノイダル圏ではなく) 前モノイダル圏になっているのである。この間に定まる関手 J は、通常の関手を副作用付きの計算と見なすために使われるもので、モナドの return やアローの arr に対応するものである。 J の像が中心的であるという条件は、 J の像は副作用付きの計算と見なしてはいるが実際には副作用がないので、他の計算との順序を自由に入れ替えられるいう性質を反映している。

次回はいよいよ Freyd 圏を用いたアローの解釈を行う。

参考文献

J. Power, E. Robinson (1997) 「Premonoidal categories and notions of computation」『Mathematical Structures in Computer Science』 7:453–468
J. Power, H. Thielecke (1997) 「Environments, continuation semantics and indexed categories」『Theoretical Aspects of Computer Software』 391–414