余帰納的定義、余帰納法、余帰納京子 - 曇りなき眼で見定めブログ

　とある論文を読んでいて余帰納法の知識が必要になったので調べた。その論文ではJacobs & Rutten "A tutorial on (co)algebras and (co)induction"で入門するとよいとあったのだが、同論文のような圏と関手を使った議論はそんなに必要そうではなかった。

　で、いろいろ検索した結果、TaPLことBenjamin C. Pierce『型システム入門』にちょっと載ってる議論が役に立った。

型システム入門プログラミング言語と型の理論

Amazon

同書の監訳者の住井英二郎先生はブログでもいろいろ書いておられる。

sumii.hatenablog.com

また住井先生が著者の一人である『プログラム意味論の基礎』(小林直樹共著・サイエンス社)でも簡単に触れられている。

プログラム意味論の基礎 (ライブラリ情報学コア・テキスト 11)

作者:小林直樹,住井英二郎
サイエンス社

Amazon

　圏と関手を使った議論もちょっと調べた。Jacobs & Ruttenの論文の改訂版が"Introduction to (co)algebra and (co)induction"というタイトルで↓の本に入っている。これを見た。

Advanced Topics in Bisimulation and Coinduction (Cambridge Tracts in Theoretical Computer Science, Series Number 52)

Cambridge University Press

Amazon

　その辺を読んで学んだ事を纏めておく。

余帰納的定義

　集合 $S$ の冪集合 $\wp (S)$ を考える。 $\wp(S)$ は包含関係 $\subset$ で順序集合となる。この順序についての単調関数 $F \colon \wp(S) \to \wp(S)$ を用意する。で、 $X \in \wp(S)$ で $X \subset F(X)$ となるものを考える。このような $X$ のうち包含関係について最大のものが、余帰納的に定義される集合なのである。しかもこの最大のもの $S_1$ は以下のように具体的に得られる。

　 $S_1 = \bigcup \{X \in \wp(S) \mid X \subset F(X)\}$

この $S_1$ はさらに、 $X = F(X)$ を満す最大の $X$ 、すなわち $F$ の最大不動点となっている。

　帰納的定義ではBNFが使われるが、余帰納的定義でも使える。

　 $A ::= f_1(A_1, ..., A_{k_1}) \mid ... \mid f_n(A_1, ..., A_{k_n})$

というBNFで余帰納的に定義される集合というのは、

　 $F(X) = \{f_1(x_1, ..., x_{k_1}) \mid x_1, ..., x_{k_1} \in X\} \cup ... \cup \{f_n(x_1, ..., x_{k_1}) \mid x_1, ..., x_{k_n} \in X\}$

によって定義される単調関数 $F$ によって余帰納的に定義される集合の事である。例えば、

　 $s ::= {\tt a}s \mid {\tt b}s$

というBNFで余帰納的に定義される集合は、

　 $F(X) = \{{\tt a}, {\tt b}\} \cup \{{\tt a}s \mid s \in X\} \cup \{{\tt b}s \mid s \in X\}$

という単調関数で余帰納的に定義される集合で、これは実のところ長さ $1$ 以上の ${\tt a, b}$ の有限列・無限列すべての集合となる。

余帰納法による証明

　余帰納法による証明は、 $S_1$ が単調関数 $F$ から余帰納的に定義されているとき、 $X \subset F(X)$ を示すことで $X \in S_1$ を示すものである。例は『プログラム意味論の基礎』28ページを見てね。

終余代数

　以上のような議論は圏と関手を使ってもっと一般化できる。圏 $C$ とその自己関手 $F \colon C \to C$ があったとき、 $C$ の対象 $X$ と射 $a \colon X \to F(X)$ の組 $(X, a)$ を $F$ -余代数という（"Introduction to (co)algebra and (co)induction"ではすべて ${\bf\rm Set}$ で議論しているが、圏一般に拡張してもよいらしい）。

　 $F$ -余代数を対象とした圏を作れる。射は次のように作る。 $(X, a), (Y, b)$ を $F$ -余代数とする。もとの圏 $C$ において射 $f \colon X \to Y$ があり、 $f \circ a = b \circ F(f)$ を満すとき（可換図式を描くとわかりやすいのだけど省略）、この $f$ を射とするのである。

　こうして得られた $F$ -余代数の圏の終対象を $F$ -終余代数と呼ぶ。これが余帰納的定義になっている。 $\wp(S)$ は包含関係 $\subset$ で順序集合となるが、この $\subset$ を射とみなすとこれは圏になる。すると単調関数 $F \colon \wp(S) \to \wp(S)$ は自己関手である。なので $X \subset F(X)$ となるとき $(X, \subset)$ は $F$ -余代数となる。 $(Y, \subset)$ も $F$ -余代数のとき、 $X \subset Y$ となれば、またそのときのみ $F$ -余代数の圏で $(X, \subset)$ と $(Y, \subset)$ の間には射がある（示すのは簡単）。ということは $F$ -終余代数は $X \subset F(X)$ となる $X$ のうち包含関係について最大のもの（から得られた余代数）であると言える。