始代数について

始代数について
　始代数とは再帰的定義もしくは帰納的定義を一般化したものとして考えることができます。これは圏論の概念から生まれたものなので、圏に関する概念、圏、関手、始対象などの知識があると簡潔に述べることができるのですが、再帰的定義との関連から整理することでも理解できると思います。
　再帰的定義や帰納的定義は自然数や文字列で使われ、コンピュータ科学（計算理論）ではBNF記法などで定義されるものです。たとえば、自然数は次のように定義できます。

・0は自然数である
・nが自然数であるとき、succ n は自然数である。
・以上の操作のみによって定義されるのが自然数である。

　以上の定義の２つ目の条件では自然数の定義に自然数が参照されています。これが再帰と呼ばれる部分です。0からsucc 0が、succ 0からsucc succ 0が、と次々と自然数が定義されます。これが帰納と呼ばれる部分です。BNF記法では次のように書けるでしょう。

自然数 ::= 0 | succ 自然数

　このように定義される集合または型では帰納法による証明ができることを意味します。たとえば、ある自然数の性質（述語）Pがすべての自然数で成り立つことを証明したい場合には、0がPを満たすことと、nがPを満たすことがsucc nがPを満たすことを含意していること、以上の2つの条件を示せば十分です。これですべての自然数についてPが成り立っているといえるのは、再帰的定義の最後の条件（以上の操作のみによって…）が保証します。

　始代数の定義では、これをある条件を満たす関数の一意的存在として整理します。再び自然数を例に取りましょう。自然数を始代数的に定義すると次のようになります。

・自然数Nは定数0と関数succ : N → N を持つ
・任意の集合Xが定数cと関数h : X → X を持つとき、次の条件を満たす関数f : N → X がただひとつ存在する。
f(0) = c
f(succ n) = h(f(n))

　これは、２つの条件を与えれば、自然数から集合Xへの関数を定義できることを示しています。本来、関数の定義をする場合は、すべての引数に対して返値がただ一つ定まる規則を与えなければなりませんが、自然数の場合は、これだけでいいということなので、これえはかなり強力です。
　このブログにおける自然数や文字列の議論でも、いくつかの演算子を定義するときにこの性質を利用しています。
　なぜ、この２つの条件だけでいいのかを形式的に示すのは、多少込み入っているので、再帰性についての専門的な文献を参照してください。