符号付き文字列が自由群であることの証明

　この記事では符号付き文字列というものを導入し、これが自由群であることを証明します。そのために、次のような順序を踏みます。
（１）符号付き文字列の始代数による整理
（２）指数関数、連接・逆連接、挿入関数の定義
（３）諸性質の整理
（４）群であることの証明
（５）自由であることの証明

（１）符号付き文字列の始代数による整理

　符号付き文字列は、文字集合が与えられたとき、符号付き文字（正の文字と負の文字）の有限列からなる集合です。また、列を構成している2つの隣接する符号付き文字が、符号が異なり値が等しいときは打ち消し合います。

　たとえば、"+a-b+c"は符号付き文字列です。また、"+a-b+b-c"は-bと+bが打ち消し合うための条件を満たすので、"+a-c"へ約分（reduction）されます。

　文字の集合をΣとして、符号付き文字列の集合をΣ^±1とします。この記法は一般的ではないので注意してください。Σ^±1は次のように再帰的に定義されます。
・空列εはΣ^±1上の符号付き文字列である。
・aがΣ上の文字、xがΣ^±1上の符号付き文字列のとき、x:+aとx:-aはΣ^±1上の符号付き文字列である。
・Σ^±1上の符号付き文字列は、以上の操作のみによって構成される。

　以上の3つの条件では、打ち消し合う性質が与えられていません。そのため、consに逆演算の性質を与えます。2番目の条件で文字を符号付き文字列に追加する操作として、(:+)と(:-)が現れました。これらは、次のような関数の定義を与えます。
\[(:+) : Σ^{±1}×Σ → Σ^{±1} \\ (:-) : Σ^{±1}×Σ → Σ^{±1}\]
　この2つが逆演算であるという条件を最後に加えることで、打ち消し合う条件が与えられます。つまり、任意の文字aと符号付き文字列xについて、次が成り立つということです。
\[ x:+a:-a = x = x:-a:+a\]
　(:+)と(:-)をそれぞれ、正のconsと負のconsと呼びましょう。

　以上の再帰的定義から次の始代数性が与えられます。
　任意の集合Xとその定数c、可逆な演算h : X × Σ → X が与えられたとき、次の漸化式を満たす関数f : Σ^±1 → X がただ一つ存在する。
\[\begin{eqnarray*}
f(ε) &=& c \\
f(x:+a) &=& h(f(x), a)\\
f(x:-a) &=& h^{-1}(f(x), a)
\end{eqnarray*}\]

　hは可逆であるという条件がありました。次のようなh^-1が存在するということです。

\[ h(h^{-1}(x, a), a) = x = h^{-1}(h(x,a),a)\]

　この性質は別の「逆演算について」の記事で整理されているので、詳しくはそちらを参照してください。

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

　（１）で与えられた始代数性から、いくつか関数を与えることができます。まずは、指数関数を与えます。

　ここで、f を Σから 任意の群Gへの関数 f : Σ → G とします。群Gでは、単位元はe、乗法は・、xの逆元はx^-1で表されるとします。このとき、次の条件を満たすような、fを底とする指数関数Σ^±1 → Gを２つ（右指数関数f^と左指数関数^f）を定義できます。

右指数関数

\[\begin{eqnarray*}f^ε &=& e \\f^{x:+a} &=& f^x \cdot f(a) \\f^{x:-a} &=& f^x \cdot (f(a))^{-1} \\\end{eqnarray*}\]

左指数関数

\[\begin{eqnarray*}^ε f&=& e \\ ^{x:+a}f &=& f(a) \cdot \ ^af\\ ^{x:-a}f &=& (f(a))^{-1} \cdot \ ^af\\\end{eqnarray*}\]

　3つ目の条件ではf(a)の逆元を掛けています。

連接・逆連接

　ここでは、consを底とする指数関数を考えることで、2つの二項演算（連接と逆連接）を導入します。連接は通常の文字列の足し算のようなものですが、逆連接はいわば引き算のようなものです。次で証明するように、これらは群における乗法と除法に対応します。

　連接・逆連接は、それぞれ次のように定義される「正のconsを底とする左指数関数」と「負のconsを底とする右指数関数」を使います。

正のconsを底とする左指数関数

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

負のconsを底とする右指数関数

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

　ここで登場している(:+a)と(:-a)はconsが与えた、負または正の文字aを追加する単項演算子です。これらは合成すると恒等関数になることから、群上の逆元の関係にあります。そのため、それぞれの定義は以上のようになります。

　xを任意の符号付き文字列として、単項演算^x(:+)と(:-)^xについて少し説明しましょう。^x(:+)は各符号付き文字列の後ろ（右）に、xをそのまま追加する演算です。(:-)^xは各符号付き文字列の後ろにに、xの逆の順序と逆の符号で追加する演算です。

