始代数

数学において、始代数(しだいすう。英:initial algebra)とは、与えられた自己関手FのF-代数の圏における始対象である。Initialityは帰納と再帰のための一般的な枠組みを提供する。

例えば、1を圏の終対象である一点集合とした場合の集合圏上の自己関手1＋(-)について考える。 この自己関手の代数は、集合X（代数の台集合(carrier)と呼ばれる）の点x ∈ Xと、関数X→Xである。点を0、関数は後者関数とすると、自然数の集合は、そのような始代数の台集合である。

二つ目の例として、集合圏上の自己関手1+N×(-)を考える。ここで、Nは自然数の集合である。 この自己関手の代数は、集合Xのx ∈ Xと、関数 N×X → Xである。点を空リスト、関数を「数と有限リストを取り、新しい有限リストと先頭の数を返す関数cons」とすると、自然数のリストはそのような始代数の台集合である。

終余代数

始代数の双対、終余代数(final coalgebra)はF-余代数の圏の終対象である。finalityは余帰納と余再帰のための一般的な枠組みを提供する。

例えば、前と同じ関手 1+(-)を使い、集合Xの真理値判定関数p : X → 2と部分関数f : X → Xの定義域はx ∈ Xとp(x) = 0で形作られる。

新しい要素ωで拡張された自然数からなる集合N ∪ {ω}は圏の終余代数の台集合である。

ここで、

p(0) = 1, p(n+1) = p(ω) = 0

pは0のため、fは正の数の場合は、前者関数（後者関数の逆関数）である。 しかし、新しい要素ωの場合は恒等関数のように振る舞う。

f(n+1) = n, f(ω) = ω

二つ目の例の同じ関手1+N×(-)について考えると、この場合の終余代数の台集合は、全ての自然数のリストからなる。これは有限リストだけでなく、無限リストも含む。演算は「リストが空かどうか判定する関数」と「空でないリストについて、先頭の数とリストの残りの組を返す解体関数」である。

定理

• 始代数は最小である。(すなわち、部分代数を持たない
• 終余代数は単純である。 (すなわち、商を持たない）

例

$X$ を $1+X$に対応づける自己関手$F: \mathbf{Set} \longrightarrow \mathbf{Set}$について考える。

自然数の集合と、関数$zero : 1 \longrightarrow N$と$succ : N \longrightarrow N$はF-始代数である。

ここで、zeroは$1$を自然数集合の任意の一者集合に対応づける関数で、succは後者関数である。

Initiality（この場合は普遍性）を確立することは難しくなく、任意のF-代数$(A, [e,f])$のユニークな準同型射は、Aの要素$e : 1 \longrightarrow A$と、Aの関数 $f : A \longrightarrow A$とすると、これは自然数nを$f^n(e)$に対応づけ、f(f(...(f(e))...))となり、eをfにn回-畳み込み適用した関数になる。

計算機科学での利用

リストや木構造の様な、プログラミングで使われる様々な有限データ構造は、特定の関手の始代数として得られる。与えられた自己関手にいくつかの始代数があるかもしれないが、それらは同型射同士の違いを除いて一意であり、これは直感的にはデータ構造の可視的な属性は、始代数によって適切に補足されることを意味する。

集合Aを要素とするリストのデータ型$List(A)$を得るには、リストを構成する演算として、

• $nil : 1\longrightarrow List(A)$
• $cons : A\times List(A)\longrightarrow List(A)$

これらの関数を組み合わせた、一つの関数を

• $[nil,cons] : 1 + (A\times List(A))\longrightarrow List(A)$,

によって与える。 これは自己関手Fの$X$から$1+(A\times X)$へのF-algebraになる。

これは、名実ともに唯一のF-始代数である。

HaskellやMLのような関数型プログラミング言語では、Initialityはfoldrとして知られる関数によって確立されている。

同様に、葉に要素を持つ二分木は始代数として得ることが出来る。

• $[tip,join] : A + (Tree(A)\times Tree(A))\longrightarrow Tree(A)$.

このタイプは代数的データ型として知られる方法で得られる。

最小不動点と関手Fによって定義された型は、F-代数と見なすことが出来き、パラメトリシティ(en:parametricity)を保持した型を提供する。

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

関連項目

• 代数的データ型
• Catamorphism
• Anamorphism

外部リンク

• 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