F代数

数学, 特に圏論において, F-代数(英:F-algebra) は、関手 $F$ に従って定義された構造である。関手を特に示す必要がない場合は単に代数とも呼ばれる。 F-代数はプログラミングで使われる、リストや木構造のようなデータ構造を表現するのに使用できる。 F-始代数(initial F-algebra)は、数学的帰納法の原理を埋め込む。

F-代数はF-余代数の双対である。

可換図式。対象A及び射αの組(A,α)と、対象B及び射βの組(B,β)はそれぞれF-代数で、この図を可換にする射fが準同型射である。これらは、F-代数の新しく定義された圏の射になるように、元の圏の射で必要な属性(property)を定義する。

形式的定義

自己関手:$F : \mathcal{C}\longrightarrow \mathcal{C}$ のF-代数とは、

圏Cの対象Aと、圏Cの射

$\alpha : FA \longrightarrow A$

の組である。

この意味で、F-代数はF-余代数の双対である。

また、F-代数$(A, \alpha)$からF-代数$(B, \beta)$への準同型射とは、 圏Cの射$f:A\longrightarrow B$ で

$f\circ \alpha = \beta \circ Ff$

を満たすものである。

F-代数と準同型射の全体は圏をなす。

例

集合$X$ を $1+X$に対応づけるような、関手 $F: \mathbf{Set} \to\mathbf{Set}$を考える。 $\mathbf{Set}$は集合の圏の意味で, $+$ は集合の直和で与えられる圏論的直和(coproduct)を意味し, $1$ は終対象である。(すなわち、任意の1者集合)。 次に、

自然数の集合N

$\mathrm{zero} : 1 \to \mathbb{N}$ (像は0) と $\mathrm{succ} : \mathbb{N} \to \mathbb{N}$ （自然数 nを n+1 にする）という、二つの関数の直和（coproduct）

$[\mathrm{zero},\mathrm{succ}] : 1+\mathbb{N} \to \mathbb{N}$

の組、$(\mathbb{N}, [\mathrm{zero},\mathrm{succ}])$ はF-代数である。

F -始代数

詳細は「始代数」を参照

自己関手$F$で与えられたF-代数の圏が始対象を持っている場合、それは始代数と呼ばれる. 上記の例で、代数$(\mathbb{N}, [\mathrm{zero},\mathrm{succ}])$ は始代数である。プログラミングで使われるリストや木構造のような、様々な有限データ構造は、特定の自己関手の始代数として得られる。

最小不動点と関手Fで構築された型はF-始代数と見なすことができ, パラメトリシティ(en:parametricity)を保持した型を提供する。

普遍代数も参照。

F -終余代数

双対的な方法で、同様の関係が最大不動点とF-終余代数の間に存在する。これらは強正規化性を維持しながら、潜在的に無限のオブジェクトを扱うことを可能にする。 強正規化を行うプログラミング言語Charityの、余帰納的データ型は驚くべき結果を得ることが出来る。 例えば、アッカーマン関数のような"強い"関数を実装するために参照の構成要素を定義する。

関連項目

• 代数的データ型
• Catamorphism

参考文献

• Pierce, Benjamin C.. “F-Algebras”. Basic Category Theory for Computer Scientists. ISBN 0262660717. 

外部リンク

• Categorical programming with inductive and coinductive types by Varmo Vene
• Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
• Algebra and coalgebra from CLiki