$\require{AMScd}$
双対的にみる余帰納法シリーズ

イントロ
帰納法と代数
余帰納法と余代数

はじめに

前回の記事では帰納法を圏論的に定式化した．

今回の記事では帰納法の双対をとることによって余帰納法を定式化できることを見る．その後，余帰納法の使用例をいくつか見ていく．

事前知識

圏論についての基本的なこと
- 圏や関手，直積，直和
帰納法についての知識
- 帰納的な関数定義

例：無限リスト

余帰納的なデータの代表例は無限リストである．
$A$上の無限リストの集合を $A^\infty$ とすると，$A^\infty$ のデストラクターとして$\mathrm{head}, \mathrm{tail}$があることをイントロの記事で述べた．

\begin{eqnarray*}
\mathrm{head} &:& A^\infty \to A \\
\mathrm{tail} &:& A^\infty \to A^\infty
\end{eqnarray*}

$\mathrm{head}$と$\mathrm{tail}$をみると，始域が同じである．つまり，一つのデストラクター $\langle \mathrm{head}, \mathrm{tail} \rangle : A^\infty \to A \times A^\infty$ にまとめられる．

$A^\infty$上の余帰納法として，関数 $f : B \to A^\infty$ を $h : B \to A$ と $g : B \to B$ と用いて余帰納的に定義できるのだった．

\begin{eqnarray*}
\mathrm{head}(f(b)) &=& h(b) \\
\mathrm{tail}(f(b)) &=& f(g(b))
\end{eqnarray*}

これは次の等式と同じである．

\begin{eqnarray*}
\mathrm{head} \circ f &=& h \\
\mathrm{tail} \circ f &=& f \circ g
\end{eqnarray*}

また，一つの等式にまとめられる．

\begin{equation*}
\langle \mathrm{head}, \mathrm{tail} \rangle \circ f = (A \times f) \circ \langle h, g \rangle
\end{equation*}

可換図式で書けば次のようになる．

\begin{CD}
  {B} @>{f}>> {A^\infty} \\
  @V{\langle h, g \rangle}VV        @VV{\langle \mathrm{head}, \mathrm{tail} \rangle}V \\
  {A\times B}    @>>{A\times f}>    {A\times A^\infty}
\end{CD}

圏論的定式化

ここで，デストラクターのドメインは$A^\infty$であり，コドメインは$A^\infty$を含む式である．よって，$A$のデストラクターとはある自己関手 $F : \mathbf{C} \to \mathbf{C}$ を用いて $A \to F(A)$ となる射だと言える．

ここで，$A$のコンストラクターとは $F(A) \to A$ なる射だったことを思いだせば，デストラクターとコンストラクターが双対になっていることがわかる．よって，帰納法を定式化する際に用いた概念の双対を取れば余帰納法が定式化できることが推察できる．

F-余代数

$\mathbf{C}$を圏，$F : \mathbf{C} \to \mathbf{C}$を関手とするとき，$F$-余代数とは $\mathbf{C}$ の対象 $A$ と射 $\alpha : A \to F(A)$ の組 $(A, \alpha)$ である．

\begin{CD}
A \\
@VV\alpha V \\
F(A)
\end{CD}

$F(X) = A\times X$ のとき，$(A^\infty, \langle \mathrm{head}, \mathrm{tail} \rangle)$ は $F$-余代数の例である．

F-余準同型

$(A, \alpha)$ と $(B, \beta)$ を $F$-余代数とする．$(A, \alpha)$ から $(B, \beta)$ への $F$-余準同型とは $\mathbf{C}$ の射 $f : A \to B$ で以下の図を可換にするものである．

\begin{CD}
  A @>f>> B \\
  @V\alpha VV        @VV\beta V \\
  F(A)   @>>F(f)>    F(B)
\end{CD}

余帰納法によって定義された関数はこの可換性を満たす．

F-余代数の圏

