始代数のソースを表示

[[数学]]において、'''始代数''' (しだいすう、{{lang-en-short|''initial algebra''}}) とは、与えられた[[関手|自己関手]] ''F'' に対する[[F代数| ''F''-代数]]の[[圏 (数学)|圏]]における[[始対象]]を言う。始代数の持つ始対象性 (''initiality'') は[[数学的帰納法|帰納]]や[[再帰]]といったものの一般の枠組みを与える。

始代数の[[圏論的双対]]概念として、[[F余代数|''F''-余代数]]の圏の[[終対象]]は'''終余代数'''（しゅうよだいすう、{{lang-en-short|''final coalgebra''}}）と呼ばれる。終余代数の終対象性 (''finality'') は[[余帰納]]や[[余再帰]]といった概念の一般な枠組みを与える。

== 始代数の例 ==
例えば、[[集合の圏]] '''Set''' において、[[終対象]]である[[一元集合]]を 1 として、自己関手 1 + (&ndash;):: ''X'' &rarr; 1 + ''X'' を考える。この自己関手 ''F'' に対する ''F''-代数とは、集合 ''X''（これをこの代数の台集合と呼ぶ）とその点 {{nowrap|''x'' ∈ ''X''}} (あるいは同じことだが写像 ''x'': 1 &rarr; ''X'') および自己写像 {{nowrap|''f'': ''X''→''X''}} の[[タプル|組]] (''X'', [''x'', ''f'']) のことを言う（紛れの虞の無い場合にしばしば、この組のことを[[記号の濫用]]により台集合と同じ記号のみを以って代用し「始代数 ''X''」などと言い表す）。この場合の始代数は、[[自然数]]全体の成す集合 '''N''' を台集合とし、その最小元 0 と後者関数 succ からなる組 ('''N''', [0, succ]) で与えられる。 

