F代数のソースを表示

{{DISPLAYTITLE:''F''代数}}
[[数学]]の特に[[圏論]]における'''''F''-代数'''（エフだいすう、{{lang-en-short|''F''-''algebra''}}）は、（自己）[[関手]] ''F'' に従って定義される構造の一つで、[[リスト (抽象データ型)|リスト]]や[[木構造 (データ構造)|木構造]]のような[[プログラミング]]で使われる[[データ構造]]を表現するのに利用できる。 [[始代数|''F''-始代数]]は、[[数学的帰納法|数学的帰納法の原理]]を捉えたものと考えることができる。文脈上紛れの虞が無い場合は、函手 ''F'' を明示するための接頭辞 ''F''- を省略して単に'''代数'''ということがある。

''F''-代数は[[F余代数| ''F''-余代数]]の[[圏論的双対|双対]]である。

== 厳密な定義 ==
[[圏 (数学)|圏]] '''C''' とその上の[[関手|自己関手]] ''F'': '''C''' &rarr; '''C''' に対し、'''''F''-代数'''とは '''C''' の対象 ''A'' と '''C''' の[[射 (圏論)|射]] &alpha;: ''F''(''A'') &rarr; ''A'' との組 (''A'', &alpha;) のことをいう。この意味で、''F''-代数は ''F''-余代数の[[双対]]である。 

[[Image:Commutative diagram defining F-algebra.png|thumb|''F''-代数の準同型がもとの圏において満たすべき条件を示した可換図式。すなわち、この条件を満たす ''f'' が新しい ''F''-代数の圏での射となる。]]
''F''-代数 (''A'', &alpha;) から別の ''F''-代数 (''B'', &beta;) への '''''F''-代数の準同型'''とは、'''C'''-射 ''f'': ''A'' &rarr; ''B'' で条件
<math display="block"> f\circ \alpha = \beta \circ F(f)</math>
を満たす（すなわち、右図の図式を可換にする）ものをいう。

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

== 例 ==
'''Set''' を[[集合の圏]]、1 を '''Set''' における終対象（すなわち任意の[[一元集合]]）、+ は '''Set''' における[[直和 (圏論)|（圏論的）直和]]（すなわち[[非交和]]）とするとき、'''Set''' の自己函手 ''F'': ''X'' &rarr; 1 + ''X'' を考えると、('''N''', [0, succ]) は一つの ''F''-代数を与える。ただし、'''N''' は[[自然数]]全体の成す集合、[0,succ] は二つの写像
<math display="block">0\colon 1 \to \mathbb{N}; * \mapsto 0,</math>
<math display="block">\mathrm{succ}\colon \mathbb{N}\to \mathbb{N}; n \mapsto n+1</math>
の直和（つまり、''x'' &isin; 1 + '''N''' が ''x'' &isin; 1 ならば写像 0 に ''x'' &isin; '''N''' ならば写像 succ に一致するような写像）である。

== ''F'' -始代数 ==
{{main|始代数}}
与えられた自己函手 ''F'' に対する ''F''-代数の圏が[[始対象]]を持つならば、その始対象を ''F''-始代数と呼ぶ。上記の例で挙げた代数 ('''N''', [0,succ]) は始代数である。プログラミングで使われるリストや木構造のようないくつもの[[有限集合|有限]]データ構造が、特定の自己関手の始代数として得られる。

函手 ''F'' から構成した[[最小不動点]]で定義される型は ''F''-始代数と見なすことができ、これはこの型に対する[[パラメトリシティ]]([[:en:parametricity]])を保つものとしてよい。<ref name=free-rectypes>Philip Wadler: [http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt Recursive types for free!] University of Glasgow, July 1998. Draft.
</ref>

{{See also|普遍代数学}}

== ''F'' -終余代数 ==

[[双対]]的な方法で、同様の関係が[[最大不動点]]とF-終余代数の間に存在する。これらは[[強正規化性]]を維持しながら、[[可能無限]]個のオブジェクトを扱うことを可能にする。<ref name=free-rectypes/> 強正規化を行うプログラミング言語[[:en:Charity (programming language)|Charity]]の、[[余帰納法|余帰納的]]データ型は驚くべき結果を得ることが出来る。 
例えば、[[アッカーマン関数]]のような"強い"関数を実装するために参照の構成要素を定義する。<ref>Robin Cockett: Charitable Thoughts ([ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/papers_and_reports/charitable.ps ps] and [ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/papers_and_reports/charitable.ps.gz ps.gz])</ref>

== 脚注 ==
<references/>

== 参考文献 ==
* {{cite book|first=Benjamin C.|last=Pierce|authorlink=Benjamin C. Pierce|title=Basic Category Theory for Computer Scientists|chapter=F-Algebras|isbn=0262660717}}

== 関連項目 ==
* [[代数的データ型]]
* [[Catamorphism]]

== 外部リンク ==

* [http://www.cs.ut.ee/~varmo/papers/thesis.pdf Categorical programming with inductive and coinductive types] by Varmo Vene
* Philip Wadler: [http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt Recursive types for free!] University of Glasgow, July 1998. Draft.
* [http://tunes.org/wiki/algebra_20and_20coalgebra.html Algebra and coalgebra] from CLiki

{{デフォルトソート:Fたいすう}}
[[Category:圏論]]
[[Category:関数型プログラミング]]
[[Category:数学に関する記事]]