論理計算と随伴関手(7) - エレファント・コンピューティング調査報告

論理プログラミングの「極限」は逆像として表すことができることがわかりましたが、逆像は「引き戻し」として表すことができるようです。「引き戻し」は「極限」で表すことができるのでここから考えていきます。

環の理論を使ってクライアント側の関数プログラミングの入出力をサーバー側で無限の時間実行されるプログラムの中に入れていくためのデザインパターンを作る、ということが今のところの目標ですが、この方向で良いのかどうかわかりませんし、できるのかどうかもよくわかりません。

ということで、圏論の極限について見ていきます。

極限の定義

(Wikipediaによる)
$F: J \rightarrow C$ を $C$ における形が $J$ の図式であるとします(これは関手 $F: J \rightarrow C$ のことを表します)。

$C$ の対象 $N$ と $J$ の対象 $X$ で添え字付けられた射の族 $\psi_X: N \rightarrow F(X)$ の組 $(N, ψ)$ が、全ての $J$ の射 $f: X \rightarrow Y$ が $F(f) \circ \psi_X = \psi_Y$ を満たすものを $F$ への錐と呼びます。
$\require{AMScd} \begin{CD} N @> id_N >> N \\ @V \psi_X VV @VV \psi_Y V \\ F(X) @>> F(f) > F(Y) \end{CD}$

$F$ への錐 $(L, \varphi)$ が、任意の $F$ への錐 $(N, \psi)$ に対して一意な射 $u : N \rightarrow L$ が存在して、 $J$ の全ての対象 $X$ が $\varphi_X \circ u = \psi_X$ を満たすとき、図式 $F: J \rightarrow C$ の極限と呼びます。
(斜めの線が書けないので可換図式を書くのは難しい)
$\begin{CD} N @> id_N >> N \\ @V \psi_X VV @VV \psi_Y V \\ F(X) @>> F(f) > F(Y) \end{CD} \begin{CD} N @> id_N >> N \\ @V u VV @VV u V \\ L @> id_L >> L \\ @V \varphi_X VV @VV \varphi_Y V \\ F(X) @>> F(f) > F(Y) \end{CD}$

引き戻し

(Wikipediaによる)
2つの射 $f: X \rightarrow Z$ と $g: Y \rightarrow Z$ に対して、以下の条件を満たす対象 $P$ と2つの射 $p_1: P \rightarrow X$ と $p_2: P \rightarrow Y$ の組を引き戻しと呼びます。

以下の可換図式が成り立ちます。

$\begin{CD} P @> p_2 >> Y \\ @V p_1 VV @VV g V \\ X @>> f > Z \end{CD}$

以下の左の図式が可換であるような $(Q, q_1, q_2)$ の組に対して $p_1 \circ u = q_1$ 、 $p_2 \circ u = q_2$ を満たす射 $u: Q \rightarrow P$ が一意的に存在します。

$\begin{CD} Q @> q_2 >> Y \\ @V q_1 VV @VV g V \\ X @>> f > Z \end{CD} \ \ \ \ \ \ \ \ \begin{CD} Q @> id_Q >> Q @> id_Q >> Q \\ @V id_Q VV @V u VV @VV q_2 V \\ Q @> u >> P @> p_2 >> Y \\ @V id_Q VV @V p_1 VV @VV g V \\ Q @>> q_1 > X @>> f > Z \end{CD}$

これを極限の定義を使って書いてみます。圏 $J$ を以下のようなものとします。すなわち対象 $X'$ 、 $Y'$ 、 $Z'$ と射 $f': X' \rightarrow Z'$ 、 $g': Y' \rightarrow Z'$ と恒等射からなる圏とします。
$\begin{CD} @. Y' \\ @. @VV g' V \\ X' @>> f' > Z' \end{CD}$
図式(関手) $F: J \rightarrow C$ により、以上のものに対応する先の圏 $C$ の対象と射を $X$ 、 $Y$ 、 $Z$ 、 $f: X \rightarrow Z$ 、 $g: Y \rightarrow Z$ とします。
$\begin{CD} @. Y \\ @. @VV g V \\ X @>> f > Z \end{CD}$

図式 $F$ への錐は以下の図式が可換となる対象 $N$ と射 $\psi_{X'}$ 、 $\psi_{Y'}$ 、 $\psi_{Z'}$ の組となります。
$\require{AMScd} \begin{CD} N @> id_N >> N \\ @V \psi_{X'} VV @VV \psi_{Z'} V \\ X @>> f > Z \end{CD} \ \ \ \ \ \ \ \ \begin{CD} N @> id_N >> N \\ @V \psi_{Y'} VV @VV \psi_{Z'} V \\ Y @>> g > Z \end{CD}$
$\psi_{Z'}$ は他のもので表すことができるので省略すると、以下の可換図式が成り立つものということになります。
$\begin{CD} N @> \psi_{Y'} >> Y \\ @V \psi_{X'} VV @VV g V \\ X @>> f > Z \end{CD}$
図式 $F$ への錐 $(P, \varphi)$ は以下の可換図式を満たすものです。
$\begin{CD} P @> \varphi_{Y'} >> Y \\ @V \varphi_{X'} VV @VV g V \\ X @>> f > Z \end{CD}$
図式 $F$ への錐 $(P, \varphi)$ が以下の条件を満たすとき図式 $F: J \rightarrow C$ の極限となります。

任意の $F$ への錐 $(Q, \psi)$ に対して、 $J$ の全ての対象 $j$ が $\varphi_j \circ u = \psi_j$ を満たす一意な射 $u : Q \rightarrow P$ が存在します。

$\begin{CD} Q @> \psi_{Y'} >> Y \\ @V \psi_{X'} VV @VV g V \\ X @>> f > Z \end{CD} \ \ \ \ \ \ \ \ \begin{CD} Q @> id_Q >> Q @> id_Q >> Q \\ @V id_Q VV @V u VV @VV \psi_{Y'} V \\ Q @> u >> P @> \varphi_{Y'} >> Y \\ @V id_Q VV @V \varphi_{X'} VV @VV g V \\ Q @>> \psi_{X'} > X @>> f > Z \end{CD}$
$(P, \varphi_{X'}, \varphi_{Y'})$ は2つの射 $f: X \rightarrow Z$ と $g: Y \rightarrow Z$ に対する引き戻しになっています。