Chapter 34

12.2 極限の例

さのたけと
さのたけと
2021.05.31に更新

ここまで我々は,圏論的な積は\mathbf{2}とよばれる簡単な圏によって生成された図式の極限であることを見てきた.

極限の例にはもっとずっと簡単なものがある: 終対象だ.すぐに想像するのはシングルトン圏が終対象を導くということだろうが,真実はもっとずっと飾り気のないものだ: 終対象は空圏(empty category)から生成される.空圏からの関手は何の対象も選ばず,したがって錐はただの頂点に収縮する.普遍錐はどの他の頂点からもそこに来る唯一の射を持つような孤独な頂点である.これが終対象の定義であることはわかるだろう.

次の面白い極限は イコライザ(equalizer) とよばれる.これは2つの対象とそれらの間を走る2つの並行な射(といつもどおり,恒等射たち)のなす圏から生成される極限である.この圏は2つの対象ab,そして2つの射からなるような図式を\mathbf{C}のなかから選ぶ:

f \mathtt{::}\ a \to b\\ g \mathtt{::}\ a \to b

この図式の上に錐を作るには,頂点cと2つの射影を追加することになる:

p\mathtt{::}\ c \to a\\ q\mathtt{::}\ c \to b

可換でなければいけなような三角形が2つできる:

q = f.p\\ q = g.p

これは,qはこれらの等式のうちの1つ(たとえばq=f.pのほう)で唯一つに決定されると言っており,qを図から取り除くことができる.すると,1つの条件だけが残ることになる:

f.p = g.p

これについて考える方法はこうだ.\mathrm{Set}に注意を集中すると,関数pの像はaの部分集合を定める.この集合に制限すれば,関数fgは等価である.

例えば,ax座標とy座標でパラメタ付けされた2次元平面だとしよう.bは実直線とし,さらに次を取る:

\begin{aligned} f~(x, y) &= 2 * y + x\\ g~(x, y) &= y - x \end{aligned}

これら2つの関数についてのイコライザは実数の集合(頂点c)と関数

p~t = (t, (-2) * t)

である.

(p~t)はこの二次元平面中で直線を定義することに注意しよう.この線に沿って,先の2つの関数は等価である.

もちろん,他にもこの等価性を導くような他の集合c'と関数p'も存在する:

f.p' = g.p'

が,そういったものはpを通して唯一な方法で分解される.例えば,c'としてシングルトン集合\{()\}をとり[1],関数として次を取る:

p'~() = (0, 0)

これはちゃんと錐になっている.なぜなら,f~(0, 0) = g~(0, 0)となっているからである.しかし,これは普遍的ではない.なぜなら,次のような唯一の分解hが存在するからである:

p' = p.h

ただし,

h~() = (0, 0)

そういうわけで,イコライザはf~x = g~xというタイプの等式を解くのに使うことができる.しかし,イコライザはもっと一般的なものである.なぜなら,これは代数学的にではなく対象と射の言葉で定義されているからだ.

等式を解く,というのをもっと一般的にした考え方はまた別の極限にあらわれている --- 引き戻し(pullback)である.今回も等価にしたい2つの射がやっぱりあるのだが,今度はそれらの定義域が異なる.次の形の3つ対象のある圏からはじまる: 1\rightarrow2\leftarrow3.この圏に対応する図式は2つの対象a, b, cと2つの射:

f \mathtt{::}\ a \to b\\ g \mathtt{::}\ c \to b

から成る.

この図式はしばしば 余スパン(cospan) とよばれる.

この図式の上にできる錐は頂点dと3つの射からなる:

p \mathtt{::}\ d \to a\\ q \mathtt{::}\ d \to c\\ r \mathtt{::}\ d \to b

可換性条件はrが他の射たちによって完全に決定されるということを言っており,図から取り除くことができる.なので,次の条件だけが残る:

g.q = f.p

引き戻しはこの形の普遍錐である.