　これらを使って、符号付き文字列上の二項演算子である連接・と逆連接／を次のように定義します。

\[\begin{eqnarray*}x\cdot y &=& \ ^y(:+)\ x \\x / y &=& (:-)^y \ x \\\end{eqnarray*}\]

　これらの漸化式を定義から確かめましょう。次のようになります。

・連接・

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

・逆連接／

\[\begin{eqnarray*}x/ ε &=& x \\x/ (y:+a) &=& (x:-a) / y \\x/ (y:-a) &=& (x:+a) / y \end{eqnarray*}\]

挿入関数η

文字の集合から符号付き文字列への挿入関数というものを定義します。これは各文字aを長さ1の符号付き文字列"+a"へ写す関数η : Σ → Σ^±1です。次のように定義されます。
\[ η(a) = ε:+a\]
　これは整数では1に対応するものです。

（３）諸性質の整理

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

・右指数法則

\[ f^{x \cdot y} = f^x \cdot f^y \\
f^{x / y} = f^x \cdot (f^y)^{-1} \]
・左指数法則
\[\ ^{x \cdot y}f = \ ^yf \cdot \ ^xf \\
\ ^{x / y}f = (^yf)^{-1} \cdot \ ^xf\]

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

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

連接と挿入関数の関係

\[ x:+a = x \cdot η(a) \\
x:-a = x / η(a)) \]

　「挿入関数と指数関数の関係」はfの"+a"乗はf(a)になるという意味で、整数におけるxの1乗はxであるという性質に対応します。また、連接と挿入関数の関係は正の文字aを追加するという操作は"+a"を連接すること、負の文字aを追加する操作は"+a"を逆連接すること（これは"-a"を連接と等しくなる）と等しいという意味で、整数における後者関数が+1と等しいこと、前者関数が-1と等しいことと対応します。
　証明については、文字列のものとほとんど同じなのでほとんど省略しますが、一つだけ行います。

証明

\[ f^{x / y} = f^x \cdot (f^y)^{-1} \]

これをyについての性質として帰納法で示します。

・εのとき

　これは、x / ε = x と fのε乗が単位元になることから明らかです。

・(y:+a)のとき

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

　1行目から2行目は、帰納法の仮定から導かれます。3行目から4行目は、逆元の積は順序を入れ替えた積の逆元であるという群の性質によって導かれます。

・(y:-a)のとき

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

　その他の指数法則はこれの多少形を変えたものなので、証明は難しくありません。

（４）群であることの証明

　ここでは、群の公理について通常の逆元による公理ではなく、別の記事「逆元による群と除法による群」で与えた除法についての公理を採用します。今までの定義で符号付き文字列上の逆元は導入されていませんが、除法が与えられていること、また、証明が容易であるというのが理由です。逆元は(ε/x)によって与えられます。

　符号付き文字列は群になります。乗法は連接、除法は逆連接、単位元は空列です。群であるとは、これらが次の条件を満たすということです。

・単位元

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

・乗法の結合法則

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

・逆演算

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

・除法の結合法則

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

　上2つの条件についての証明は、文字列のときとほとんど同じなので省略します。下2つの条件がモノイドから群へ拡張するときに加わった条件になります。これらの条件について、定義から次のように書き換えることができます。

・逆演算

\[\ ^y(:+) \circ (:-)^y = id_{Σ^{±1}} = (:-)^y \circ \ ^y(:+)\]

・除法の結合法則

\[\ ^z(:-) \circ (:+)^y = (:-)^{y/z} \]

　この書き換えの正当性は各式に符号付き文字列xを与えることで直ちに確認できます。

　逆演算についての条件は、負のconsを底とする指数関数と正のcosnを底とする指数関数が逆演算の関係にあることを示しています。（正のconsと負のconsは逆演算でしたが、指数関数は確かめていません）また、除法の結合法則は、右指数法則と負のconsが正のconsの逆演算であることから導かれます。

　それでは、負のconsを底とする指数関数と正のconsを底とする指数関数が逆演算であることを示しましょう。

証明

\[\ ^x(:+) \circ (:-)^x = id_{Σ^{±1}} = (:-)^x \circ \ ^x(:+)\]

　xについての帰納法で示します。

・εのとき

　これは自明です。

・(x:+a)のとき

　左辺

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

　1行目から２行目は帰納法の仮定から導かれます。

　右辺

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

・(x:-a)のとき

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

以上で、群の条件を確認できました。

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

　これは、右指数関数が、挿入関数と合成したら底になる、群の準同型になっているという2つの条件を満たすこと、そして、その条件を満たす関数はただ一つであることを示すということです。

　挿入関数と合成したら底になることは（３）の「指数関数と挿入関数の関係」ですでに示しました。群の準同型であるとは、次を満たすことです。

\[ f^ε= e \\ f^{x \cdot y} = f^x \cdot f^y \\ f^{x/y} = f^x \cdot (f^y)^{-1} \]

