ガチ勢になるための圏論勉強会 第二回 まとめ

ガチ勢になるための圏論勉強会第二回で読んだ、A.Pitts の Relational Properties of Domains の定理 3.3 の証明のまとめ。これが有名な "inverse limit construction" なのだろう。多分。定理の背景は論文か第一回のまとめ参照。


定理 3.3: 局所連続な関手 $F : \mathbf{Cpo}^\text{op}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ は常に最小不変性、つまり $i : F(D,D) \cong D$ で $\operatorname{fix}(\lambda f.\ i\circ F(f,f) \circ i^{-1}) = \operatorname{id}$ となるような $i$, $D$ を持つ。

証明:
まず $$\begin{align*} f^\circ\circ f &= \operatorname{id} \\ f \circ f^\circ &\sqsubseteq \operatorname{id} \end{align*}$$ となるような $f^\circ$ が存在する時、$f$ は埋め込みであると言い、$f^\circ$ はそれに対応する射影と呼ぶ。$f$ が決まると、それに対応する $f^\circ$ は高々一つしか無い。論文では証明されていないが、勉強会では次のように証明した。仮に射影の条件を満たす別の関数 $g$があったとする。
$$\begin{align*} g\circ f &= \operatorname{id} \\ f \circ g &\sqsubseteq \operatorname{id} \end{align*}$$ すると
$$\begin{align*} f^\circ &= g \circ f \circ f^\circ & \ \ (\because g \circ f = \operatorname{id}) \\ &\sqsubseteq g & \ \ (\because f\circ f^\circ \sqsubseteq \operatorname{id}) \end{align*}$$ で、
$$\begin{align*} g &= f^\circ \circ f \circ g & \ \ (\because f^\circ \circ f = \operatorname{id}) \\ &\sqsubseteq f^\circ & \ \ (\because f\circ g \sqsubseteq \operatorname{id}) \end{align*}$$ なので $g = f^\circ$ となり、$f$ に対応する射影は無二であることが分かる。関数合成が単調である事の証明は省く。[注1] 論文では書かれていないが、逆に射影が決まると埋め込みが (最大) 一つに決まる。証明は同様。

この埋め込み←→射影の対応を使って次のような双方向の鎖を作る。[注2]
$$\begin{equation}\label{eq:chain} D_0 \underset{\underset{i_0^\circ}{\leftharpoondown}}{\overset{i_0}{\rightharpoonup}} D_1 \underset{\underset{i_1^\circ}{\leftharpoondown}}{\overset{i_1}{\rightharpoonup}} D_2 \underset{\underset{i_2^\circ}{\leftharpoondown}}{\overset{i_2}{\rightharpoonup}} \cdots \end{equation}$$ where
$$\begin{align*} D_0 &= \varnothing_\bot \\ D_{n+1} &= F(D_n, D_n) \\ i_0 &= \bot_{\varnothing_\bot \rightarrow D_1} \\ i_{n+1} &= F(i_n^\circ, i_n) \end{align*}$$ この鎖の極限 (直観的に言えば鎖を無限に右に辿って行き着く対象) が、定理の主張している $D$ になる。この鎖の構成は (反変と共変、二種類の引数に対応する為 $-^\circ$ を駆使していることを除けば) 単純に $F$ を $\bot$ な対象と $\bot$ な射に繰り返し適用しているだけなので、その極限が不動点になるというのはそれほど不思議な事ではない。

この事を厳密に論証するには $D$ を天下り的に与えてそれが圏論的な極限になっていることを示す (Pitts は余極限としているが、どちらでも論証できる)。その上で元の鎖を $F$ で写した新たな鎖
$$F\,(D_0,D_0) \underset{\underset{F\,(i_0, i_0^\circ)}{\leftharpoondown}}{\overset{F\,(i_0^\circ,i_0)}{\rightharpoonup}} F\,(D_1,D_1) \underset{\underset{F\,(i_1, i_1^\circ)}{\leftharpoondown}}{\overset{F\,(i_1^\circ,i_1)}{\rightharpoonup}} F\,(D_2,D_2) \underset{\underset{F\,(i_2, i_2^\circ)}{\leftharpoondown}}{\overset{F\,(i_2^\circ,i_2)}{\rightharpoonup}} \cdots$$ を考える。これは、元の鎖の定義を見れば分かるように単に $\eqref{eq:chain}$ から $D_0$ を省いて得られる
$$\begin{equation} D_1 \underset{\underset{i_1^\circ}{\leftharpoondown}}{\overset{i_1}{\rightharpoonup}} D_2 \underset{\underset{i_2^\circ}{\leftharpoondown}}{\overset{i_2}{\rightharpoonup}} \cdots \label{eq:chain2} \end{equation}$$ と同じなので、元の鎖と同じ極限を持つはずである (up to iso)。この同一性を立証する同型射が $i$ になる。

