双対的にみる余帰納法シリーズ
- イントロ
2. 帰納法と代数
3. 余帰納法と余代数
はじめに
帰納法について圏論的な見方を解説した日本語のWebページはそれなりにあるが， 余帰納法についてはみかけない． しかし， Haskellで使われる無限リストは余帰納的なデータの代表例であり， 余帰納法の解説にはある程度の意味があると信じて本記事を書く．
帰納法は知っているけど， 余帰納法って何? という読者が大半かと思われるので， まず本記事では余帰納法の使い方に焦点を当てて余帰納法への導入を行なう． その後， 余帰納法が帰納法の双対になっていることや， 余帰納的な証明手法であるBisimulationについていくつかの記事に分けて解説する(予定)．
事前知識
読者が以下のことを知っていることを前提に以降の記事を書く．
- 圏論についての基本的なこと
- 圏や関手， 直積， 直和
- 帰納法についての知識
- 帰納的な関数定義
(本記事では圏論の知識は使わない)
帰納的データ， 帰納法
帰納的データの代表的な例としてリストがある．
集合$A$上のリストの集合を$A^*$とすると， $A^*$のコンストラクターとして以下のものを考えられる．
\begin{eqnarray*}
\mathrm{nil} &\in& A^* \\
\mathrm{cons} &:& A \times A^* \to A^*
\end{eqnarray*}
また， $A^*$上の帰納法として$A^*$からの関数を$\mathrm{nil}, \mathrm{cons}$を用いて帰納的に関数を定義できる． すなわち， 関数 $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*}
Haskellでのコードで表わすと以下のようになる．
f [] = b
f (x:xs) = g x (f xs)
余帰納的データ， 余帰納法
余帰納的データの代表例として， 無限リストがある．
まず， 無限リストがどのような構造を持っているかを考えよう． 無限リストは値の無限列だと考えることができる． すなわち， 無限リストは0番目の値， 1番目の値， 2番目の値， … と無限の要素を持っている． 以上のことから無限リストとは$\mathbb{N}$からの関数だと考えてよさそうだ．
よって， 集合$A$上の無限リストの集合$A^\infty$を次で定義する．
$$
A^\infty = \{ f : \mathbb{N} \to A \}
$$
集合$A^\infty$上の関数として以下のものを考えられる．
\begin{eqnarray*}
\mathrm{head}&& : A^\infty \to A \\
\mathrm{head}&&(\alpha) = \alpha(0) \\
\mathrm{tail}&& : A^\infty \to A^\infty \\
\mathrm{tail}&&(\alpha) = \alpha^+ \quad\quad (\alpha^+(n) = \alpha(n+1))
\end{eqnarray*}
実は無限リスト$\alpha$について次の関係が成り立つ． ここで， $f^{(n)}$ は $f$ の $n$ 回適用を表わす．
\begin{eqnarray*}
\alpha(0) &=& \mathrm{head}(\alpha) \\
\alpha(1) &=& \mathrm{head}(\mathrm{tail}(\alpha)) \\
\alpha(2) &=& \mathrm{head}(\mathrm{tail}^{(2)}(\alpha)) \\
&\vdots& \\
\alpha(n) &=& \mathrm{head}(\mathrm{tail}^{(n)}(\alpha)) \\
&\vdots&
\end{eqnarray*}
このことから $\mathrm{head}, \mathrm{tail}$ は無限リストを特徴付けていると言える． よって， $\mathrm{head}, \mathrm{tail}$ をコンストラクターに対応してデストラクターと呼ぼう．
$A^\infty$ 上の余帰納法として， $A^\infty$ への関数を$\mathrm{head}, \mathrm{tail}$を用いて余帰納的に定義できる． すなわち， 関数 $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*}
Haskellではこの記法をサポートしていないため， 直接書くことはできないが同様のことを unfoldr :: (b -> Maybe (a, b)) -> b -> [a] で実現できる．
f = unfoldr (\b -> Just (h(b), g(b)))
ここで， 以下の双対性があることに注意しよう．
- コンストラクター $\longleftrightarrow$ デストラクター
- $A^*$ からの関数 $\longleftrightarrow$ $A^\infty$ への関数
本記事では詳細に述べないが， 後続の記事ではこの双対性に焦点を当てて解説する．
余帰納的定義の例
次のような関数 $\mathrm{even} : A^\infty \to A^\infty$ を考える．
$$ \mathrm{even}(\alpha)(n) = \alpha(2n) $$
これは次の等式で余帰納的に定義できる．
\begin{eqnarray*}
\mathrm{head}(\mathrm{even}(\alpha)) &=& \mathrm{head}(\alpha) \\
\mathrm{tail}(\mathrm{even}(\alpha)) &=& \mathrm{even}(\mathrm{tail}(\mathrm{tail}(\alpha)))
\end{eqnarray*}
この定義のもと， 次の関係が成り立つ．
\begin{eqnarray*}
\mathrm{even}(\alpha)(0) &=& \mathrm{head}(\mathrm{even}(\alpha)) &=& \mathrm{head}(\alpha) &=& \alpha(0) \\
\mathrm{even}(\alpha)(1) &=& \mathrm{head}(\mathrm{tail}(\mathrm{even}(\alpha))) &=& \mathrm{head}(\mathrm{tail}(\mathrm{tail}(\alpha))) &=& \alpha(2) \\
&& &\vdots& && \\
\mathrm{even}(\alpha)(n) &=& \mathrm{head}(\mathrm{tail}^{(n)}(\mathrm{even}(\alpha))) &=& \mathrm{head}(\mathrm{tail}^{(2n)}(\alpha)) &=& \alpha(2n) \\
&& &\vdots& &&
\end{eqnarray*}
よって， 余帰納的定義を用いて目的の関数が得られた．
次の関数 $\mathrm{odd}(\alpha)(n) = \alpha(2n+1)$ は $\mathrm{even}$ を用いて簡単に定義できる．
$$ \mathrm{odd}(\alpha) = \mathrm{even}(\mathrm{tail}(\alpha)) $$
最後に $\mathrm{merge} : A^\infty \times A^\infty \to A^\infty$を余帰納的に定義する．
\begin{eqnarray*}
\mathrm{head}(\mathrm{merge}(\alpha, \beta)) &=& \mathrm{head}(\alpha) \\
\mathrm{tail}(\mathrm{merge}(\alpha, \beta)) &=& \mathrm{merge}(\beta, \mathrm{tail}(\alpha))
\end{eqnarray*}
この定義が次と同値であることが確かめられる．
\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 $$
(証明)． 任意の自然数 $n$ と任意の $\alpha \in A^\infty$ について $\mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha))(n) = \alpha(n)$ であることを示せばよい． これを $n$ についての帰納法で示す．
($n=0$ のとき)
\begin{eqnarray*}
\mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha))(0)
&=& \mathrm{head}(\mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha))) \\
&=& \mathrm{head}(\mathrm{even}(\alpha)) \\
&=& \alpha(0)
\end{eqnarray*}
($n = k+1$ のとき)
\begin{eqnarray*}
\mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha))(k+1)
&=& \mathrm{head}(\mathrm{tail}^{(k+1)}(\mathrm{merge}(\mathrm{even}(\alpha), \mathrm{odd}(\alpha)))) \\
&=& \mathrm{head}(\mathrm{tail}^{(k)}(\mathrm{merge}(\mathrm{odd}(\alpha), \mathrm{tail}(\mathrm{even}(\alpha))))) \\
&=& \mathrm{head}(\mathrm{tail}^{(k)}(\mathrm{merge}(\mathrm{odd}(\alpha), \mathrm{even}(\mathrm{tail}(\mathrm{tail}(\alpha)))))) \\
&=& \mathrm{head}(\mathrm{tail}^{(k)}(\mathrm{merge}(\mathrm{even}(\mathrm{tail}(\alpha)), \mathrm{odd}(\mathrm{tail}(\alpha))))) \\
&=& \mathrm{merge}(\mathrm{even}(\mathrm{tail}(\alpha)), \mathrm{odd}(\mathrm{tail}(\alpha)))(k) \\
&=& \mathrm{tail}(\alpha)(k) \\
&=& \alpha(k+1)
\end{eqnarray*}
(証明終)
この証明は無限リストが$\mathbb{N}$からの関数であるという内部的な構造を利用して， 帰納法によって命題を示した． 内部的な構造を利用せず， 余帰納的な性質を用いて示す方法はないだろうか? その疑問の答えとして， bisimulationがある． 詳しくは後述するが， bisimulationは余帰納的なデータにおける等式を示すための手法である．
まとめ
帰納的データはコンストラクターが特徴付けるが， 余帰納的データはデストラクターが特徴付ける．
帰納的データからの関数は帰納的に定義できる． 余帰納的データへの関数は余帰納的に定義できる．
参考文献
- 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. (リンク)