再び集合だけに焦点を当てるなら,対象dacの元からなるペアであって,fが最初の要素に作用したものはgが2番目の要素に作用したものと同じであるようなものと思うことができる.これでも一般的すぎるというのなら,gが定数関数(g~\_=1.23ということにしよう)であるという特別な場合を考えてみるとよい(bは実数値の集合だと仮定している).すると,次の等式を解いていることになる:

f~x = 1.23

この場合,cの選択は(これが空集合でない限り)関係がなく,したがってシングルトン集合として取ることができる.例えば,集合aは3次元ベクトルの集合で,fがベクトルの長さとしよう.すると,引き戻しはペア(v, ())の集合(ただしvは長さ1.23のベクトルであり,等式\sqrt{(x^{2}+y^{2}+z^{2})} = 1.23の解)であり,()はシングルトン集合のダミー元である.

しかし引き戻しはもっと一般的な応用があり,プログラミングにも使える.例えばC++のクラスを,射がサブクラスとスーパークラスとを繋ぐ矢印である圏として考えよう.継承は推移的な性質だと考えられるので,もしCBを継承し,BAを継承しているなら,CAを継承している(だって,CへのポインタをAへのポインタが期待されているところに渡すことはできるでしょう).また,すべてのクラスが恒等射を持つように,CCを継承していると仮定することにする.このようにして,サブクラス関係はサブタイピングと整合するようになる.C++はまた多重継承をサポートしているので,2つのクラスBCAを継承し,4番目のクラスDBCを多重に継承しているというダイヤモンド継承の図式を構成することができる.普通,DAの2つのコピーを持つことになるが,これは全く望まれることではない.しかし,DAのコピーを1つだけ持つように仮想継承を使うことができる.

Dをこの図式の引き戻しにすることは何を意味するのだろう?これはBCとを多重に継承するどんなクラスEもまたDのサブクラスであることを意味している.これを(サブタイピングが名前で行なわれる)C++で直接表現することはできない(C++コンパイラがこの種のクラス関係を推論することはないだろう --- これには「ダックタイピング」が必要だ).しかし,サブタイピング関係の外側に出て,EからDへのキャストが安全かどうかを代わりに問うことはできる.このキャストは,DBCとを(追加のデータやメソッドのオーバーライドなしに)そのまま組み合わせたものなら安全だろう.そしてもちろん,BCとのメソッドたちの間に名前の衝突があるなら,引き戻しは存在し得ない.

型推論では引き戻しのもっと進んだ使い方もある.しばしば,2つの式の型を 単一化(unify) する必要がある.例えば,コンパイラにある関数の型を推論してほしいとしよう:

twice f x = f (f x)

コンパイラは,すべての変数と部分式に準備の型を割り当てる.具体的には,このように割り当てられるだろう:

f       :: t0
x       :: t1
f x     :: t2
f (f x) :: t3

ここから次が推論される:

twice :: t0 -> t1 -> t3

コンパイラは関数適用のルールから結論づけられる制約の集合を見つけもする:

t0 = t1 -> t2 -- fはxに適用されるから 
t0 = t2 -> t3 -- fは(f x)に適用されるから

両方の式の未知の型を置換したときに同じ型を生成するような型(あるいは型変数)の集合を見つけることによって,これらの制約は単一化されることになる.そのような置換の1つは:

t1 = t2 = t3 = Int 
twice :: (Int -> Int) -> Int -> Int

だが,明らかにこれは最も一般的なものではない.最も一般的な置換は引き戻しによって得られる.この本の範疇から外れるので詳細には踏み込まないが,その結果は次のようになるだろうということで納得してほしい:

twice :: (t -> t) -> t -> t

ここで,tは自由な型変数である.

(和訳:@ashiato45

脚注
  1. 訳注: シングルトン集合は1元からなる集合で,圏論の本だとそのただ1つの元は★などで表示されることが多いです.この本では,Haskellのunit typeが取りうるただ1つの値()を使っているようです. ↩︎