まず天下り的に
$$D = \left\{x \in D_n : \forall n.\ x_n = i_n^\circ\,x_{n+1}  \right\}$$ とする。直観的には例えば無限リスト [1..] の表示はそれの有限な近似の列 $(\bot, (1:\bot), (1:1:\bot), \ldots) \in D$ と同一視するという事らしい。コーシー列で実数を構成するのに似ている。$D_n$ の鎖では右に行くほど $F$ の適用回数が増える (= より深いデータ構造が定義される) ので、より深くまで定義された近似値が拾ってこれる。$x_n = i_n^\circ\,x_{n+1}$ という制約は例えば $(\bot, (1:\bot), (2:3:\bot), (1:5:3\bot))$ のように互いに近似関係にないデータをそれぞれの $D_n$ から拾ってくるのを禁止している。

$$\begin{gather*}\pi_n  : D \rightarrow D_n \\ \pi_n\,(x_0, x_1, \ldots, x_n, \ldots) = x_n \end{gather*}$$ という射影は次のような埋め込みと対応する (i.e. $j_n^\circ = \pi_n$)。
$$\begin{gather*} j_n : D_n \rightarrow D \\ j_n\,x_n =  (\ldots, i^\circ_{n-2}\,(i^\circ_{n-1}\,x_n), i^\circ_{n-1}\,x_n, x_n, i_n\,x_n, i_{n+1}\,(i_n\,x_n), \ldots) \end{gather*}$$ $j_n$ は $(x_0,x_1, \ldots, x_n, \ldots)$ から $x_n$ だけ与えられたら、「$x_n$ より左は $i_k^\circ$ で要素を復元し、$x_n$ 右は $i_k$ で復元する」という手法でできるだけ元の列を復元する。$D$ の定義より左に行く時の復元は完璧な復元だが、右に行く時の復元は元のデータより ($\sqsubseteq$ で) 小さい。つまり $j_n$ は元の列を $n$ 個目まで完璧に復元するので、上限を取ると完全な逆関数になることが予想される。この予想は、下の補題の後に実際に証明する。

$D$ が $\eqref{eq:chain2}$ の鎖の極限であるとは、任意の $D'$ と $\pi_n' : D' \rightarrow D_n$ に対して、$\forall n.\ \pi_n' = i_n^\circ \circ \pi_{n+1}'$ が成り立つならば $\forall n.\ \pi_n \circ k = \pi_n'$ となる $k : D' \rightarrow D$ がただ一つ存在することである。これを示すために一つ補題を証明しておく。

補題:
$\forall n.\ \pi_n' = i_n^\circ \circ \pi_{n+1}'$ となるような $D'$ と $\pi_n'$ が与えられた時、$j_n \circ \pi_n'$ は上昇列であって
$$\pi_m \circ \bigsqcup_n j_n \circ \pi_n' = \pi_m'$$ となる。これは $D' = D, \pi_n' = \pi_n$ の場合でも成り立つ。


