【しゃあっコヒーレンス・スペース！】整合空間(coherence space)をじっくりとその1

　↓これの続きっちゃあ続きである。

cut-elimination.hatenablog.com

"Proofs and Types"を読んでいくシリーズだったが、第7章のSystem Tの導入をちょっと飛ばして第8章の整合空間(coherence space)を詳細に読みたいのよ。

　整合空間から線形論理を解説している照井先生の「線形論理の誕生」という論文も勉強になるので適宜参照する。

動機

　整合空間はプログラムの表示的意味論を構築するための数学的道具である。まず表示的意味論の発想というものがちゃんと解説されている。「誕生」でも似たような議論がある。表示的意味論では、型を集合、関数としてのプログラムを数学的な関数と対応させる。しかしこの時、どのような数学的関数を取ってこれば良いかが問題となる。「あらゆる関数」としてしまうと意味がない*1。スコット流の表示的意味論（領域理論）では、型を位相空間（領域、ドメイン）と対応させ、関数をそれらの間の連続写像に限定する。こうすることでデータやプログラムに近似を導入し、逆に言うと近似が可能な集合や関数に表示的意味論を限定できたのである。ちょっと先走ると、整合空間による意味論は、型を整合空間とし、連続写像に更なる性質を加えた安定写像というものに関数を限定する訳だ*2。

　ジラール先生はスコット流の表示的意味論にいくつか不満を述べている。一つは関数空間の収束を上手く扱えないとか書いてあるのだが私にはよく分らなかった。もう一つは、トポロジーという幾何学的な道具立てがあまり意味を成していないという点である。スコット意味論が位相空間になったのは単なる偶然ではないかと指摘している。「よってトポロジー的直観自体が誤りではないかと考え、もっと別なのを探そうとするのは自然なことである」（54ページ）。

　この批判がどれくらい刺さっているのかは分らないが、そういうわけなので整合空間理論はトポロジーに拘らない。スコット意味論を更に単純化して再構成する。

定義、例

　整合空間の定義は以下の通り。

定義：整合空間とは、以下の条件を満す（集合の）集合 ${\mathcal A}$ である。

1) $a \in {\mathcal A}$ かつ $a' \subset a$ ならば $a' \in {\mathcal A}$ 。

2) $M \subset {\mathcal A}$ として $(\forall a_1, a_2 \in M)[a_1 \cup a_2 \in {\mathcal A}]$ ならば $\bigcup M \in {\mathcal A}$ 。

すぐに分るのは、 $\emptyset \in {\mathcal A}$ である。何故なら何かしらの $a \in {\mathcal A}$ について $\emptyset \subset a$ なので条件1)より。個々の整合空間はデータの領域を表す。※整合空間全体の集合というのが存在するのかどうか分らないので、以下ちょっとボカします。

　例が挙げられている。まず ${\mathcal Bool}$ は $\{\emptyset, \{{\bf t}\}, \{{\bf f}\}\}$ というもの。そして ${\mathcal Int}$ は $\{\emptyset, \{0\}, \{1\}, \{2\}, ...\}$ という感じ。どちらも定義を満たしている。部分集合や和集合が簡単なものしかないので確かめるのは容易である。整合空間ではないものの例としては $\{\emptyset, \{0\}, \{1\}, \{2\}, \{1, 2\}, \{0, 2\}, \{0, 1\}\}$ というのが挙げられている。部分集合 $\{\{0\}, \{1\}, \{2\}\}$ はどの二つの要素の和集合ももとの集合に属すが、 $\bigcup \{\{0\}, \{1\}, \{2\}\} = \{0, 1, 2\}$ はそうではない（ $\{0, 1, 2\}$ を要素として付け加えれば整合空間になる）。

　続いて網の定義

$|{\mathcal A}| := \bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$

とする。 $|{\mathcal A}|$ の要素をトークンと呼ぶ。トークン間の ${\mathcal A}$ を法とした整合関係を以下のように定義する。

　 $\alpha \ddagger \alpha' \; ({\rm mod} \; {\mathcal A})$ *3　iff　 $\{\alpha, \alpha'\} \in {\mathcal A}$