　以上の条件はすでに示しました。

　ただし、通常の群における準同型は逆元を逆元に写すことです。符号付き文字列xの逆元に相当するのはε/xです。3つ目の条件に当てはめれば、通常の準同型の定義を満たすことが確認できます。

　最後にそれがただ一つであることを示します。これは自由モノイドのときとほとんど同じで、始代数であることが効いてきます。

　gが挿入関数と合成したら底になる、群の準同型になっているという条件を満たすとします。つまり、次の条件をgは満たします。

\[g(η(a)) = f(a) \\ g(ε) = e \\ g(x \cdot y) = g(x) \cdot g(y) \\ g(x/y) = g(x) \cdot (g(y))^{-1}\]

　以上の性質から、gは次の性質を満たします。

\[g(ε) = e \\ g(x:+a) = g(x) \cdot f(a) \\ g(x:-a) \cdot (f(a))^{-1} \]

　この証明には、連接と挿入関数の関係と挿入関数と合成したら底になるという性質から示すことができます。

　確認したように、右指数関数が満たすので上の性質を満たします。この3つの等式は、始代数における漸化式と一致しています。そのため、これはただ一つであることが示されます。

モナドとコモナドについて

モナドとコモナド

　逆演算という概念を導入するために、積コモナドという道具を使いました。このコモナドというのは圏論の概念で、モナドの双対概念として登場します。これらを数学に導入する意義はいくつかあるのですが、ここでは、型の条件から合成できそうにないものについて、合成を定義できることくらいにとらえるといいと思います。モナドとコモナドの定義は、２つの操作と2つ条件からなります。逆演算の記事では、条件については触れませんでした。
　ただし、ここで紹介するのは、歴史的にはクライスリトリプルというもので、モナドの通常の定義（単位元＋乗法）とは異なっているので注意してください。

積コモナド

　集合Xを任意に固定します。このとき、各集合Aに対して積A × Xを考えることができます。これに次の2つの操作を加えたものが、集合Xが与える積コモナドです。

・余単位元ε
　任意の集合Aに対して、ε_A : A × X → A を次のように定義する。
\[ ε_A (a, x) = a \]
・余拡張†
　任意の関数f : A × X → B に対して、f^† : A × X → B × X を次のように定義する。
\[ f^†(a, x) = (f(a, x), x)\]

合成

　これらの操作を考えることの意義は関数の合成を考えることができることです。関数f : A × X → B と 関数 g : B × X → C が与えられたとき、素朴に考えればf と g を合成することはできません。f の 余ドメイン（B）と g のドメイン（B × X）が等しくないからです。このようなとき、余拡張を使うと次のように合成することができます。

\[g \circ f^† : A × X → C \]
　これはfを余拡張することで、fの余ドメインがB×Xになりgのドメインと一致するからです。A × X の値(a, x)を与えると次のようになります。
\[g \circ f^† (a, x) = g(f(a, x), x)\]
　以上のことは「逆演算について」で触れたことです。しかし、これらがきちんと「合成」の条件を満たしていることを確かめなければなりません。

合成の条件

　通常の関数の合成については恒等関数の単位元性と結合法則という2つの条件が必要です。

・恒等関数の単位元性
\[ f \circ id_A = f =  id_B \circ f \]
・結合法則
\[(h \circ g) \circ f = h \circ (g \circ f) \]
　恒等関数というものが通常の関数にはありますが、積コモナドにおいてこれに相当するものが余単位元です。積コモナドではこれらの条件に対応する条件があります。
・余単位元の単位元性
\[ f \circ ε_A^† = f = ε_B \circ f^†\]
　これは次のように言い換えられます。
\[ε_A^† = id_{A×X} \]
・結合法則
\[(h \circ g^†) \circ f^† = h \circ (g \circ f^†)^† \]

　これは次のように言い換えられます。

\[g^† \circ f^† = (g \circ f^†)^† \]

　それぞれの条件について簡潔に言い換えたものを加えました。コモナドは圏論で定義される概念ですが、実はこの簡潔な条件の方が、コモナドの条件になっています。簡潔な条件の方が証明などにおいて簡単ですが、意味的にはわかりにくいので、あえて、関数の合成の条件に類比させて述べておきました。証明は簡単なのでここでは省略します。

コモナドの条件

　さきほどの合成の条件をコモナドの条件として整理します。余単位元と余拡張は次の2つの条件を満たしていなければなりません。

\[ε_A^† = id_{A×X} \\ g^† \circ f^† = (g \circ f^†)^† \]

ベキモナド

　モナドの例もここで紹介しましょう。各集合Aについてその冪集合Pow(A)を考えることができ、次の2つの操作が与えられます。

・単位元

　任意の集合Aに対して、η_A : A → Pow(A) を次のように定義する。
\[ η_A (a) = \{a\} \]