証明:
この証明の概要は輪講担当者の奥村がこのカンペから拾ってきた。まず
$$\begin{equation}\label{eq:pi_expand} \pi_n =  i_n^\circ \circ \pi_{n+1} \hspace{4ex} \pi_n' =  i_n^\circ \circ \pi_{n+1}' \hspace{4ex} j_n = j_{n+1} \circ i_n\end{equation}$$ である。これらを利用すると
$$\begin{align*} j_n \circ \pi_n' &=  j_{n+1}\circ i_n \circ i_n^\circ \circ \pi_{n+1} \\ &\sqsubseteq j_{n+1} \circ \pi_{n+1} & (\because i_n \circ i_n^\circ \sqsubseteq \operatorname{id}) \end{align*}$$ つまり $j_n \circ \pi_n'$ が上昇列であることが分かり、さらに、$m \le n$ ならば
$$\begin{align} \pi_m \circ j_n \circ \pi_n' &= i_m \circ i_{m+1} \circ \cdots \circ i_{n-1} \circ \pi_{n} \circ j_n \circ \pi_n' & \notag \\ &= i_m \circ i_{m+1} \circ \cdots \circ i_{n-1} \circ \pi_n' \notag \\ &= \pi_m' \label{eq:pi_j_pi} \end{align}$$ となる事も分かる。従って、任意の $m$ について
$$\begin{align*} \pi_m \circ \bigsqcup \{j_n \circ \pi_n' : n \ge 0\} &= \pi_m \circ \bigsqcup \{j_n \circ \pi_n' : n \ge m\}  & (j_n \circ \pi_n' \text{は上昇列だから}) \\ &= \bigsqcup \{\pi_m \circ j_n \circ \pi_n' : n \ge m \} \\ &= \bigsqcup \{\pi_m' : n \ge m\} & \text{\eqref{eq:pi_j_pi} より} \\ &= \bigsqcup \{\pi_m'\} = \pi_m' \end{align*}$$ となる。
(補題終わり)

ここで $k = \bigsqcup_n j_n \circ \pi_n'$ とする。補題によりこれは well-defined であり、しかも全ての $n$ について
$$\pi_n \circ k =  \pi_n \circ \bigsqcup_m j_m \circ \pi_m' = \pi_n'$$ である。従って、条件を満たす $k$ が最低一つは存在する。逆に $\forall n.\ \pi_n \circ k =  \pi_n'$ が成り立つならば、
$$\begin{equation}\label{eq:pi_k_j_pi} j_n\circ \pi_n \circ k = j_n \circ \pi_n' \end{equation}$$ である。補題により右辺が上昇列なので両辺が上昇列となり、上限を取ることが出来る。補題で $D' = D$ とするとどの $n$ についても $\forall n.\ \pi_n \circ \bigsqcup_m j_m \circ \pi_m = \pi_n$ つまり
$$\pi_n \left(\left(\bigsqcup_m j_m \circ \pi_m\right)\,(x_0,x_1,\ldots)\right) = \pi_n (x_0,x_1,\ldots) = x_n$$
なので、$\bigsqcup_m j_m \circ \pi_m = \operatorname{id}$。従って、$\eqref{eq:pi_k_j_pi}$ の両辺の上限を取ると
$$k = \operatorname{id} \circ k = \bigsqcup_n j_n \circ \pi_n \circ k = \bigsqcup_n j_n \circ \pi_n'$$ となり、条件を満たす $k$ は一意であることが示せた。よって $D$ は $\eqref{eq:chain2}$ の極限である。

論文にもある通り、上記の論証は $i_n$ や $j_n$ の性質の内、$F$ が保存するものしか使っていないので $F(D,D)$ は
$$F\,(D_0,D_0) \underset{\underset{F\,(i_0, i_0^\circ)}{\leftharpoondown}}{\overset{F\,(i_0^\circ,i_0)}{\rightharpoonup}} F\,(D_1,D_1) \underset{\underset{F\,(i_1, i_1^\circ)}{\leftharpoondown}}{\overset{F\,(i_1^\circ,i_1)}{\rightharpoonup}} F\,(D_2,D_2) \underset{\underset{F\,(i_2, i_2^\circ)}{\leftharpoondown}}{\overset{F\,(i_2^\circ,i_2)}{\rightharpoonup}} \cdots$$ の極限である。しかしこの鎖はそのまま $\eqref{eq:chain2}$ の鎖なので、$D$ も $F(D,D)$ も同じ鎖 $\eqref{eq:chain2}$ の極限である。極限は一意なので $i : F(D,D) \cong D$ が存在し、この同型射は $D' = F(D,D)$ と置いた時の $k$ と一致する。[注3]

