文字列が自由モノイドであることの証明

　この記事では文字列の集合が自由モノイドであることを示します。そのためには次のような順序を踏みます。
（１）文字列の始代数性
（２）指数関数、連接、挿入関数の定義
（３）諸性質の整理
（４）モノイドであることの証明
（５）自由であることの証明
　

（1）文字列の始代数性

Σを文字の集合としたとき、文字列の集合Σ*は次のように再帰的に定義できます。
・空列εはΣ*の文字列である。
・aがΣの文字、xがΣ*の文字列のとき、x:aはΣ*の文字列である。
・Σ*の文字列は、以上の操作のみによって構成される。

　２番目の条件では、文字列の後ろに文字を追加する操作を(:)という記号で表しています。これは次のような関数を与えます。
\[ (:) : Σ^*×Σ → Σ^* \\ (:)\ (x, a) = x:a \]
　この操作はconsと呼ばれます。

　以上の定義によって、次のようなことが言えます。
　任意に集合X、Xの定数c、関数 h : X × Σ → X が与えられたとき、次のような関数 f : Σ* → X がただ一つ存在する。
\[\begin{eqnarray*}
f(ε) &=& c \\
f(x:a) &=& h(f(x), a)
\end{eqnarray*}\]
　
　これは文字列が一つの始代数であることを意味しています。また、この性質からいくつかの関数を定義することができます。

（２）指数関数、連接、挿入関数の定義

指数関数

Mを単位元e、乗法・を持つ任意のモノイドとします。任意に文字の集合ΣからモノイドMへの関数f : Σ → M が与えられたとき、f を底とする右指数関数 f^ : Σ* → M を次のように定義します。
\[\begin{eqnarray*}
f^ε &=& e \\
f^{x:a} &=& f^x \cdot f(a)
\end{eqnarray*}\]
　同様に左指数関数^f : Σ* → M を次のように定義します。
\[\begin{eqnarray*}
^εf &=& e \\
^{x:a}f &=&   f(a) \cdot \ ^xf
\end{eqnarray*}\]

　これら２つの等式を条件として与えることで、関数が定義できるのは（１）における始代数であることが保証しています。

連接

　consは各文字aに対して、文字列上の単項演算子(:a)を与えます。つまり、文字aを後ろに追加する演算子です。これによりconsは、文字を文字列上の単項演算子へ写す関数を与えます。文字列上の単項演算子全体はモノイド構造を持っているので（idを単位元、合成を乗法とする）、consを底とする指数関数を考えることができます。まず、consを底とする左指数関数を考えましょう。

\[\begin{eqnarray*}
^ε(:) &=& id_{Σ^*} \\
^{x:a}(:) &=&   (:a) \circ \ ^x(:)
\end{eqnarray*}\]

　これを使って、連接・を次のように定義します。

\[ x \cdot y = \ ^y(:)\ x \]

　次のように定義されていると考えると分かりやすいかもしれません。

\[\begin{eqnarray*}
x \cdot ε &=& x \\
x \cdot (y:a) &=& (x \cdot y):a
\end{eqnarray*}\]
　これは、連接の定義のyの部分にεと(y:a)を与えることで確認できます。

挿入関数(insertion)

挿入関数η : Σ → Σ*は自然数の1に対応するもので、次のように定義されます。
\[ η(a) = ε:a \]

　空列に文字aを追加する関数ですが、これは文字aを長さ1の文字列aへ変換する操作を表しています。

（３）諸性質の整理

　（２）で指数関数・連接・挿入関数を定義しました。これらには次のような関係があります。

指数法則（右指数法則と左指数法則）

\[ f^{x \cdot y} = f^x \cdot f^y \\ \ ^{x \cdot y}f = \ ^yf \cdot \ ^xf \]

挿入関数と指数関数の関係

\[ f^{η(a)} = f(a) \]

連接と挿入関数の関係

\[ x:a = x \cdot (η\ a)\]

　２、3番目の性質は、それぞれ自然数における1乗したら底になるという性質の、3番目の性質は、自然数における後者関数が1を足す関数であるという性質の一般化になっています。

証明（右指数法則と左指数法則）

