【しゃあっコヒーレンス・スペース！】整合空間(coherence space)をじっくりとその2 安定関数(stable function)

　↓これの続きです。

cut-elimination.hatenablog.com

今回は安定関数が出てくるはずです。

用語の整理

　いろいろ用語、記法が出てきている。

用語・記法：整合空間 ${\mathcal A}$ の要素を ${\mathcal A}$ の点(point)という。 $|{\mathcal A}|$ のクリークを整合部分集合(coherence subset)とも言う。点とは即ち整合部分集合である。また、 ${\mathcal A}$ の点のうち有限集合であるものの集合を ${\mathcal A}_{fin}$ と書く。

　もうちょっと定義っぽい定義も出てくる。

定義： $a \in {\mathcal A}$ の近似(approximant)とは、任意の $a$ の部分集合 $a'$ である。有限近似とは近似のうち有限集合であるもの。

整合空間の定義1)より、近似も ${\mathcal A}$ の要素である。

有限近似の性質

　近似は有限のものさえあれば良さそうだということが徐々に示されていく。まずは以下の命題。

命題1：任意の $a \in {\mathcal A}$ はその有限近似の集合の和である。即ち

　 $a = \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}$

証明： $\alpha \in a$ とすると、 $\alpha \in \{\alpha\} \subset a$ となり、勿論 $\{\alpha\}$ は有限集合なので $\alpha \in \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}$ 。よって $a \subset \bigcup \{a_\circ \mid a_\circ \subset a$ & $a_\circ \; {\rm finite} \}$ 。また $\alpha \in \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}$ とすると、ある $a$ の有限部分集合 $a'$ が存在して $\alpha \in a'$ 。よって $\alpha \in a$ なので $\bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \} \subset a$ 。以上より $a = \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}$ 。

また、以下も成立つ。

命題2： $a \in {\mathcal A}$ の有限近似の集合 $I$ は有向である。即ち、 $I$ は空でなく、任意の二つの要素 $a_1, a_2 \in I$ に対して $a_1, a_2 \subset a'$ となる $a' \in I$ が存在する。

証明：どんな集合でも空集合を部分集合として持つため、常に $\emptyset \in I$ 。よって $I$ は空でない。また、 $a_1, a_2 \in I$ の時、 $a' = a_1 \cup a_2$ とすればこれも $a$ の有限部分集合なので $a_1, a_2 \subset a'$ かつ $a' \in I$ 。以上から $I$ は有向集合である。

　近似の導入は、再帰理論において全関数ではない部分関数を考えるように、様々なデータに全的な(真な)ものと部分的なものとの区別を与えることになる。これが近似の発想だとジラール先生は述べている。ただし ${\mathcal Bool}$ や ${\mathcal Int}$ は、全的なものはブール値や自然数のシングルトンで部分的なものは空集合という単純な分れ方をする。

　その後いろいろ書いてあるのは難しげなので割愛。安定関数に移る。

安定関数の定義と性質

定義：二つの整合空間 ${\mathcal A}, {\mathcal B}$ が与えられた時、 ${\mathcal A}$ から ${\mathcal B}$ への関数 $F$ が安定であるのは、以下の条件を満す時である。

1) $a' \subset a \Rightarrow F(a') \subset F(a)$ 　単調性

2) $F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i))$ （ $\{a_i\}_{i \in I}$ は有向集合族）連続性

3) $a_1 \cup a_2 \in {\mathcal A} \Rightarrow F(a_1 \cap a_2) = F(a_1) \cap F(a_2)$ 　安定性

実は連続性は単調性を含意している

命題3： $F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i)) \Rightarrow [a' \subset a \Rightarrow F(a') \subset F(a)]$