これは反射的で対称的な関係である。よって $|{\mathcal A}|$ に $\ddagger$ を付与したものは（反射的な）無向グラフとなり、これを ${\mathcal A}$ の網(web)と呼ぶ。

整合空間の性質と諸々の証明、そして考察

　整合空間 ${\mathcal A}$ について $\bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ となることを証明しておく。

命題1：整合空間 ${\mathcal A}$ について $\bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ 。

証明： $\alpha' \in \bigcup {\mathcal A}$ とすると、ある $a \in {\mathcal A}$ が存在して $\alpha' \in a$ 。この $a$ について $\{\alpha'\} \subset a$ が言える。整合空間の定義1)より $\{\alpha'\} \in {\mathcal A}$ 。よって $\alpha' \in \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ 。故に $\bigcup {\mathcal A} \subset \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ 。

　また、 $\alpha' \in \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ ならば $\{\alpha'\} \in {\mathcal A}$ であるが、 $\alpha' \in \{\alpha'\}$ なので $\alpha' \in \bigcup {\mathcal A}$ 。よって $\{\alpha \mid \{\alpha\} \in {\mathcal A}\} \subset \bigcup {\mathcal A}$ 。

　以上より $\bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}$ 。

この命題から、整合空間からその網への対応付け $|\cdot|$ は単射だということも見て取れる。全ての網には当然対応する整合空間が存在するので、整合空間(たち)と網(たち)の間には全単射が存在する。しかしこれだけにとどまらない。

　網からもとの整合空間を得る具体的な操作がある。まずは以下の命題を示す。

命題2：整合空間 ${\mathcal A}$ について以下が成立つ。

　 $a \in {\mathcal A} \Leftrightarrow a \subset |{\mathcal A}|$ & $(\forall \alpha_1, \alpha_2 \in a)[\alpha_1 \ddagger \alpha_2\; ({\rm mod} \; {\mathcal A})]$

証明： $(\Rightarrow)$ $a \in {\mathcal A}$ と仮定する。 $\alpha \in a$ ならば $\{\alpha\} \subset a$ が言えるので、整合空間の定義1)より $\{\alpha\} \in {\mathcal A}$ 。よって網の定義より $\alpha \in |{\mathcal A}|$ なので $a \subset |{\mathcal A}|$ 。また、任意の $\alpha_1, \alpha_2 \in a$ について $\{\alpha_1, \alpha_2\} \subset a$ が言えるが、これも同様に $\{\alpha_1, \alpha_2\} \in {\mathcal A}$ 。よって $\alpha_1 \ddagger \alpha_2\; ({\rm mod} \; {\mathcal A})$ 。

$(\Leftarrow)$ $a \subset |{\mathcal A}|$ と $(\forall \alpha_1, \alpha_2 \in a)[\alpha_1 \ddagger \alpha_2 \; ({\rm mod} \; {\mathcal A})]$ すなわち $(\forall \alpha_1, \alpha_2 \in a)[\{\alpha_1, \alpha_2\} \in {\mathcal A}]$ を仮定する。 $\{\{\alpha\} \mid \alpha \in a\}$ という集合を考える。 $\{\alpha'\} \in \{\{\alpha\} \mid \alpha \in a\}$ ならば $\alpha' \in a$ であり、仮定より $\alpha' \in |{\mathcal A}|$ 。よって網の定義より $\{\alpha'\} \in {\mathcal A}$ となるから、 $\{\{\alpha\} \mid \alpha \in a\} \subset {\mathcal A}$ である。また任意の $\{\alpha_1\}, \{\alpha_2\} \in \{\{\alpha\} \mid \alpha \in a\}$ について $\alpha_1, \alpha_2 \in a$ なので、仮定より $\{\alpha_1, \alpha_2\} = \{\alpha_1\} \cup \{\alpha_2\} \in {\mathcal A}$ 。以上と整合空間の定義2)から $\bigcup \{\{\alpha\} \mid \alpha \in a\} \in {\mathcal A}$ 。しかし $\bigcup \{\{\alpha\} \mid \alpha \in a\} = a$ であるので $a \in {\mathcal A}$ 。