・拡張

　任意の関数f : A → Pow(B) に対して、f^＃ : Pow(A) → Pow(B) を次のように定義する。
\[ f^＃ (A') = \bigcup_{a \in A'}f(a) \]

合成

　関数f : A → Pow(B) と 関数 g : B → Pow(C) が与えられたとき、合成は次のように定義します。

\[ g^＃ \circ f : A → \mathcal{P}(C) \]

　Aの値aを与えると次のようになります。

\[ g^＃ \circ f (a) = \bigcup_{b \in f(a)}g(b)\]

合成の条件

　合成の条件は次のようになります。２つの表現で書かれているのは、先ほどの合成との類比と簡潔なものです。

・単位元の単位元性
\[ f^＃ \circ η_A = f = η_B^＃ \circ f \\
η_A^＃ = id_{\mathcal{A}} \]
・結合法則
\[(h \circ g)^＃ \circ f = h^＃ \circ (g^＃ \circ f) \\ (h \circ g)^＃ = (h^＃ \circ g)^＃ \]

プログラミングにおけるモナド

　HaskellではMaybeモナドというものが標準で用意されています。これは、次のような方です。

Maybe a ::= Just a | Nothing

　これを使うと、たとえばaからbへの部分関数fを次のように表現できます。

f :: a -> Maybe b

f x | defined     = Just f(x)

     | undefined = Nothing

　モナドを使うと、これらを合成することができます。Maybeモナドの単位元と拡張は次のようなものです。

・単位元

 return :: a -> Maybe a

 return x = Just x

・拡張

 f :: a -> Maybe b に対して、 >>=f :: Maybe a -> Maybe b は次のような関数です。

 (>>=f) Just x    = f(x)

          Nothing  = Nothing

　これらもモナドの条件を満たします。

参考文献

　モナド・コモナドについては、次のものが参考になると思います。

・数学セミナー2011.12 圏論の歩き方(第5回)モナドと計算効果 勝股 審也

・モナドへの近道・Haskell からの寄り道 2007 中村翔吾 

・圏論によるプログラミングと論理 灘高パソコン部2013年部誌

　また、積コモナドについては、次のものを参考にしました。

・Should I use a Monad or a Comonad? 2012 Dominic Orchard 

補足

　積コモナドは逆演算を定義するために導入したもので、逆演算については次の記事を見てください。

逆演算について

始代数について

始代数について
　始代数とは再帰的定義もしくは帰納的定義を一般化したものとして考えることができます。これは圏論の概念から生まれたものなので、圏に関する概念、圏、関手、始対象などの知識があると簡潔に述べることができるのですが、再帰的定義との関連から整理することでも理解できると思います。
　再帰的定義や帰納的定義は自然数や文字列で使われ、コンピュータ科学（計算理論）では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への関数を定義できることを示しています。本来、関数の定義をする場合は、すべての引数に対して返値がただ一つ定まる規則を与えなければなりませんが、自然数の場合は、これだけでいいということなので、これえはかなり強力です。
　このブログにおける自然数や文字列の議論でも、いくつかの演算子を定義するときにこの性質を利用しています。
　なぜ、この２つの条件だけでいいのかを形式的に示すのは、多少込み入っているので、再帰性についての専門的な文献を参照してください。

符号付き文字列について

符号付き文字列について

文字列の拡張

  ある文字の集合はある操作によって文字列の集合を与えます。この文字列について代数的な視点で見れば、モノイドという代数構造を持つこと、文字とのあいだに自由という関係があることを確認しました。符号付き文字列はこれを群に拡張したものに相当するものです。

符号付き文字列の直観的な説明

  直観的な説明から与えましょう。通常の文字列は文字の有限列として捉えることができます。符号付き文字列の場合は、符号がついた文字の有限列です。ここで言われている「符号sign」とは「符号付き整数」などで使われている符号のことで、符号付きであるとは、それらに「正 positive」と「負 negative」のいずれかが付与されていることを意味します。つまり、正の文字と負の文字を考えて、それらの有限列を考えたものが符号付き文字列です。

符号付き文字列の例

  例えば"+a-b+c"や"+d-e"といったものが符号付き文字列です。各文字について符号（プラス+とマイナス-）が付与されています。
　単純に２種類の符号を与えるだけではありません。正と負には互いに打ち消し合う性質を与えます。符号付き文字列の場合は、正の文字と負の文字が隣接していて、その値（つまり、符号を無視した文字）が等しい場合は、打ち消し合います。たとえば、"+a+b-b+c"という符号付き文字列は2文字目と3文字目がそのような関係にありますので、この文字列は"+a-c"という文字列と「等しい」という定義を与えます。

符号付き文字列が群構造を持つこと

  このような性質を与えることで、符号付き文字列は群の構造を持ちます。つまり、任意の符号付き文字列について、連接したら空列になるような符号付き文字列が存在するということです。たとえば、"+a-b+c"という符号付き文字列は"-c+b-a"という符号付き文字列と連接したら、次のように空列になります。