\[ f^{x \cdot y} = f^x \circ f^y \\ ^{x \cdot y}f = f^y \circ f^x \]
これはyについての帰納法で示される。
上の等式について行います。
・εのとき
\[ f^{x \cdot ε} = f^x \circ f^ε \]

これはεが単位元であること、fのε乗が単位元になることから示されます。

・y:aのとき

\[ f^{x \cdot (y:a)} = f^x \circ f^{y:a} \]

左辺を展開して右辺と等しくなることを示します。

\[\begin{eqnarray*} f^{x \cdot (y:a)} &=& f^{(x \cdot y):a} \\  &=&f^{x \cdot y} \circ f (a) \\  &=&(f^x \circ f^y) \circ f(a) \\&=& f^x \circ (f^y \circ f(a)) \\&=& f^x \circ f^{y:a} \end{eqnarray*}\]

下の等式は上の式とほとんど同じなので省略します。

証明（挿入関数と指数関数の関係）

fを任意のモノイドMへの関数f : Σ → M とします。
\[f^{η(a)} = f^{ε:a} = f^ε \cdot f( a) = f(a)\]

証明（連接と挿入関数の関係）

右辺が左辺と等しくなることを示します。

\[ x \cdot (ε:a) = (x \cdot ε):a = x:a \]

（４）モノイドであることの証明

　文字列の集合Σ*は連接と空列についてモノイドです。つまり、次の条件を満たします。

・単位元

\[x \cdot ε = x = ε \cdot x \]

・結合法則

\[ x \cdot (y \cdot z) = (x \cdot y) \cdot z \]

　単位元について証明しましょう。左辺がxに等しくなることは定義から明らかです。右辺がxに等しくなることはxについての帰納法で示されます。

証明（単位元）

・εのとき

\[\begin{eqnarray*}
ε \cdot ε &=& ε
\end{eqnarray*}\]

・(x:a)のとき

\[\begin{eqnarray*}
ε \cdot (x:a) &=& (ε \cdot x) : a \\
&=& x : a
\end{eqnarray*}\]

　εのときは、空列が右単位元であることから明らかです。また、(x:a)のときは、二行目で帰納法の仮定を使用しているところに注意してください。

　結合法則について証明しましょう。これは左辺を展開することで右辺と等しくなることが示せます。

証明（結合法則）

\[\begin{eqnarray*}
x \cdot (y \cdot z) &=& \ ^{y \cdot z} (:)\ x \\
&=& \ ^z(:) \circ \ ^y(:)\ x \\
&=& \ ^z(:)(\ ^y(:)\ x) \\
&=& (x \cdot y) \cdot z \\
\end{eqnarray*}\]
　この証明を見ると、左指数法則が結合法則を与えていることが確認できます。

（５）自由であることの証明

　文字列Σ*の集合がΣを基底とする自由モノイドであることは、任意のモノイドMへの関数f : Σ → M に対して、モノイド準同型 f^ : Σ* → M がただ一つ存在し次を満たすことを意味します。

\[ f^＾ \circ η = f\]

　これの証明は実はほとんど済んでいます。まず、f^をfを底とする右指数関数と置けば、f^は空列を単位元に写すことと、指数法則からモノイド準同型です。最後のηも挿入関数とおけば、（３）で示した挿入関数と指数関数の関係で示されています。

　最後に残るのは、f^の一意性の証明です。

　gをf^の条件を満たす関数とします。

\[ g(ε) = e \\ g(x \cdot y) = g(x) \cdot g(y) \\ g(η(a)) = f(a)\]

　これがf^と等しいことを示せば、f^が一意的であること示されます。そのためには、f^が始代数性から定義された関数であることを使います。つまり、gがf^の定義における条件を満たすことを示せば、g = f^が成り立つということです。
\[ g(ε) = e \\ g(x:a) = g(x) \cdot f(a) \]
　上の式は、gがモノイド準同型であることから示されます。下の式は次のように確認できます。
\[ g(x:a) = g(x \cdot (η\ a)) = g(x) \cdot g(η\ a) = g(x) \cdot f(a)\]
以上でg = f^が示され、文字列が自由モノイドであることが示されました。