したがって、
$$F(j_n, \pi_n)\circ i^{-1} = F(j_n, \pi_n) \circ k = \pi_n$$ (論文は極限ではなく余極限を使っているので $F$ の引数と $i$ の位置が左右逆になっている。今更直すのは面倒なのでこのままにする。)となり、簡単な記号操作で
$$\forall n.\ j_{n+1} \circ \pi_{n+1} = i\circ F(j_n \circ \pi_n, j_n\circ \pi_n)\circ i^{-1}$$ が示せる。ここで $j_0 \circ \pi_0 = \bot$ なので
$$\operatorname{id} = \bigsqcup_n j_n \pi_n = \bigsqcup_n \delta^n\,\bot = \operatorname{fix}\,\delta$$ (ただし $\delta\,  f = \ i\circ F(f, f)\circ i^{-1}$) となり $i, D$ は最小であることが示せた。

三行まとめ

• 最小不動点 $i,D$ は $F$ を⊥な対象と⊥な関数に繰り返し適用した領域 $D_n$ の極限として得る。
• $F$ を繰り返して適用して出てきた射は $D_n \rightarrow D_{n+1}$ の埋め込みになるため、逆向きの射を射影という形で求められるので profunctor の $F$ を繰り返し適用できる。
• 極限 $D$ は $D_n$ から一つずつ近似値を選んで出来た列全ての集合。

次回は 定理 3.4 から。

[注1] 因みに $f^\circ$ を陽に与えることも出来る。
$$f^\circ\,x = \max\{y : f\,y \sqsubseteq x\}$$ $\max$ は当然存在すれば一意であり、存在しないならば $f$ は埋め込みではない。これが射影になることの証明は読者への課ｄ(ry
この事を利用すると、埋め込みではない関数の例が簡単に見つけられる。例えば
$$\begin{align*} f : &\text{Bool}_\bot \rightarrow \text{()} \times \text{()} \\ f\,\text{True} &= (\text{()}, \bot) \\ f\,\text{False} &= (\bot, \text{()}) \\ f\,\bot &= (\bot, \bot) \end{align*}$$ は $\max\{ y: f\,y \sqsubseteq (\text{()}, \text{()})\}$ が存在しないので射影を持たない。

[注2] この鎖が well-defined であるには、全ての $n$ について $i_n^\circ$ が定義されている、つまり $i_n$ が埋め込みである必要がある。まず $\bot : \varnothing_\bot \rightarrow F\,(\varnothing_\bot, \varnothing_\bot)$ が埋め込みである事は容易に分かる。また、任意の埋め込み $f$ について $F(f^\circ, f)$ も埋め込みであり、$(F\,(f^\circ, f))^\circ = F\,(f, f^\circ)$ となる:
$$\begin{align*} F\,(f^\circ, f)\circ F\,(f,f^\circ) &= F\,((f^\circ, f) \circ (f, f^\circ)) & (\text{関手は合成を保存}) \\ &= F\,(f\circ f^\circ, f \circ f^\circ) & (\text{積圏での合成の定義}) \\ &\sqsubseteq F\,(\operatorname{id}, \operatorname{id}) & (F\text{は単調}) \\ &= \operatorname{id} & (\text{関手はidを保存}) \end{align*}$$ 二行目では、左成分は反変なので合成した関数の左右が逆になる事に注意。逆の合成も同様にして $\operatorname{id}$ になることが示せる。したがって、$n$ についての帰納法で $i_n$ も埋め込みであることが分かる。

[注3]$k$ は $D$ と $D'$ によって変化するので、それぞれ区別をつけるため $k_{D' \Rightarrow D} : D' \rightarrow D$ と表記することにする。$D$ も $F(D,D)$ も極限なので $k_{D \Rightarrow F(D,D)}$ と $k_{F(D,D) \Rightarrow D}$ が存在する。これらの合成、例えば $k_{D \Rightarrow F(D,D)} \circ k_{F(D,D) \Rightarrow D}$ は $k_{D \Rightarrow D}$ の条件を満たすので $k_{D \Rightarrow D}$ と一致しなくてはならない。しかし $\operatorname{id}$ もまた $k_{D \Rightarrow D}$ の条件を満たすので $k_{D \Rightarrow F(D,D)} \circ k_{F(D,D) \Rightarrow D} = \operatorname{id}$ となる。逆の合成も同様。