F代数
数学の特に圏論におけるF-代数（エフだいすう、英: F-algebra）は、（自己）関手 F に従って定義される構造の一つで、リストや木構造のようなプログラミングで使われるデータ構造を表現するのに利用できる。 F-始代数は、数学的帰納法の原理を捉えたものと考えることができる。文脈上紛れの虞が無い場合は、函手 F を明示するための接頭辞 F- を省略して単に代数ということがある。
厳密な定義
圏 C とその上の自己関手 F: C → C に対し、F-代数とは C の対象 A と C の射 α: F(A) → A との組 (A, α) のことをいう。この意味で、F-代数は F-余代数の双対である。
F-代数 (A, α) から別の F-代数 (B, β) への F-代数の準同型とは、C-射 f: A → B で条件
- [math] f\circ \alpha = \beta \circ F(f)[/math]
を満たす（すなわち、右図の図式を可換にする）ものをいう。
F-代数の全体は、F-代数準同型を射として圏をなす。
例
Set を集合の圏、1 を Set における終対象（すなわち任意の一元集合）、+ は Set における（圏論的）直和（すなわち非交和）とするとき、Set の自己函手 F: X → 1 + X を考えると、(N, [0, succ]) は一つの F-代数を与える。ただし、N は自然数全体の成す集合、[0,succ] は二つの写像
- [math]0\colon 1 \to \mathbb{N}; * \mapsto 0,[/math]
- [math]\mathrm{succ}\colon \mathbb{N}\to \mathbb{N}; n \mapsto n+1[/math]
の直和（つまり、x ∈ 1 + N が x ∈ 1 ならば写像 0 に x ∈ N ならば写像 succ に一致するような写像）である。
F -始代数
与えられた自己函手 F に対する F-代数の圏が始対象を持つならば、その始対象を F-始代数と呼ぶ。上記の例で挙げた代数 (N, [0,succ]) は始代数である。プログラミングで使われるリストや木構造のようないくつもの有限データ構造が、特定の自己関手の始代数として得られる。
函手 F から構成した最小不動点で定義される型は F-始代数と見なすことができ、これはこの型に対するパラメトリシティ(en:parametricity)を保つものとしてよい。[1]
普遍代数学も参照。
F -終余代数
双対的な方法で、同様の関係が最大不動点とF-終余代数の間に存在する。これらは強正規化性を維持しながら、可能無限個のオブジェクトを扱うことを可能にする。[1] 強正規化を行うプログラミング言語Charityの、余帰納的データ型は驚くべき結果を得ることが出来る。 例えば、アッカーマン関数のような"強い"関数を実装するために参照の構成要素を定義する。[2]
関連項目
脚注
参考文献
- 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