"+a-b+c"+"-c+b-a"= "+a-b+c-c+b-a" = "+a-b+b-a" = "+a-a" = ""

符号付き文字列の定義

　文字列の場合は、空列とconsから再帰的に定義することで文字列を定義することができました。再帰的に定義したので、帰納法による証明をすることができたり、始代数性から再帰的な関数の定義を与えることができたりと、扱いやすい性質を持っていました。符号付き文字列の場合は、consを拡張することでそれが達成されます。consとは文字列に文字を追加する操作を表すものでした。符号付き文字列の場合は、追加する文字に符号が加わるので2つのconsが考えられます。これを正のconsと負のconsと呼びましょう。打ち消し合う性質を与えるためには、正のconsと負のconsが「逆演算」であるという条件を与えることで達成されます。この「逆演算」については、次の記事を参照してください。

逆演算について

符号付き文字列が群であること

　ここでは形式的な証明は行いませんが、その概要を述べておきます。文字列の場合は、consを底とする指数関数が連接になりました。同様に、正のconsを底とする指数関数を考えることができ、これが符号付き文字列上の連接になります。負のconsを底とする指数関数を考えると連接の逆演算（乗法に対しては除法に相当するもの）が現れます。文字列の連接を足し算と考えたときは、これは引き算になるでしょう。次のような計算になります。

"+a-b+c" - "+c" = "+a-b+c-c" = "+a-b"

"+a-b+c" - "-b+c" = "+a-b+c-c+b" = "+a"

　このように符号を反転・順序を反転して連接させるという演算が現れます。これにより群の構造を持っていることを示すためには、従来の群の公理（モノイド＋逆元）ではなく、別の記事で導入した群の公理（モノイド＋除法）が簡単です。逆元を作る場合には、この引き算（除法）から定義することになるので、遠回りになるからです。

逆元による群と除法による群

証明の要

　文字列の場合では、指数関数の性質が直接モノイドの条件に変化することがありました（たとえば、指数法則が結合法則へ）。そのように、除法の条件（逆演算性と結合性）は、それぞれ、正のconsと負のconsの逆演算であることと、指数法則から直接導かれます。

整数について

　整数も特殊な符号付き文字列であると考えられるので、再帰的に定義することができます。正のconsと負のconsに対応するのは、後者関数successorと前者関数predecessorです。逆演算であるというのはこの場合は逆射関係になります。また、連接に対応するのは足し算＋でその逆は引き算-になります。

　従来の代数の議論では整数を定義する場合は、自然数の組を考えて、その同値類を取るという人工的な方法を取ることが多いですが、おそらくこの方が自然であると思われます。

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

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

（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^が示され、文字列が自由モノイドであることが示されました。

自然数と文字列の対応関係

自然数と文字列の対応関係

自然数の集合と文字列の集合は、両者とも自由モノイドなので対応関係があります。たとえば、0と空列はモノイド単位元です。このようにいくつか対応項が作れるので、ここでまとめてみましょう。文字が1種類しかない場合を考えたときの文字列の集合が自然数に相当しているので、これにより対応関係を調べることができます。

自然数	文字列
0	ε
σ	(:)
1	η
(+)	(・)

0とε

0と空列εは、お互いモノイドの単位元であること、また再帰的定義における構成子（初期値）としても対応しています。

σと(:)

σは自然数上の後者関数（successor）、(:)は文字列に文字を追加するconsです。両者ともに、再帰的定義における構成子です。

1とη

ηは挿入関数（inclusion）と呼ばれる文字集合から文字列集合への関数で、各文字aを長さ1の文字列aへ返す関数です。構成子から次のように定義されます。
\[ η(a) = a:ε\]
　同様に1もσ0として定義されます。

(+)と(・)

(+)は自然数上の足し算、(・)は文字列上の連接で、両者ともにモノイド乗法として共通しています。両者ともにσまたは(:)を底とする指数関数を考えることで定義することができます。詳しくは、指数関数の一般化に関する記事を参照してください。

それぞれの関係

自然数と文字列の間に4つの対応項があることを確認しました。これら4つは基本的な構成要素といえるでしょう。4つの間には指数関数によってある関係があります。それをここでまとめましょう。

自然数

\[ 1 = σ0 \\
 m + n = σ^m\ n \\
σm = 1 + m \]

文字列

\[ η(a) = a:ε \\
 x \cdot y = (:)^x\ y \\
a:x = η(a) \cdot x \]

掛け算について

