F余代数

提供: testwiki
ナビゲーションに移動 検索に移動

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

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

定義

テンプレート:Mvarを圏𝒞上の自己関手

F:𝒞𝒞

とするとき、テンプレート:Mvar-余代数とは𝒞の対象 A と

α:AFA

の組 (A,α) である。

テンプレート:Mvar-余代数 (A,α) から別のテンプレート:Mvar-余代数 (B,β) への(テンプレート:Mvar-余代数としての)準同型とは、𝒞の射

f:AB

であって

Ffα=βf

を満たすものである。

これにより、ある自己関手テンプレート:Mvarについて、テンプレート:Mvar-余代数全体は圏をなす。

関手 F:𝐒𝐞𝐭𝐒𝐞𝐭 として、 X を (X×A){1} に送るものを考える。すると テンプレート:Mvar-余代数 α:X(X×A){1}=FX はアルファベットA上の有限または無限ストリームをあらわすことになる。このとき X は状態集合、 α は状態遷移関数である。状態遷移関数を状態に適用した場合、2通りの結果が考えられる。ひとつは A の元とストリームの次の状態が返される場合、もうひとつは単元集合 {1} の元が返される場合である。後者は特別な「終状態」、つまりストリームが打ち止めであることを表す値である。

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

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

応用

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

関連項目

参考文献

外部リンク