F余代数

数学の特に圏論における -余代数 (エフよだいすう、) は、(自己)関手  によって定義される構造の一つである。代数や余代数を扱う文脈ではよく、シグネチャに由来する関手を考える。-余代数の概念は計算機科学で使われることが多い。例えば、遅延評価、ストリームのような無限データ構造、状態遷移系などは-余代数の言葉で説明される。

-余代数は-代数の双対である。あるシグネチャと等式理論に対する代数を全て集めたクラスがバラエティをなすのと同様、所与の等式理論を満たす-余代数 (はそのシグネチャから由来するとする) 全体は余バラエティーをなす。

 定義 
を圏上の自己関手

とするとき、-余代数とはの対象  と射

の組  である。

-余代数  から別の-余代数  への(-余代数としての)準同型とは、の射

であって

を満たすものである。

これにより、ある自己関手について、-余代数全体は圏をなす。

 例 
関手  として、  を  に送るものを考える。すると -余代数  はアルファベット上の有限または無限のストリームをあらわすことになる。このとき  は状態集合、  は状態遷移関数である。状態遷移関数を状態に適用した場合、2通りの結果が考えられる。ひとつは  の元とストリームの次の状態が返される場合、もうひとつは単元集合  の元が返される場合である。後者は特別な「終状態」、つまりストリームが打ち止めであることを表す値である。

多くの実用的な例では、このような余代数の状態遷移関数は  という形になっていて、「セレクタ」「オブザーバ」「メソッド」のように機能別に  と分割して考えることができるようになっている。多くの場合、オブザーバーは何らかの属性値を出力するようになっていて、状態を書き換えるメソッドは  のように追加のパラメーターを受け取って次の状態を返す形になっている。このような分解は、-始代数をいくつかの「コンストラクタ」の直和に分解できる現象の双対になっている。

をの冪集合とし、これを集合の圏の共変関手とみなす。このとき、-余代数は二項関係の入った集合と一対一に対応する。さらにここで集合を固定する。すると自己関手の余代数はラベルつき遷移系と一対一に対応し、余代数の間の準同型は関数双模倣に対応する。

 応用 
余代数は状態をもつシステム (状態遷移系や、オブジェクト指向プログラミングにおけるクラスなど) や、無限の内容を持ちうるデータ構造 (ストリームなど) などの挙動を、十分に一般的かつ利用しやすい形で記述できることから、計算機科学で広く用いられるようになった。代数的仕様がシステムの動作を関数として (特に、コンストラクタによって生成される帰納的なデータ型を用いて) 記述するのに対し、余代数的仕様はシステムの動作を余帰納的なプロセス、つまりセレクタの出力によって観測される内容として (オートマトン理論のような考え方で) 記述する。このときありえる全ての無限動作を漏れなく重複なく集めてきた集合が終余代数となるため、終余代数も重要な役割を果たす。余代数によって記述されるシステムの性質を記述するのには、余代数的様相論理が適している。

 関連項目 
 余代数 (代数学における)

 参考文献 
 B. Jacobs and J. Rutten,  A Tutorial on (Co)Algebras and (Co)Induction.  EATCS Bulletin 62, 1997, p.222-259. 
 Jan J. M. M. Rutten: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1): 3-80 (2000).
 J. Adámek, Introduction to coalgebra. Theory and Applications of Categories 14 (2005), 157-199
 B. Jacobs, Introduction to Coalgebra. Towards Mathematics of States and Observations (book draft)
 Yde Venema: Automata and Fixed Point Logics: a Coalgebraic Perspective. Information and Computation, 204 (2006) 637-678.

 外部リンク 
 CALCO 2009: Conference on Algebra and Coalgebra in Computer Science
 CALCO 2011

Category:圏論
Category:余代数
Category:数学に関する記事