全てのノード間に辺があるグラフを完全グラフという。あるグラフの完全グラフであるような部分グラフをグラフ理論ではクリークという。この命題が主張するのは、整合空間から網を作った時、網のクリークの集合がもとの整合空間になっているという事である。

　もっと言うと実は整合空間はグラフとクリークから定義できる。まず、任意の反射的無向グラフのクリークの集合は整合空間になる。

命題3：反射的無向グラフのクリークの集合は整合空間である。

証明：反射的無向グラフ ${\mathcal G} = (G, \ddagger)$ のクリークの集合 $C({\mathcal G})$ （より厳密にはクリークのノードの集合の集合）が整合空間の定義の二つの条件を満している事を示す。

1) $g \in C({\mathcal G})$ かつ $g' \subset g$ と仮定する。任意の $\gamma_1, \gamma_2 \in g'$ について $\gamma_1, \gamma_2 \in g \in C({\mathcal G})$ なので、 $\gamma_1 \ddagger \gamma_2$ 。よって $g'$ もクリークなので $g' \in C({\mathcal G})$ 。

2) $M \subset C({\mathcal G})$ とし、 $(\forall g_1, g_2 \in M)[g_1 \cup g_2 \in C({\mathcal G})]$ とする。任意の $\gamma_1, \gamma_2 \in \bigcup M$ についてある $g'_1, g'_2 \in M$ が存在し $\gamma_1 \in g'_1$ かつ $\gamma_2 \in g'_2$ 、よって $\gamma_1, \gamma_2 \in g'_1 \cup g'_2$ 。仮定より、 $g'_1 \cup g'_2 \in C({\mathcal G})$ なので $\gamma_1 \ddagger \gamma_2$ 。したがって $\bigcup M$ もクリークなので $\bigcup M \in C({\mathcal G})$ 。

命題2より、任意の整合空間は整合関係で作った反射的無向グラフのクリークの集合だった。そして命題3より、任意の反射的無向グラフのクリークの集合は整合空間である。よって以下が言える。

定理：整合関係と反射的無向グラフのクリークの集合は同じである（クラスとして一致する）。

　反射的無向グラフからクリークの集合を得る操作は、反射的無向グラフたちから整合空間たちへの写像となる。しかも命題2を見れば分る通り、この操作は整合空間から網を得る操作（これは命題1より単射だった）の逆写像になっている（よって整合空間（反射的無向グラフのクリークの集合）と網との間には全単射がある）。反射的無向グラフから整合空間を作り、その網を定義するともとの反射的無向グラフに戻るのである。よって反射的無向グラフは常に何らかの整合空間の網となる。なので整合空間を定義する際は、反射的無向グラフを網と呼んでそのクリークの集合を整合空間としても良い。「線形論理の誕生」ではこの方法で定義しているのだが、反射的無向グラフ(網)の方を整合空間と呼んでる。この定義でも良い訳だが、適宜読み替える必要がある。

　反射的無向グラフから整合空間を作った時、その網を定義通りに作ったらそれがちゃんともとのグラフになっているかどうかは気になる所である。反射的無向グラフから網を作る操作が全単射であるということがもう分っているからこれは既に示されている筈だが、もうちょい考えてみる。命題3の証明中の定義を再利用する。 $\gamma_1, \gamma_2 \in |C({\mathcal G})|$ が $\gamma_1 \ddagger \gamma_2 \; ({\rm mod} \; C({\mathcal G}))$ とは、 $\{\gamma_1, \gamma_2\} \in C({\mathcal G})$ ということ、すなわち $\{\gamma_1, \gamma_2\}$ が ${\mathcal G}$ のクリークという事である。これは $\gamma_1 \ddagger \gamma_2$ と同値である。つまり $\gamma_1 \ddagger \gamma_2 \; ({\rm mod} \; C({\mathcal G}))$ と $\gamma_1 \ddagger \gamma_2$ は同値な訳で、万事オッケーである。