$F$-余準同型の合成は$F$-準同型である．すなわち， $f, g$ が $F$-準同型なら $g \circ f$ も$F$-余準同型である．
これは以下の図が可換になることからわかる．

\begin{CD}
  A @>f>> B @>g>> C\\
  @V\alpha VV        @VV\beta V  @VV\gamma V\\
  F(A)   @>>F(f)>    F(B) @>>F(g)> F(C)
\end{CD}

恒等射もあきらかに$F$-余準同型である．

以上のことから$F$-余代数は圏を成す．これを$\mathrm{Coalg}(F)$と書く．

F-終余代数

$\mathrm{Coalg}(F)$の終対象を$F$-終余代数と呼ぶ．
すなわち， $F$-余代数 $(A, \alpha)$ が $F$-終余代数とは $(A, \alpha)$ への $F$-余準同型が一意に存在することである．

このとき $F$-終余代数は同型を除いて一意であることが終対象が同型を除いて一意であることからわかる．

また， $(A, \alpha)$ が $F$-終余代数ならば $A \cong F(A)$ である．証明は $F$-始代数の場合の双対なので省略する．

終余代数からみる余帰納法

無限リストは終余代数である．すなわち，任意の $(B, \langle h, g \rangle : B \to A\times B)$ について以下の図を可換にする $f : B \to A^\infty$ が一意に存在する．

\begin{CD}
  {B} @>{f}>> {A^\infty} \\
  @V{\langle h, g \rangle}VV        @VV{\langle \mathrm{head}, \mathrm{tail} \rangle}V \\
  {A\times B}    @>>{A\times f}>    {A\times A^\infty}
\end{CD}

(証明)．$A^\infty = \{ i : \mathbb{N} \to A \}$ だったことを思い出そう．つまり，任意の$b \in B$ について $f(b) : \mathbb{N} \to A$ を定義すればよい．ここで $f(b) : \mathbb{N} \to A$ を次のように帰納的に定義する．

\begin{eqnarray*}
f(b)(0) &=& h(b) \\
f(b)(n+1) &=& f(g(b))(n)
\end{eqnarray*}

このように定義された $f : B \to A^\infty$ が可換図式を満たすことを示す．
それには次の2つの等式を示せばよい．

\begin{eqnarray*}
\mathrm{head} \circ f &=& h \\
\mathrm{tail} \circ f &=& f \circ g
\end{eqnarray*}

任意の$b \in B$について，

\begin{eqnarray*}
\mathrm{head} \circ f (b)
&=& \mathrm{head}(f(b)) \\
&=& f(b)(0) \\
&=& h(b)
\end{eqnarray*}

となり，$\mathrm{head}\circ f = h$である．また，任意の$n \in \mathbb{N}$について

\begin{eqnarray*}
(\mathrm{tail} \circ f (b)) (n)
&=&  \mathrm{tail}(f(b))(n) \\
&=& f(b)(n+1) \\
&=& f(g(b))(n)
\end{eqnarray*}

より，$\mathrm{tail} \circ f (b) = f(g(b))$ であり，$\mathrm{tail} \circ f = f \circ g$ が分かる．
以上より，$f$の存在は言えた．次に一意性を示す．

$f : B \to A^\infty$が可換図式を満たすとする．このとき，

\begin{eqnarray*}
\mathrm{head} \circ f &=& h \\
\mathrm{tail} \circ f &=& f \circ g
\end{eqnarray*}

なので，任意の$b \in B$ と $n \in \mathbb{N}$ について次の等式が成り立つ．

\begin{eqnarray*}
f(b)(0) &=& h(b) \\
f(b)(n+1) &=& f(g(b))(n)
\end{eqnarray*}

よって，帰納的に $f$ が一意であることが言える．(証明終了)

余帰納法の例

関数 $\mathrm{even} : A^\infty \to A^\infty$ を次の可換図式を満たすものとする．