この始代数 ('''N''', [0, succ]) が実際に始対象性（この場合は[[普遍性]]）を持つことを確かめるのは難しくない。実際、('''N''', [0, succ]) から勝手な ''F''-代数 (''A'', [''e'', ''f'']) (''e'' &isin; ''A'', ''f'': ''A'' &rarr; ''A'') へのただ一つの準同型射は、自然数 ''n'' に対して ''e'' に ''f'' を ''n''-回反復適用した ''f''<sup>''n''</sup>(''e'') (= ''f''(''f''(…(''f''(''e''))…)) を対応付ける函数によって与えられる。

別な例として、集合の圏上の自己関手 1 + '''N'''×(–):: ''X'' &rarr; 1 + '''N'''&times;''X'' を考えると、この自己関手に対する代数とは、集合 ''X'' とその上の点 {{nowrap|''x'' ∈ ''X''}} および関数 {{nowrap|''f'': '''N''' × ''X'' → ''X''}} の組 (''X'', [''x'', ''f'']) のことになる。この場合の始代数は、自然数を要素とする有限な長さのリスト全体の成す集合、その点としての空リストおよび自己写像 [[cons (Lisp)|cons]]（与えられた自然数と有限リストから、その自然数をリストの先頭に付け加えてえられるリストを返す函数）の組で与えられる。

== 終余代数の例 ==
例えば、前と同じく集合の圏 '''Set''' における自己関手 1 + (–) に対して、その余代数とは台集合 ''X'' とその上の真理値判定関数 {{nowrap|''p'': ''X'' → 2}} および定義域が {{nowrap|1=''p''(''x'') = 0}} なる {{nowrap|''x'' ∈ ''X''}} の全体で与えられる自己部分写像{{nowrap|''f'': ''X'' → ''X''}} の組 (''X'', ''p'', ''f'') のことであり、この場合の終余代数は自然数全体に新しい元 &omega; を付け加えた集合 {{nowrap|'''N''' ∪ {ω}}} と 0 を判定する函数 ''p''<sub>0</sub>（即ち、{{nowrap|1=''p''<sub>0</sub>(0) = 1}} かつ任意の ''n'' &isin; '''N''' に対して {{nowrap|1=''p''<sub>0</sub>(''n''+1) = 0}} かつ {{nowrap|1=''p''<sub>0</sub>(ω) = 0}}）および、0 以外の自然数に対して前者関数（後者関数の[[逆関数]]）として作用し &omega; は動かさない部分写像 ''f''（即ち、任意の ''n'' &isin; '''N''' に対して {{nowrap|1=''f''(''n''+1) = ''n''}} かつ {{nowrap|1=''f''(ω) = ω}}）の組 ('''N''' &cup; {&omega;}, ''p''<sub>0</sub>, ''f'') で与えられる。

先のもう一つの例である、集合の圏上の自己関手 1 + '''N'''×(–) も同様に考えると、この場合の終余代数のは、自然数を要素とするリスト全体の成す集合（これには有限リストも無限リストも含む）と、「リストが空かどうかを判定する関数」および「空でないリストに対して、そのリストの先頭の自然数とそのリストの先頭を取り除いたリストとの順序対を返す関数 decons」の組で与えられる。

== 定理 ==
* 始代数は最小である (すなわち、真の部分代数を持たない)<ref name=infin/>。
* 終余代数は[[単純代数|単純]]である (すなわち、真の商を持たない<ref>[http://tunes.org/wiki/induction_20and_20co-induction.html Induction and Co-induction] from CLiki</ref>)<ref name=infin>[http://tunes.org/wiki/initiality_20and_20finality.html Initiality and finality] from CLiki</ref>。

== 計算機科学での利用 ==
[[リスト_(抽象データ型)|リスト]]や[[木構造 (データ構造)|木構造]]など、[[プログラミング]]で使われる有限[[データ構造]]の多くは、特定の関手に対する始代数として構成することができる。与えられた自己関手に対応する始代数は複数存在し得るけれども、それらは[[同型]]の[[違いを除いて]]一意である。このことはつまり直感的には、データ構造が「持っているはず」の性質はデータ構造を始代数として定義することで適切に（実現の仕方に依らないで）捕捉できるということである。

集合 ''A'' の元を要素に持つリストのデータ型 <math>\mathrm{List}(A)</math> を得るために、リスト構成演算
* <math>\mathrm{nil}\colon 1\to \mathrm{List}(A),</math>
* <math>\mathrm{cons}\colon A\times \mathrm{List}(A)\to \mathrm{List}(A)</math>
の直和として与えられる一つの関数
: <math>[\mathrm{nil},\mathrm{cons}]\colon 1 + (A\times \mathrm{List}(A))\to \mathrm{List}(A)</math>
が ''A'' を台集合として、''X'' に 1 + (''A'' &times; ''X'') を対応させる '''Set''' の自己函手 ''F'' に対する ''F''-代数を与えることを注意しよう。実はこれが唯一の ''F''-始代数となる。この始代数が持つ始対象性は、[[Haskell]]や[[ML (プログラミング言語)|ML]]のような[[関数型プログラミング言語]]で[[fold|<code>foldr</code>]]と呼ばれている関数によって与えられる。

同様に、葉に要素を持つ[[二分木]]は、
: <math>[\mathrm{tip},\mathrm{join}]\colon A + (\mathrm{Tree}(A)\times \mathrm{Tree}(A))\to \mathrm{Tree}(A)</math>
の与える始代数として得ることができる。この方法で得られるデータ型を[[代数的データ型]]と呼ぶ。

函手 ''F'' から構成される最小不動点を用いて定義されたデータ型は、[[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>。双対に移って、[[最大不動点]]と ''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]{{リンク切れ|date=2017年10月 |bot=InternetArchiveBot }} and [ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/papers_and_reports/charitable.ps.gz ps.gz]{{リンク切れ|date=2017年10月 |bot=InternetArchiveBot }})</ref>

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

== 脚注 ==
<references/>

== 外部リンク ==
* [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://citeseer.ist.psu.edu/rutten94initial.html Initial Algebra and Final Coalgebra Semantics for Concurrency] by  J.J.M.M. Rutten and D. Turi
* [http://tunes.org/wiki/initiality_20and_20finality.html Initiality and finality] from CLiki

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