Algebras and Coalgebras, Section 10. Final coalgebras

終余代数 (final coalgebra) の基本的な話。

終余代数とは、余代数の圏の終対象のこと。関手を fix するごとに定義される。理論はだいたい知ってるので例を中心に見ていく。

some examples

black box machine $M \rightarrow C \times M$ . M が機械の内部状態で C が出力。状態遷移を起こすごとに C の要素を出力する。これは $C \times (-)$ 上の coalgebra で、この関手の final coalgebra は C のストリーム $C^\omega \ni (c_0, c_1, c_2, \dots) \rightarrow (c_0, (c_1, c_2, \dots)) \in C \times C^\omega$ である。

決定性オートマトン $A \rightarrow 2 \times A^C$ . A が状態の集合、C はアルファベットの集合。2 は {0,1} で、現在の状態が受理状態のとき 1 で、そうでないときは 0 をとる。これは $2 \times (-)^C$ 上の coalgebra で final coalgebra は C 上の言語全体の集合 $P(C^*) \ni L \rightarrow (\lambda_0(L), \lambda_1(L)) \in 2 \times A^C$ である。ここで

$\lambda_0(L) = 1 \Longleftrightarrow \epsilon \in L$ ;
$\lambda_1(L)(c) = \{ w | cw \in L \}$ .

Vietoris functor の上の余代数の圏は descriptive general frame の圏に同型であり、したがって modal algebra の圏の双対に同値である。modal algebra の圏における始対象は Lidenbaum algebra *1 なので、それに対応する canonical frame が Vietoris functor の終余代数となる。

だいたいこれくらい。あとは関数型言語の話で見たことのある、ストリームの zip の話が出てきていたりしました。様相論理の本で見ることになるとは。

existence of final coalgebra

final coalgebra の構造射*2は同型である。このことから、powerset functor など一部の関手については final coalgebra が存在しないことが容易に従う (濃度を比較するだけ)。

あとは、そういう場合でも小さいとは限らない集合の圏とか non-well-founded set を考えるとうまくいったり、超限帰納法で final coalgebra を近似する方法があったりするという話が載っています。この部分は、新しい概念を提示しているというより技術的なテクニックの紹介のように見えたのでざっと目を通しただけで終わりにしてしまいました。

*1:本には書いてありませんでしたが、生成系(あるいは命題変数)の濃度を決めないと Lindenbaum algebra は決まりません。生成系は空であるとした場合が始対象になります。

*2:という名前を使うのかどうか確かではありませんが