証明： $F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i))$ を仮定する。 $a' \subset a$ とすると $\{a', a\}$ は有向集合になる。よって仮定より $F\bigl(\bigcup \{a', a\}\bigr) = F(a) = \bigcup \{F(a'), F(a)\}$ 。 $F(a') \subset \bigcup \{F(a'), F(a)\}$ なので $F(a') \subset F(a)$ 。

　連続性について重要な性質がある。

命題4： $F$ は連続 $\Leftrightarrow F(a) = \bigcup \{F(a_\circ) \mid a_\circ \subset a, \; a_\circ \; {\rm finite}\}$ & $F$ は単調

証明： $(\Rightarrow)$ $F$ が連続と仮定する。命題1より、 $a = \bigcup \{a_\circ \subset a, \; a_\circ \; {\rm finite}\}$ 。これと命題3より。

$(\Leftarrow)$ $F(a) = \bigcup \{F(a_\circ) \mid a_\circ \subset a, \; a_\circ \; {\rm finite}\}$ & $F$ は単調を仮定する。単調性より、任意の有向集合族 $\{a_i\}_{i \in I}$ について $F(a_i) \subset F(\bigcup^\uparrow_{i \in I} a_i)$ なので、 $\bigcup F(a_i) \subset F(\bigcup^\uparrow_{i \in I} a_i)$ 。また、 $\beta \in \bigcup^\uparrow_{i \in I} a_i$ とする。仮定より $F(\bigcup^\uparrow_{i \in I} a_i) = \bigcup \{F(a_\circ) \mid a_\circ \subset \bigcup^\uparrow_{i \in I} a_i, \; a_\circ \; {\rm finite}\}$ なので、ある $\bigcup^\uparrow_{i \in I} a_i$ の有限部分集合 $a'_\circ$ が存在して $\beta \in F(a'_\circ)$ 。 $a'_\circ$ は $\bigcup^\uparrow_{i \in I} a_i$ の有限部分集合なので、ある有限個の $a_1, a_2, ..., a_k$ の和の部分集合となる。これらは有向なので、和集合 $a_l(l \in I)$ は存在する。 $a'_\circ \subset a_l$ なので単調性より $F(a'_\circ) \subset F(a_l)$ 。 $F(a_l) \subset \bigcup^\uparrow_{i \in I} F(a_i)$ なので $F(a'_\circ) \subset \bigcup^\uparrow_{i \in I} F(a_i)$ 。よって $F(\bigcup^\uparrow_{i \in I} a_i) \subset \bigcup^\uparrow_{i \in I} F(a_i)$ 。以上より $F(\bigcup^\uparrow_{i \in I} a_i) = \bigcup^\uparrow_{i \in I} F(a_i)$ 。

"Proof and Types"ではあまり詳しく書いていなくて、単調性なしで連続性と同値になるように読み取れるようなことが書いてあるのだが、単調性なしで良いのかどうかは分らなかった。まあまあまあ。「線形論理の誕生」では「有限呼び出し性」という同じような性質+単調性と連続性との同値性を証明していたので、それに倣った。とにかく、定義域のデータの有限近似さえ得られていれば安定関数は復元できるということが分る。

　続いて安定性について。これは圏論的に解釈すると自然だと書いてある。整合空間を $\subset$ を射とする圏と見ると、単調性は関手であることを表し、連続性はフィルター付き余極限というやつを表す。そして安定性は $a \subset a \cup b \supset b$ のプルバックの保存と同じことになる。まあ証明せずとも図を書いてみれば明らかでしょう。

　ドメインが整合空間であるという条件の有効性を表す例が挙げられている。我々は ${\mathcal Int}$ から ${\mathcal Int}$ へのどんな関数も安定関数で表現できるのであって欲しい。 ${\mathbb N}$ から ${\mathbb N}$ への関数 $f$ を $f(0) = f(1) = 0, \; f(n+2) = 1$ と定義する。これに対応する安定関数 $F$ は $F(\{0\}) = F(\{1\}) = \{0\}, \; F(\{n + 2\}) = \{1\}$ となる筈である。また、単調性より $F(\emptyset) = \emptyset$ とならなければならない。この時、 $F(\{0\} \cap \{1\}) = F(\emptyset) = \emptyset \neq F(\{0\}) \cap F(\{1\}) = \{0\}$ であるが、 $0$ と $1$ が整合でないこと、つまり $\{0\} \cup \{1\} = \{0, 1\} \in {\mathcal Int}$ から、安定性は侵されていないことになる。

　どんな関数も安定関数で表現できることは証明できるっぽい。

命題5：任意の ${\mathbb N}$ から ${\mathbb N}$ への関数 $f$ に対して、 $\{n\} \mapsto \{f(n)\}$ であるような安定関数 $F : {\mathcal Int} \to {\mathcal Int}$ が存在する。

証明： $F(\emptyset) = \emptyset, F(\{n\}) = \{f(n)\}$ としてこれが安定関数であることを確認すれば良い。

単調性： ${\mathcal Int}$ の要素 $a, a'$ が $a \subset a'$ となるのは $a = \emptyset$ の時だけだが、 $F(\emptyset) = \emptyset$ なので $F$ が単調性を満たすことは明らか。

連続性： ${\mathcal Int}$ の部分集合で有向集合となるのは $\{\emptyset, \{m\}\}$ という形のものだけであるが、この時 $\bigcup \{\emptyset, \{m\}\} = \{m\}$ で $F(\emptyset) = \emptyset$ なので、 $F(\bigcup \{\emptyset, \{m\}\}) = F(\{m\}) = \{f(m)\} = \bigcup \{\emptyset, \{f(m)\}\} = \bigcup \{F(\emptyset), F(\{m\})$ となり、連続性も満す。

安定性： $a \cup a'$ となるのは $a = \emptyset$ または $a' = \emptyset$ の時のみである。このとき $a \cap a' = \emptyset$ なので、 $F(a \cap a') = F(\emptyset) = \emptyset$ となる。 $F(a)$ と $F(a')$ もどちらかが $\emptyset$ になるので、 $F(a) \cap F(a') = \emptyset$ でもある。よって $F(a \cap a') = F(a) \cap F(a')$ で安定性も満す。