Alloyでは、タプルを矢印記号「->」で書くんですよね。最初は「なにこれ？」と思いました。例えば、aとbのタプル（この場合はペア）である (a, b) を、a->b と書くのです。集合の直積も同じ記法で、「集合Aと集合Bの直積」を A->B で表します*1。
最初は違和感があるものの、しばらく使っていると非常に具合がいいんです。なんでだろ？ なんでこの記法がうまく働くのだろう？ と考えてみたら、関係圏の閉構造にマッチしているからだと気が付きました。
内容：
- 関係圏と色々な積
- モノイド閉圏
- モノイド閉圏としての関係圏
- 矢印の秘密
関係圏と色々な積
関係圏Relは次のように定義される圏です。
- 対象の集まり*2|Rel|は、すべての集合からなる集まり。|Rel| = |Set|
- A, B∈|Rel| に対して、そのホムセット Rel(A, B) は、Pow(A×B) = (直積集合A×Bの部分集合の全体)。Rel(A, B) の要素、つまりRelの射を、「AからBへの関係」と呼ぶ。
- R:A→B, S:B→C in Rel に対して、RとSの（この順での）結合 R;S は： R;S := {(x, z)∈A×C | ∃y.[(x, y)∈R ∧ (y, z)∈S]} 。
- 対象Aの恒等射idAは： idA := ΔA := {(x, y)∈A×A | x = y} 。
このように定義されるRelが実際に圏になることは皆さん確認してください。Relは色々と面白い性質を持ちますが、それは割愛して、誤解しやすいところを以下に注意します。
集合の直積A×Bは、関係圏Rel内の直積ではありません。話をハッキリさせるために、次の言葉使いをします。
- 集合の直積 -- 与えられた実際の集合AとBに対して、Aの要素とBの要素からなるタプルを全部寄せ集めて構成した実際の集合
- 圏の直積（デカルト積、あるいは単に積） -- 与えられた対象AとBに対して、圏論の極限として（up-to-isoで）定まる対象
圏Relの対象は集合ですから、対象（集合）AとBに対して集合の直積A×Bを具体的に作れます。そうやって作った対象（集合）A×B は、圏論的な直積には（必ずしも）なってない、ということです。
では、圏Relに直積がないのか？ と言うとそうではありません。Relにおける圏論的直積は、集合の直和で与えられます。「直和が直積」なのです。そして、Relにおける圏論的直和（余直積、余積）もまた集合の直和なのです。圏論的な直積と直和が両方とも集合の直和で与えられ、集合の直積は圏論的直積でも圏論的直和でもありません。
この状況は、ベクトル空間の圏の場合とよく似ています。ベクトル空間の圏では、圏論的直積と圏論的直和は一致して*3、どちらも集合（ベクトル空間の台集合）の直積です。それとは別にテンソル積があり、これは圏論的直積でも圏論的直和でもありません。まとめておきましょう。
| 集合圏 | 関係圏 | ベクトル空間の圏 | |
|---|---|---|---|
| 圏論的直積 | 集合の直積 | 集合の直和 | 集合の直積 |
| 圏論的直和 | 集合の直和 | 集合の直和 | 集合の直積 |
| - | - | 集合の直積 | テンソル積 |
モノイド閉圏
圏Relにおいて、集合の直積は圏論的直積でも圏論的直和でもありませんが、集合の直積を作る演算はモノイド積にはなります。そこで、モノイド積を持つ圏とその閉構造について少し説明します。
C = (C, □, I) がモノイド圏だとは、Cが圏であり、さらに□とIで構成される構造が載っていることです。
- □:C×C→C は二項関手（双関手）である。
- IはCの対象である。Iを、単一対象の自明な圏1からCへの関手とみなすこともある。
- □とIは、モノイドと同様な法則を満たす。
正確に言えば、結合法則と左右の単位法則はup-to-isoのものです。そのことを述べるには、結合法則を与える自然同型αと左右の単位法則を与える自然同型λとρ、さらに一貫性法則も必要です。ですが、めんどくさいので「モノイドと同様な法則を満たす」で済ましておきます。同型や同値もあまり気にしないでイコール（=）で表します。
さて、Cの対象Aを固定して、右からの掛け算関手 (-)□A を考えます。この掛け算関手に右随伴関手（随伴対の右側相方）があるとき、それをAのベキ関手とか指数関手といいます。Aを右肩に乗せて (-)A と書くのが普通ですが、ここでは、[- ←A] と書きます。同様に、左からの掛け算関手 A□(-) の右随伴は [A→ -] とします。ホムセットのあいだの自然な同型の形で書けば以下のようです。
- C(X×A, Y) = C(X, [Y←A])
- C(A×X, Y) = C(X, [A→Y])
圏Cが対称（symmetric）で、モノイド積の左右の違いを無視していいのなら、次の形が便利です。
- C(X×A, Y) = C(X, [A→Y])
以下では対称性を仮定して、C = (C, □, I, σ) が対称モノイド圏だとします（σが対称）。どんな対象Aに対しても、Aのベキ（指数）関手 [A→ -] が存在するなら、その圏はモノイド閉です。
型付きラムダ計算の舞台となるデカルト閉圏はモノイド閉圏の典型的な例ですが、デカルトではないモノイド閉圏も存在します。他ならぬRelがその具体例となります。
モノイド閉圏としての関係圏
圏Rel内で、集合の直積×（くどいですが、圏の直積ではありません）と単元集合 I = {*} を考えると、(Rel, ×, I) はモノイド圏になります。Relの射、つまり関係 R:A→B, S:C→D に対して、R×S:A×C→B×D は、集合としてのR×Sを、同型 (A×B)×(C×D)→(A×C)×(B×D) を使って解釈し直すだけのことです。タプルの成分交換 (a, b)|→(b, a) をσとすると、(Rel, ×, I, σ) は対称モノイド圏です。
集合の直積に関する結合法則 (X×A)×Y = X×(A×Y) （同型）から、Pow((X×A)×Y) = Pow(X×(A×Y)) （同型）が導かれます。これと、関係圏Relのホムセットの定義より：
- Rel(X×A, Y) = Rel(X, A×Y)
これはつまり、関手 (-)×A の右随伴が A×(-) であることを示します。関係圏Relでは、集合の直積というモノイド積の指数が同じく集合の直積で与えられます*4。(-)×A の右随伴とみなした A×(-) を A->(-) と書くことにします。すると：
- Rel(X×A, Y) = Rel(X, A->Y)
一般に、AとBの指数対象 A->B は内部ホム hom(A, B) とみなせて、カリー化を内部化した関係が成立します。
- hom(A×B, C) = hom(A, B->C) in Rel
これは、次のように書けます。
- (A×B)->C = A->(B->C)
関係圏Relでは、指数演算「->」は集合の直積「×」なので、上のカリー化の式は単なる「×」の結合法則に帰着します。
- (A×B)×C = A×(B×C)
矢印の秘密
Alloyのように、直積を矢印で表してもツジツマがあうのは、関係圏Relでは、指数演算の実体が直積になっているからです。矢印による A->B を、あたかも「AからBへの関数の全体」のように解釈をしても、モノイド閉構造の恩恵から、デカルト閉圏のときと同じように事が進みます。だから、デカルト閉圏で培った矢印のメンタルモデルをあまり変更せずに済むわけです。
またAlloyでは、集合とそのあいだの関係だけで、高階の対象物を導入していません。それでも、カリー化／反カリー化の操作ができるので、記述力に不満を感じることが少ないのではないでしょうか。フラットな意味領域なのに、フラットのなかでも高階の対象物らしきものが扱えるのです。
いちおうの種明かしが出来たので、これで気兼ねなく矢印記法を使えます :-)
