$\require{AMScd}$
双対的にみる余帰納法シリーズ
1. イントロ
2. 帰納法と代数
3. 余帰納法と余代数
はじめに
前回の記事では余帰納法の使い方について簡単に述べた．
余帰納法を定式化するときに，帰納法の双対として観ると非常に簡潔になる．そのため，本記事ではまず帰納法を圏論的視点から定式化する．
事前知識
- 圏論についての基本的なこと
- 圏や関手， 直積， 直和
- 帰納法についての知識
- 帰納的な関数定義
例： 自然数
自然数も帰納的データである．自然数のコンストラクターとして以下の2つがある．
\begin{eqnarray*}
0 &\in& \mathbb{N} \\
\mathrm{succ} &:& \mathbb{N} \to \mathbb{N}
\end{eqnarray*}
ここで0は終対象$1 = \{*\}$からの関数$0 : 1 \to \mathbb{N}$と見れる．こう見ると，$0$ と $\mathrm{succ}$ はコドメインが同じである．よって一つのコンストラクター $[0, \mathrm{succ}] : 1 + \mathbb{N} \to \mathbb{N}$ にまとめられる．
自然数上の帰納法によって $f : \mathbb{N} \to B$ を $b \in B$ と $g : B \to B$ を用いて定義できる．
\begin{eqnarray*}
f(0) &=& b \\
f(\mathrm{succ}(x)) &=& g(f(x))
\end{eqnarray*}
$b \in B$ を $b : 1 \to B$ として見ると次の等式と同値である．
\begin{eqnarray*}
f \circ 0 &=& b \\
f \circ \mathrm{succ} &=& g \circ f
\end{eqnarray*}
これは次の一つの等式にまとめられる．
$$ f \circ [0, \mathrm{succ}] = [b, g] \circ (1 + f) $$
可換図式で書けば次のようになる．
\begin{CD}
{1 + \mathbb{N}} @>{1 + f}>> {1+B} \\
@V{[0,\mathrm{succ}]}VV @VV{[b,g]}V \\
\mathbb{N} @>>f> B
\end{CD}
例： リスト
$A$ 上のリストの集合 $A^*$ のコンストラクターは以下の2つである．
\begin{eqnarray*}
\mathrm{nil} &\in& A^* \\
\mathrm{cons} &:& A \times A^* \to A^*
\end{eqnarray*}
自然数のときと同様に一つのコンストラクター $[\mathrm{nil}, \mathrm{cons}] : 1 + A \times A^* \to A^*$ にまとめられる．
リスト上の帰納法によって $f : A^* \to B$ を $b \in B$ と $g : A \times B \to B$ を用いて定義できる．
\begin{eqnarray*}
f(\mathrm{nil}) &=& b \\
f(\mathrm{cons}(x, l)) &=& g(x, f(l))
\end{eqnarray*}
これも一つの等式にまとめられる．
$$ f \circ [\mathrm{nil}, \mathrm{cons}] = [b, g] \circ (1 + A \times f) $$
可換図式で書けば次のようになる．
\begin{CD}
{1 + A \times A^*} @>{1 + A\times f}>> {1+A\times B} \\
@V{[\mathrm{nil},\mathrm{cons}]}VV @VV{[b,g]}V \\
A^* @>>f> B
\end{CD}
圏論的定式化
自然数の場合もリストの場合もコンストラクターのドメインは $\mathbb{N}$ や $A^*$ を含む式であり，コドメインはそれら単体のみである．よって，$A$のコンストラクターとはある自己関手 $F : \boldsymbol{C} \to \boldsymbol{C}$ を用いて $F(A) \to A$ となる射だと言える．
このアイディアをもとに帰納法を定式化できる．
F-代数
$\boldsymbol{C}$ を圏， $F : \boldsymbol{C} \to \boldsymbol{C}$ を関手とするとき，$F$-代数とは $\boldsymbol{C}$ の対象 $A$ と射 $\alpha : F(A) \to A$ の組 $(A, \alpha)$ のことである．
\begin{CD}
F(A) \\
@VV\alpha V \\
A
\end{CD}
$F_1(X) = 1+X$ のとき $(\mathbb{N}, [0, \mathrm{succ}])$ は $F_1$-代数の例である．
$F_2(X) = 1+A\times X$ のとき $(A^*, [\mathrm{nil}, \mathrm{cons}])$ は $F_2$-代数の例である．
F-準同型
$(A, \alpha)$ と $(B, \beta)$ を $F$-代数とする．$(A, \alpha)$ から $(B, \beta)$ への $F$-準同型とは $\boldsymbol{C}$ の射 $f : A \to B$ で以下の図を可換にするものである．
\begin{CD}
F(A) @>F(f)>> F(B) \\
@V\alpha VV @VV\beta V \\
A @>>f> B
\end{CD}
帰納法によって定義された関数はこの可換性を満たす．
F-代数の圏
$F$-準同型の合成は$F$-準同型である．すなわち， $f, g$ が $F$-準同型なら $g \circ f$ も$F$-準同型である．
これは以下の図が可換になることからわかる．
\begin{CD}
F(A) @>F(f)>> F(B) @>F(g)>> F(C)\\
@V\alpha VV @VV\beta V @VV\gamma V\\
A @>>f> B @>>g> C
\end{CD}
恒等射もあきらかに$F$-準同型である．
以上のことから$F$-代数は圏を成す．これを$\mathrm{Alg}(F)$と書く．
F-始代数
$\mathrm{Alg}(F)$の始対象を$F$-始代数と呼ぶ．
すなわち， $F$-代数 $(A, \alpha)$ が $F$-始代数とは $(A, \alpha)$ からの $F$-準同型が一意に存在することである．
このとき $F$-始代数は同型を除いて一意であることが始対象が同型を除いて一意であることからわかる．
また， $(A, \alpha)$ が $F$-始代数ならば $F(A) \cong A$ である．
(証明)． $(F(A), F(\alpha))$ は $F$-代数である． このとき， 以下の図を可換にする射 $i$ が唯一存在する．
\begin{CD}
F(A) @>F(i)>> F(F(A)) \\
@V\alpha VV @VF(\alpha)VV \\
A @>>i> F(A)
\end{CD}
この $i$ が $\alpha$ の逆射であることを示す． $\alpha \circ i$ は $(A, \alpha)$ の自己準同型であり， $(A, \alpha)$ は始対象でなので $\alpha \circ i = \mathrm{id}$ となる(以下の図を参照)．
\begin{CD}
F(A) @>F(i)>> F(F(A)) @>F(\alpha)>> F(A) \\
@V\alpha VV @VF(\alpha)VV @V\alpha VV \\
A @>>i> F(A) @>>\alpha > A
\end{CD}
次に$i \circ \alpha$を考える。
\begin{array}{lcl}
i \circ \alpha &=& F(\alpha) \circ F(i) \\
&=& F(\alpha \circ i) \\
&=& F(\mathrm{id}) \\
&=& \mathrm{id} \\
\end{array}
(証明終)
始代数から見る帰納法
自然数やリストは始代数である．リストについて着目すると，任意の $(B, [b, g] : 1+A\times B \to B)$ について，以下の図を可換にする $f : A^* \to B$ が一意に存在する．
\begin{CD}
{1 + A \times A^*} @>{1 + A\times f}>> {1+A\times B} \\
@V{[\mathrm{nil},\mathrm{cons}]}VV @VV{[b,g]}V \\
A^* @>>f> B
\end{CD}
これは $b, g$ を与えたときに関数 $f : A^* \to B$ を帰納的に定義することに対応している．
参考文献
- B. Jacobs and J.J.M.M. Rutten.
An introduction to (co)algebras and (co)induction.
In: Advanced topics in bisimulation and coinduction , pp. 38-99, 2011. (リンク)