\begin{CD}
  {A^\infty} @>{\mathrm{even}}>> {A^\infty} \\
  @V{\langle \mathrm{head}, \mathrm{tail}\circ\mathrm{tail} \rangle}VV        @VV{\langle \mathrm{head}, \mathrm{tail} \rangle}V \\
  {A\times A^\infty}    @>>{A\times \mathrm{even}}>    {A\times A^\infty}
\end{CD}

これは $\mathrm{even}(\alpha)(n) = \alpha(2n)$ という定義と同じである．
$\mathrm{odd} : A^\infty \to A^\infty$ を $\mathrm{odd} = \mathrm{even}\circ \mathrm{tail}$ と定義する．

$\mathrm{merge} : A^\infty\times A^\infty \to A^\infty$ を次の可換図式を満たすものとする．

\begin{CD}
  {A^\infty\times A^\infty} @>{\mathrm{merge}}>> {A^\infty} \\
  @V{\langle \mathrm{head}\circ\pi_1, \langle \pi_2, \mathrm{tail}\circ\pi_1 \rangle \rangle}VV        @VV{\langle \mathrm{head}, \mathrm{tail} \rangle}V \\
  {A\times (A^\infty\times A^\infty)}    @>>{A\times \mathrm{merge}}>    {A\times A^\infty}
\end{CD}

これは次の定義と同じである．

\begin{equation*}
\mathrm{merge}(\alpha, \beta)(n) = \begin{cases}
\alpha(m) & (n = 2m) \\
\beta(m) & (n = 2m + 1)
\end{cases}
\end{equation*}

このとき，
$$ \mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha)) = \alpha $$
すなわち，
$$ \mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle = \mathrm{id} $$
を示そう．

ここで，$\mathrm{id} : A^\infty \to A^\infty$ が$A^\infty$から自身への唯一の余準同型であることに注意する．
すると，左辺が$A^\infty$から自身への余準同型であることを示せば等式が終余代数の定義から従う．
つまり，次の等式を示せばよい．

\begin{eqnarray*}
\mathrm{head}\circ\mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle &=& \mathrm{head} \\
\mathrm{tail}\circ\mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle &=& \mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle \circ \mathrm{tail}
\end{eqnarray*}

実際に計算すると

\begin{eqnarray*}
\mathrm{head}\circ\mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle 
&=& \mathrm{head}\circ\pi_1 \circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{head} \circ \mathrm{even} \circ \pi_1 \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{head} \circ \mathrm{even} \circ \mathrm{id} \\
&=& \mathrm{head} \circ \mathrm{even} \\
&=& \mathrm{head}
\end{eqnarray*}

\begin{eqnarray*}
\mathrm{tail}\circ\mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle 
&=& \mathrm{merge} \circ \langle \pi_2, \mathrm{tail}\circ\pi_1 \rangle \circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge} \circ \langle \mathrm{odd} \circ \pi_2 , \mathrm{tail}\circ\mathrm{even}\circ\pi_1 \rangle \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge} \circ \langle \mathrm{even} \circ \mathrm{tail} \circ \pi_2 , \mathrm{even}\circ\mathrm{tail}\circ\mathrm{tail}\circ\pi_1 \rangle \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge} \circ \langle \mathrm{even} \circ \mathrm{tail} \circ \pi_2 , \mathrm{odd}\circ\mathrm{tail}\circ\pi_1 \rangle \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge} \circ ( \mathrm{even} \circ \mathrm{tail} \times \mathrm{odd}\circ\mathrm{tail}) \circ \langle \pi_2, \pi_1 \rangle \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge} \circ ( \mathrm{even} \times \mathrm{odd}) \circ (\mathrm{tail} \times \mathrm{tail}) \circ \langle \mathrm{id}, \mathrm{id} \rangle \\
&=& \mathrm{merge}\circ (\mathrm{even} \times \mathrm{odd}) \circ \langle \mathrm{id}, \mathrm{id} \rangle \circ \mathrm{tail}
\end{eqnarray*}

となり，等式が示される．

参考文献

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. (リンク)