定理 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$ から一つずつ近似値を選んで出来た列全ての集合。
[注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}$ となる。逆の合成も同様。
No comments:
Post a Comment