自然数上の掛け算(×)は次のように定義することができます。
\[ (×) : \mathbb{N} × \mathbb{N} → \mathbb{N} \\
m × n = m^n\]
　右辺が通常の意味での指数関数にならないことに注意です。自然数は、任意のモノイドの元を底とする指数関数を考えることができました。ここでは、任意のモノイドとして単位元を0、乗法を+とする自然数を選んだということです。通常の指数関数の場合は、モノイドの二項演算を乗法として考えるので指数関数という表現を使いましたが、加法として考える場合は、直観的には掛け算になります。

文字列の掛け算について

自然数上の掛け算の類似から、あえて文字列Σ*上の掛け算を考えると次のようになります。
\[ (×) : Σ^* × \mathbb{N} → Σ^* \\
x × m = x^m
\]
　これは、文字列xをm回連接する計算です。連接を加法としてとらえる場合は左辺の表記が、乗法としてとらえる場合は右辺の表記がいいでしょう。

掛け算の性質

自然数上の掛け算の性質が文字列へ一般化できるものをまとめましょう。自然数上の次の性質が一般化できます。
\[ m × 0 = 0 \\ m × 1 = m \\ m × (n_1 + n_2) = m × n_1 + m × n_2\]
　ただし、自然数上の掛け算が可換であるからといって、これを入れ替えてはいけません。文字列上では可換性は失われます。
　以上の性質に対応する文字列上の性質は次のようになります。
\[ x × 0 = ε \\ x × 1 = x \\ x × (n_1 + n_2) = (x × n_1) \cdot (x × n_2) \]

自由モノイドについて

自由代数について

符号付き文字列というものを導入するというまでの道すじには自由代数の視点がありました。コンピュータ科学上では文字と文字列というものを対象にします。この2つは代数の視点から見れば、基底と自由モノイドという関係に言い換えることができます。代数の視点に立ったときに、モノイドから群への拡張をコンピュータ科学上でも行えるのではないかという着想が得られました。それを、この記事の上で再現するというのがこの記事、そして他の関連する記事の試みです。
　この記事では、文字と文字列の関係を代数の視点から整理するということを行います。その整理が行われたとき、群への拡張は自然に思えるでしょう。

文字と文字列の関係

文字と文字列の関係は、代数の視点から見れば、基底と自由モノイドという関係に重ねられます。これはコンピュータ科学上で行われる文字から文字列を再帰的に定義するというものとは異なる条件によって定式化されます。ここでは、それに関係する文字と文字列の代数的な関係をここでまとめてみましょう。

文字列がモノイドであること

文字の集合をΣとするとき、Σ上の文字の文字列の集合をΣ*と表します。文字列の集合上には連接と呼ばれる結合的な二項演算が定義され、また、連接における単位元である空列というものが存在します。これらの条件は文字列がモノイドであることを示しています。
　これは自然数の指数関数に関する性質の一般化になっています。そのため、自然数の指数関数についての性質を確認することが、理解の助けになるかもしれません。
自然数上の指数関数について

挿入関数η

各Σの文字aについて、長さ1のΣ*上の文字列aを返す関数が存在します。直観的にはあまりに自明な関数ですが、これは両者を代数的に関係づける上で重要な役割を担います。これを挿入関数ηとして定義されます。
\[ η : Σ → Σ^*\]

指数関数

Mを乗法・と単位元eを持つ任意のモノイドとします。また、f を任意のΣからMへの関数f : Σ → M への関数としたとき、次のようなモノイド準同型f^ : Σ* → M がただ一つ存在します。
\[ f^{η(a)} = f(a) \]

　ポイントフリーに書き換えると次のようになります。
\[ f^＾ \circ η = f\]

　f^がただの関数ではなく、モノイド準同型であるとは次の条件を満たすことを意味しています。
\[ f^ε = e \\
f^{x \cdot y} = f^x \cdot f^y\]

　一般的にはこのような呼び方はされませんが、これをfを底とする指数関数と呼びましょう。
　指数関数が存在することは、文字列の集合の始代数性から証明することができますが、これは多少長くなることですので、別の機会に譲ります。

指数関数の直観的な意味

定義や性質だけを与えたので、多少f^が分かりにくいですが、適当な文字列を与えれば、f^がどのような関数かが分かるでしょう。たとえば、文字列"abcd"をf^に与えると次のように展開されます。
\[ f^{abcd} = f(a) \cdot f(b) \cdot f(c) \cdot f(d) \]

（補足）自由モノイドから自由群へ

以上の自由モノイドの定義は群へ拡張するのはとても簡単です。モノイドの部分を群に書き換えるだけで達成されます。しかし、文字列が文字から再帰的に定義することは、群の場合は、多少面倒なことをしなければなりません。しかし、再帰的に定義される文字列が自由モノイドであることを証明することが、どのように定義すれば自由群を作ることができるかについて、示唆を与えるでしょう。

自然数上の指数関数について

自然数の代数的性質について

