始代数
数学において、始代数 (しだいすう、英: initial algebra) とは、与えられた自己関手 F に対する F-代数の圏における始対象を言う。始代数の持つ始対象性 (initiality) は帰納や再帰といったものの一般の枠組みを与える。
始代数の圏論的双対概念として、F-余代数の圏の終対象は終余代数（しゅうよだいすう、英: final coalgebra）と呼ばれる。終余代数の終対象性 (finality) は余帰納や余再帰といった概念の一般な枠組みを与える。
始代数の例
[編集]例えば、集合の圏 Set において、終対象である一元集合を 1 として、自己関手 1 + (–):: X → 1 + X を考える。この自己関手 F に対する F-代数とは、集合 X（これをこの代数の台集合と呼ぶ）とその点 x ∈ X (あるいは同じことだが写像 x: 1 → X) および自己写像 f: X→X の組 (X, [x, f]) のことを言う（紛れの虞の無い場合にしばしば、この組のことを記号の濫用により台集合と同じ記号のみを以って代用し「始代数 X」などと言い表す）。この場合の始代数は、自然数全体の成す集合 N を台集合とし、その最小元 0 と後者関数 succ からなる組 (N, [0, succ]) で与えられる。
この始代数 (N, [0, succ]) が実際に始対象性（この場合は普遍性）を持つことを確かめるのは難しくない。実際、(N, [0, succ]) から勝手な F-代数 (A, [e, f]) (e ∈ A, f: A → A) へのただ一つの準同型射は、自然数 n に対して e に f を n-回反復適用した fn(e) (= f(f(…(f(e))…)) を対応付ける函数によって与えられる。
別な例として、集合の圏上の自己関手 1 + N×(–):: X → 1 + N×X を考えると、この自己関手に対する代数とは、集合 X とその上の点 x ∈ X および関数 f: N × X → X の組 (X, [x, f]) のことになる。この場合の始代数は、自然数を要素とする有限な長さのリスト全体の成す集合、その点としての空リストおよび自己写像 cons（与えられた自然数と有限リストから、その自然数をリストの先頭に付け加えてえられるリストを返す函数）の組で与えられる。
終余代数の例
[編集]例えば、前と同じく集合の圏 Set における自己関手 1 + (–) に対して、その余代数とは台集合 X とその上の真理値判定関数 p: X → 2 および定義域が p(x) = 0 なる x ∈ X の全体で与えられる自己部分写像f: X → X の組 (X, p, f) のことであり、この場合の終余代数は自然数全体に新しい元 ω を付け加えた集合 N ∪ {ω} と 0 を判定する函数 p0（即ち、p0(0) = 1 かつ任意の n ∈ N に対して p0(n+1) = 0 かつ p0(ω) = 0）および、0 以外の自然数に対して前者関数（後者関数の逆関数）として作用し ω は動かさない部分写像 f（即ち、任意の n ∈ N に対して f(n+1) = n かつ f(ω) = ω）の組 (N ∪ {ω}, p0, f) で与えられる。
先のもう一つの例である、集合の圏上の自己関手 1 + N×(–) も同様に考えると、この場合の終余代数のは、自然数を要素とするリスト全体の成す集合（これには有限リストも無限リストも含む）と、「リストが空かどうかを判定する関数」および「空でないリストに対して、そのリストの先頭の自然数とそのリストの先頭を取り除いたリストとの順序対を返す関数 decons」の組で与えられる。
定理
[編集]計算機科学での利用
[編集]リストや木構造など、プログラミングで使われる有限データ構造の多くは、特定の関手に対する始代数として構成することができる。与えられた自己関手に対応する始代数は複数存在し得るけれども、それらは同型の違いを除いて一意である。このことはつまり直感的には、データ構造が「持っているはず」の性質はデータ構造を始代数として定義することで適切に（実現の仕方に依らないで）捕捉できるということである。
集合 A の元を要素に持つリストのデータ型 を得るために、リスト構成演算
の直和として与えられる一つの関数
![{\displaystyle [\mathrm {nil} ,\mathrm {cons} ]\colon 1+(A\times \mathrm {List} (A))\to \mathrm {List} (A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bbc6d945517c61ec2f45a2726edfeb5688a0ae0d)
が A を台集合として、X に 1 + (A × X) を対応させる Set の自己函手 F に対する F-代数を与えることを注意しよう。実はこれが唯一の F-始代数となる。この始代数が持つ始対象性は、HaskellやMLのような関数型プログラミング言語でfoldrと呼ばれている関数によって与えられる。
同様に、葉に要素を持つ二分木は、
![{\displaystyle [\mathrm {tip} ,\mathrm {join} ]\colon A+(\mathrm {Tree} (A)\times \mathrm {Tree} (A))\to \mathrm {Tree} (A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/260fe0d20f6084d56549fcf39289280d3524cf69)
の与える始代数として得ることができる。この方法で得られるデータ型を代数的データ型と呼ぶ。
函手 F から構成される最小不動点を用いて定義されたデータ型は、 F-代数と見なすことができ、またこのデータ型がパラメトリシティを持つようにすることができる[3]。双対に移って、最大不動点と F-終余代数の間に同様の関係が成立し、余帰納的データ型に応用される。これらを、強正規化性を維持しながら可能無限のオブジェクトを扱うことを許すために用いることができる[3]。強正規化を行うプログラミング言語Charityの、余帰納的データ型は驚くべき結果を得ることが出来る。 例えば、アッカーマン関数のような"強い"関数を実装するために参照の構成要素を定義する。[4]
関連項目
[編集]脚注
[編集]- ^ a b Initiality and finality from CLiki
- ^ Induction and Co-induction from CLiki
- ^ a b Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
- ^ Robin Cockett: Charitable Thoughts (ps[リンク切れ] and ps.gz[リンク切れ])
外部リンク
[編集]- Categorical programming with inductive and coinductive types by Varmo Vene
- Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
- Initial Algebra and Final Coalgebra Semantics for Concurrency by J.J.M.M. Rutten and D. Turi
- Initiality and finality from CLiki