自然数は代数の視点から見れば、一元集合（要素を一つしか持たない集合）を基底とする自由モノイドです。この代数的条件を身近なレベルにまで書き下すと、これは底と指数関数に関する性質を表しています。ここでは、まずは指数関数の性質をいくつか整理して、それらを代数の言葉に翻訳するということを行います。これは文字列にも拡張できるので、文字列の代数的性質への理解の補助線を与えるでしょう。

自然数がモノイドであること

自然数上には足し算＋という結合的な二項演算が存在し、また、0という足し算について単位元である特別な数も存在します。これらの条件は、自然数がモノイドであるということを意味しています。

自然数と指数関数

指数関数の定義

Nを自然数の集合、Mを乗法・と単位元eを持つ任意のモノイドとします。Mの任意の元xが与えられたとき、xを底とする指数関数x^ : N → M を次のように定義できます。
\[\begin{eqnarray*}
x^0 &=& e \\
x^{n+1} &=& x \cdot x^n \\
\end{eqnarray*}\]
　このように関数が定義できることは、自然数の始代数的な性質から直ちに示せるのですが、ここでは直接関係しないので、他の記事に譲ります。また、この後に示すいくつかの性質も自然数の定義から証明することができます。

底と指数関数の関係

指数関数と底の間には次のような関係があります。
\[ x^1 = x \]
　つまり、1乗すると底になるということです。

指数法則

指数関数は次のような法則を満たします。
\[ x^0 = e \\ x^{m+n} = x^m \cdot x^n \]

指数関数の一意性

底と指数関数の関係と指数法則を満たすような、自然数からモノイドMへの関数はただ一つしか存在しません。

自然数と自由モノイド

底と指数関数の関係、指数法則、一意性というこれらの条件が自然数が一元集合の自由モノイドであるということを意味しています。自由モノイドの条件とこれらの対応を確認しましょう。一元集合の自由モノイドであるとは次のように表されます。

　自然数は定数1が存在し、任意のモノイドMの元xに対して次のようなモノイド準同型x^ : N → M がただ一つ存在する。
\[ x^1 = x\]

　底と指数関数の関係はほとんどそのまま表れているのが確認できるでしょう。モノイド準同型であるというのが指数法則に対応しています。一意性についても同じです。

補足

文字列の場合は文字集合を基底とする自由モノイドが文字列になります。このとき変化しているのは基底です。その結果、定数1とモノイドの元xという部分が変化します。
　文字列における定数1に対応するのが挿入関数（文字を長さ1の文字列に返す関数）です。また、モノイドの元xは、文字からモノイドへの任意の関数に変わります。詳しくは、別の記事で整理しているのでそれを参照してください。
自由モノイドについて

逆元による群と除法による群

群の公理について

群の公理は通常は各元が逆元を持つモノイドとして与えられます。逆元から乗法の逆の演算である除法を定義することができます。たとえば、整数の引き算は符号を反転した数を足すという演算として導入できます。これの逆を考えることはできないでしょうか。つまり、除法を持つモノイドとして群を考えて、逆元を除法から考えるということです。
　それは可能です。この記事では、２つの群の公理の定式化を行い、それが同値であることを示します。

２つの群の公理

まず、通常の群の公理から確認します。

逆元による群の公理

集合Gは次のような二項演算・と定数eを持つ。
・乗法は結合的
\[ x \cdot (y \cdot z) = (x \cdot y) \cdot z \]
・eは単位元
\[ x \cdot e = x = e \cdot x\]
・逆元の存在
\[x^{-1} \cdot x = e = x \cdot x^{-1} \]
　ただし、x、y、zはGの任意の元です。
　これに代わると思われる除法による群の公理は次のようなものです。

除法による群の公理

集合Gは次のような二項演算・と二項演算／と定数eを持つ。
・乗法は結合的
\[ x \cdot (y \cdot z) = (x \cdot y) \cdot z \]
・eは単位元
\[ x \cdot e = x = e \cdot x\]
・除法は乗法の逆演算
\[ (x \cdot y) / y = x = (x / y) \cdot y \]
・乗法と除法は結合的
\[ (x \cdot y) / z = x \cdot (y / z) \]
　ただし、x、y、zはGの任意の元です。

　逆元の条件の部分が、除法について２つの条件に置き換わりました。また、逆演算という言葉については、次を参照してください。

• 逆演算について



2つの公理が同じ代数を与えること

この２つの公理が同じ代数の定義を与えることを示しましょう。次の２つを行います。

（１）逆元による群から除法を定義して、それが除法の条件を満たすことを確かめる。

（２）除法による群から逆元を定義して、それが逆元の条件を満たすことを確かめる。

　

（１）

　Gを逆元による群の公理を満たす代数であるとします。

除法の定義

G上で次のような二項演算／を定義します。

\[ x / y = x \cdot y^{-1}\]

　これが除法の条件を満たすことを示しましょう。

逆演算であること

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

　左辺と右辺がそれぞれxに等しくなることを示します。

左辺

\[\begin{eqnarray*} (x \cdot y) / y &=& (x \cdot y) \cdot y^{-1} \\ &=& x \cdot (y \cdot y^{-1}) \\ &=& x \cdot e \\ &=& x \end{eqnarray*}\]

右辺

\[\begin{eqnarray*} (x / y) \cdot y &=& (x \cdot y^{-1}) \cdot y \\ &=& x \cdot (y^{-1} \cdot y) \\ &=& x \cdot e \\ &=& x \end{eqnarray*}\]

結合的であること

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

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

\[\begin{eqnarray*} (x \cdot y) / z &=& (x \cdot y) \cdot z^{-1} \\ &=& x \cdot (y \cdot z^{-1}) \\ &=& x \cdot  (y / z) \end{eqnarray*}\]

　以上で（１）は達成されました。

（２）

　Gを除法による群を満たす代数であるとします。

逆元の定義

各元xに対してx^-1を次のように定義します。
\[ x^{-1} = e / x\]

　これが逆元の条件を満たすことを示します。

逆元の条件

\[x^{-1} \cdot x = e = x \cdot x^{-1} \]

　左辺と右辺がそれぞれeと等しくなることを確かめます。

左辺
\[\begin{eqnarray*} x^{-1} \cdot x &=& (e / x) \cdot x \\ &=& e \end{eqnarray*}\]

右辺

\[\begin{eqnarray*} x \cdot x^{-1} &=& x \cdot (e / x) \\ &=& (x \cdot e) / x \\ &=& (e \cdot x) / x  \\ &=& e \end{eqnarray*}\]

　以上で（２）が達成されたので、２つの群の公理が同値であることを確かめられました。

除法による群の公理について

　通常は除法による群の公理というのは行われません。私の調べる限りでは、そのような仕事を見つけることはできなかったので、以上の公理化は自前で行いました。このような仕事がなかった背景には、需要がないこと、逆元に比べて複雑であること、この２つが主要であると思われます。この２つの状況について、この公理が持っている可能性について説明しましょう。
　まず、需要についてですが、この公理化の意義を説明することで回答になるでしょう。これは群を構成するときに有効です。たとえば、ある集合から自由群を生成する場合にそれが群であることを確かめるときに、除法の公理を確かめるほうが簡単です。自然数から整数を構成する場合も同様です。
　別の記事で、符号付き文字列というものを与える予定です。文字集合から再帰的な定義により与えた自由群です。これが群であることを示すために、演算を定義するのですが、再帰的に与えた場合は、除法の方が先に出てきます。また、その証明も除法による群の公理のほうが容易です。
　次に、その複雑さについてですが、逆演算はコモナドの視点からかなり自然に定式化できます。それについては先程も参照を与えましたが、次の記事で示しています。

• 逆演算について

これにより、合成して単位元になるという形で逆演算というものを定義できます。

逆演算について

足し算と引き算のような関係は積コモナドにより定式化ができます。整数Z上の足し算+と引き算-を考えます。

\[ (+) : \mathbb{Z} × \mathbb{Z}→ \mathbb{Z} \\ (-) : \mathbb{Z} × \mathbb{Z}→ \mathbb{Z}\]
積コモナド(_×Z)を考えます。余単位元εと余拡張^†は次のようになります。
・余単位元ε
任意の集合Xに対してε_X : X × Z → X は
\[ ε_X : X × \mathbb{Z} → X \\ ε_X(x, n) = x \]
これは射影に相当します。

・余拡張^†
任意の関数f : X → Y × Z に対してf^† : X × Z → Y × Z は
\[ f^† : X × \mathbb{Z} → Y × \mathbb{Z} \\ f^† (x, n) = (f(x, n), n) \]

足し算+と引き算-は次のように合成すると余単位元になるという関係にあります。
これは、積コモナドが与える余クライスリ圏上で合成すると恒等射になるという関係を表します。
\[ (+) \circ (-)^† = ε_\mathbb{Z} = (-) \circ (+)^†\]

各式に２つの整数の組(m, n)を与えると次のようになります。
\[ (m - n) + n = m = (m + n) - n\]

確認しましょう。

・左辺
\[\begin{eqnarray*} (+) \circ (-)^† (m, n) &=& (+) ((-)^{†}(m, n)) \\&=& (+) ((-)(m, n), n) \\ &=& (+) (m - n, n) \\&=& (m - n) + n \end{eqnarray*} \]
・中辺
\[\begin{eqnarray*}ε_\mathbb{Z} (m, n) &=& m \end{eqnarray*} \]

・右辺
\[\begin{eqnarray*} (-) \circ (+)^† (m, n) &=& (-) ((+)^{†}(m, n)) \\&=& (-) ((+)(m, n), n) \\ &=& (-) (m + n, n) \\&=& (m + n) - n \end{eqnarray*} \]