４． F-代数
今回はあまり聞きなれてはいないと思われるF-代数( F-algebra )について学んでみよう。代数という名が示すとおり、これは、半群、モノイド、群、環などの代数を表現するための重要な役割を担っているが、それにもまして、数学的帰納法による再帰的表現において重要な役割を果たしてくれる。一般に、再帰的表現は、記述を平易化し、読みやすくしてくれ、さらには証明をしやすくしてくれるが、F-代数はその道具を与えてくれる。
それでは累計、フィボナッチ数(Fibonacci number)、素数などを例にあげながら、F-代数と数学的帰納法を活かしたプログラミングについて見ていこう。
４．１ F-代数の定義
F-代数とは、圏\(\mathcal{C}\)とその上での自己関手\(F: \mathcal{C} \rightarrow \mathcal{C}\)に対して、\(\mathcal{C}\)の対象\(A\)とその射
\begin{eqnarray}
α: F(A) \rightarrow A
\end{eqnarray}
の組\( (A,α) \)のことを言う。そして、\(A\)を台集合(carrier)、\( α \)を評価射(evaluation function, structure map )と呼ぶ。図で表すと次のようになる。
例１ 自然数
定義はいたって簡単だ。例を挙げて理解を深めることにしよう。最初に自然数を考える。自然数は、\(0\)から始まる無限な整数の集まりだ(中学・高校では\(1\)からと学んだと思うが、\( 1 \)を別の意味で使うので、紛らわしさを避けるために、ここでは\(0\)からにする)。
そこで集合の圏\( \mathbf{Set}\)を考えることにしよう。この集合において、\( 1 \)を終対象とし、\( + \)を\( \mathbf{Set} \)上での直和とする。そして\(F: \mathbf{Set} \rightarrow \mathbf{Set}\)を自己関手とし、これは集合\(X\)を「\( 1 \)あるいは\(X\)」に移すものとしよう。ここで「\( 1 \)あるいは\(X\)」は直和\( + \)を用いて、\( 1 + X\)と表すことにしよう。
つぎに\(X\)から\(1+X\)に移すための二つの射を用意しよう。そしてここでは台集合を自然数とするので、その集合を\(\mathbb{N} \)で表す。二つの射は\( 0\)と\(succ \)で、次に示すように、\( 0\)は終対象\( 1 \)を自然数の始まりに移し、また\(succ \)は次の自然数を得る。
\begin{eqnarray}
0 &:& 1 \rightarrow \mathbb{N}; * \mapsto 0, \\
succ &:& \mathbb{N} \rightarrow \mathbb{N}; n \mapsto n+1
\end{eqnarray}
これにより、\([0,succ]:1+ \mathbb{N} \rightarrow \mathbb{N} \)となる。
したがって自然数は、\(F: X \rightarrow 1+X\)を自己関手とし、\( ( \mathbb{N}, [0,succ] ) \)を組みとするF-代数となる。
Haskellで実装してみよう。
まずF-代数の定義で出てきた評価射\( α \)にたいして、次のようなデータ型\(Algebra\)を用意しよう(ちなみにHaskellではControl.Functor.Algebraというパッケージがある)。
type Algebra f a = f a -> a
つぎは関手\(F\)をデータ型を用いて表現することだ。これは、\(F:X \rightarrow 1+X\)で、\( [0,succ] \)という二つの射で表わした。すなわち\(0:1 \rightarrow \mathbb{N} \)と\(succ:\mathbb{N} \rightarrow \mathbb{N} \)だ。ここでは\(F\)を\(NatF\)とし、次のように代数的データ型を用いて定義する(ここでは、任意のデータ型\(a\)で定義しておき、評価射のところで台集合を自然数\(\mathbb{N} \)とする)。
data NatF a = Zero | Succ a
さて\(F\)が定まったので、評価射を具体的に定義しよう。\(F\)の台集合を自然数の代わりに便宜的に整数¥(I nt ¥)とし、評価射\(algN\)を次のように定めよう。
algN :: Algebra NatF Int algN Zero = 0 algN (Succ n) = n + 1
これを用いて実行してみよう。
例２ モノイド(足し算と掛け算)
次の例はモノイドだ。モノイドの定義はいくつかあるが、古典的な定義は、集合\(M\)の上に次の二つの射をもち、結合律と単位律を満たすことだ。なお\(1\)は自然数のときに用いた終対象だ。
\begin{eqnarray}
μ &:& M \times M \rightarrow M; x + y \mapsto z \ (if \ addition), \\
η &:&1 \rightarrow M; * \mapsto 0 \ (if \ addition)
\end{eqnarray}
これより\( [η, μ]:1 + M \times M \rightarrow M\)となり、\(F: X \rightarrow 1 + X \times X \)である。なお\(+\)は自然数のときと同様に直和だ。
Haskellでこれを実現しよう。\(η\)を\(MEmpty\)とし、\( μ\)を\(MAppend\)とする。そして\(F\)を新たなデータ型\(MonF\)で表すことにしよう。
data MonF a = MEmpty | MAppend a a
整数の足し算は、評価射\(algP\)を用意し、次のように定義すればよい。
algP :: Algebra MonF Int algP MEmpty = 0 algP (MAppend m n) = m + n
図で示すと次のようになる。
同様に整数の掛け算は次のように用意できる。
algM :: Algebra MonF Int algM MEmpty = 1 algM (MAppend m n) = m * n
\(MonF\)でのデータコンストラクタ\(MEmpty, MAppend\)が射となっていることを確認しておこう。
例３ 環(加算と乗算)
加算と乗算が成り立つ世界を環と呼ぶ。もう少し詳しく説明すると、集合\(R\)の上に二つの演算\(+\)と\( \times\)が用意されていて、\(+\)がアーベル群、\(\times\)が半群(またはモノイド)のとき、\( (R,+,\times) \)の組を環という。
モノイドは、演算を\(\circ\)としたとき、次を満たすものである(半群は単位元がなくてもよい)。
1) 任意の\(a,b\)に対して、\(a \circ b \in R\)
2) 結合律( \( (a \circ b) \circ c = a \circ (b \circ c)\) )を満たし、
3) 単位元( \(i \in R \))を有し、単位律( \( i \circ a = a = a \circ i \))を満たす。
アーベル群とは上記の性質に加えて、次を満たすものである。
4) 任意の\(a\)に対して逆元 \( (a^{-1}) \)を有する。なお、逆元とは\( a \circ a^{-1} = i \)を満たすものである。
5) 可換律(\( a \circ b = b \circ a \))を満たす。
従ってアーベル群は
\begin{eqnarray}
μ &:& M \times M \rightarrow M; x + y \mapsto z \ (if \ addition), \\
η &:&1 \rightarrow M; * \mapsto 0 \ (if \ addition) \\
ι &:& M \rightarrow M; x \mapsto (-x) \ (if \ addition)
\end{eqnarray}
に加えて、単位律、結合律、可換律を満たすものである。
このためアーベル群では自己関手\(F\)は\(F: 1 + X + X \times X\)となる。またモノイドでは\(F: 1 + X \times X\)であったので、環では\(F: 1 + 1 + X + X \times X + X \times X\)となる。
整数の上での加算\(+\)と乗算\(\times\)を有するF-代数を、新しいデータ型\(RingF\)を用いて次のように定義しよう。
data RingF a = RZero | ROne | RNeg a | RAdd a a | RMul a a
評価射を\(algR\)で表すことにすると、次のようになる。
algR :: Algebra RingF Int algR RZero = 0 algR ROne = 1 algR (RNeg m) = - m algR (RAdd m n) = m + n algR (RMul m n) = m * n
例４ 多項式の環
多項式も環となる。演算(\(+, \times\))は次のように定義できる。
\begin{eqnarray}
\sum^{n}_{i=0} a_i x^i + \sum^{n}_{i=0} b_i x^i = \sum^{n}_{i=0} (a_i + b_i) x^i \\
\sum^{n}_{i=0} a_i x^i \times \sum^{m}_{j=0} b_j x^j = \sum^{n+m}_{k=0} (\sum_{i+j=k}a_i b_j) x^k
\end{eqnarray}
これに対するデータ型は、次のようになる。
data Expr = RZero | ROne | RNeg Expr | RAdd Expr Expr | RMul Expr Expr
４．２ 不動点
F-代数において、自己関手\(F\)を適応し続け、その前後で変化がなくなったとき、これを不動点\(Fix(F)\)と呼ぶ。
厳密に定義すると、自己関手\(F\)の不動点(fixed point)とは、
\begin{eqnarray}
F(Fix(F)) = Fix(F)
\end{eqnarray}
となるような\( Fix(F)\)である。
Haskellでは次のように定義できる。
newtype Fix f = Fix (f (Fix f))
ところで等号の左側の\(Fix\)は型コンストラクタだが、右側の最初の\(Fix\)はデータコンストラクタである。これは、下図に示すように、射として\(f (Fix \ f) \)を\(Fix \ f \)に写像する。
\(Fix\)とは逆の射、すなわち\(Fix \ f \)を\(f (Fix \ f) \)に写像する射\(unFix\)も用意しておこう。
unFix :: Fix f -> f (Fix f) unFix (Fix x) = x
ここで\(unFix : Fix (F) \rightarrow F(Fix (F)); Fix(x) \mapsto x \)である。
不動点の定義より、
\begin{eqnarray}
Fix \circ unFix = id \\
unFix \circ Fix = id
\end{eqnarray}
であることに注意しておこう。
４．３ Lambekの定理
台集合\(A\)と評価射\(α:F(A) \rightarrow A\)の対( \( (A, F(A) \rightarrow A \) )をF-代数と定めた。それでは、二つの代数が存在したときに、片方の代数の構造が他方の代数の構造の中で保持されているという性質をどのように記述したらよいのかについて考えよう。構造が保たれるということは、圏論の世界では大切な性質で、たとえば関手はこの役割を担っている。
F-代数の圏
いま二つのF-代数( \( A, α:F(A) \rightarrow A \) )と( \( B, β:F(B) \rightarrow B \) )があったし、前者の代数の構造が、後者の代数の構造の中で保持される条件を考えることにしよう。
対象\(A\)から対象\(B\)への射を\(m\)とする。上の図で\( F(A) \)から\(B\)を得ることを考える。経路は二つある。上側の経路を辿ると\(β \circ F(m) \)となる。これは後者の代数の方に移って計算するというものである。下側の経路を辿ると\(m \circ α\)である。これは前者の代数で計算した後で、その値を後者の値に変えるというものである。これが一致することが、構造を保持するための約束なので、次の式を得る。
\begin{eqnarray}
β \circ F(m) = m \circ α
\end{eqnarray}
ある代数の構造が別のある代数の構造の中で保たれるとき、準同型(homomorphism)であると言い、その条件は上に示した式である。これより\(F\)代数\( (A, α:F(A) \rightarrow A) \)と\( (B, β:F(B) \rightarrow B) \) を圏とした時に、\(m\)が関手であれば二つの圏は準同型となる。そして上図は可換図式となる。
そして準同型を射として構成した圏をF-代数の圏と呼ぶ。上図であれば\(m\)が射、( \( A, α:F(A) \rightarrow A \) )と( \( B, β:F(B) \rightarrow B \) )が対象となる。
始代数
F-代数の圏が始対象を有するならば、その始対象をF-始代数と呼ぶ。これまで例で挙げてきた自然数、足し算や掛け算のモノイド、加算と乗算からなる環などはF-始代数の例である。
それではLambekの定理を示そう。これはF-始代数に関するものだ。
Lambekの定理
F-代数の圏において、台集合が始対象\(I\)のとき、\(F(I)\)と\(I\)は同型(isomorphic)である。
証明
\(I\)が始対象であることから、\(I\)の中に複数の要素が含まれていたとしても、それらは同型であることに注意して証明を行う。\(I\)が始対象であることから、\(I\)から\(F(I)\)に対してただ一つの射が存在する。これを\(m\)としよう。また評価射を\( j : F(I) \rightarrow I \)とすると、\(F(I)\)と\(I\)が同型であることを示すには、
\begin{eqnarray}
j \circ m = id_I \\
m \circ j = id_{F(I)}
\end{eqnarray}
であることを示せばよい。それでは次の可換図式を用いて証明しよう(この可換図式はF-代数の圏である)。
下側の横方向の射の合成\( j \circ m \)は\(I\)から\(I\)への射であり、\(I\)の任意の要素はお互いに同型なので、これは恒等射となる。すなわち\(j \circ m = id_I \)である。
上側の横方向の射の合成\( F(j) \circ F(m) \)は\(F(I)\)から\(F(I)\)への射であり、\( f(j) \circ F(m) = F (j \circ m) = F(id_I) = id_{F(I)} \)より、これは恒等射となる。(証明おわり)
これより、\( I \)と\( F(I) \)が同型であることから、\(I\)が不動点であることが分かる。すなわち、
\begin{eqnarray}
j &:& F(I) \rightarrow I \ \ (cf \ Fix : F (Fix (F)) \rightarrow Fix (F)) \\
m &:& I \rightarrow F(I) \ \ (cf \ unFix : Fix (F) \rightarrow F (Fix (F))
\end{eqnarray}
となり、\(j\)は\(Fix\)であり、\(m\)は\(unFix\)である。また\(Fix(F)\)が台集合であることにも注意して欲しい。
４．４ Catamorphism
F-代数で表された自然数は、1)出発点となるものと、2)任意の\(n\)という数とその次の数との関係、を用いて定義した。すなわち始まりの値\(0\)と、任意の数\(n\)が与えられたときにその次の数\(n+1\)が求められるように定めた。このように定義されたものからは、最初に初めの数\(0\)を用意し、それに次の数を求める方法を適応して\(1\)を求め、さらにこれを適応して\(2\)を求めるということを繰り返す。
これは高校の頃に習った数学的帰納法だ。これまで説明した方法を一般化し、数学的帰納法をより自然な形で表して、利用できるようにしたのがCatamorphismである(残念ながらCatamorphismに対する日本語は用意されていない)。
F-代数の圏の性質
下図のように、F-始代数\( (Fix (F),F (Fix (F)) \rightarrow Fix (F)) \)とF-代数\( (A,α:F(A) \rightarrow A) \)を用意しよう。これはF-代数の圏なので下図は可換図式である。
左側はF-始代数であることから、\( F (Fix (F))\)と\(Fix (F) \)は同型であり、\( Fix . unFix = id_{Fix (F)} \)かつ\( unFix . Fix = id_{F(Fix (F))} \) とする\(unFix : Fix (F) \rightarrow F (Fix (F)) \)が存在する。また\(unFix (Fix \ x) = x \)である。
さらに\( Fix F \)が始対象であることから、\(A\)への射が存在する。これを\(m\)としよう。これにより\( F (Fix F) \)から\(F (A) \)への射は\(F(m)\)となる。
左側のF-始代数\( (Fix (F),F (Fix (F)) \rightarrow Fix (F)) \) と右側のF-代数\( (A,α:F(A) \rightarrow A) \)が準同型であることから、
\begin{eqnarray}
m = α . F(m) . unFix
\end{eqnarray}
となる。
上記の式が数学的帰納法を与えるが、これを実際の例で追っていこう。
例１ 加算
それではモノイドでの加算を利用してHaskellを用いて具体的に見ていくこととしよう。モノイドでの加算はこれまで用いていたものではなく、リストを用いることにしよう。
data ListF a b = Nil | Cons a b
これは自己関手なので、次のように\(Functor\)のインスタンスとする。
instance Functor (ListF a) where fmap f Nil = Nil fmap f (Cons e lst) = Cons e (f lst)
さらにF-代数や不動点に関しても定めておこう。
type Algebra f a = f a -> a newtype Fix f = Fix ( f (Fix f)) unFix :: Fix f -> f (Fix f) unFix (Fix x) = x
\(ListF\)の評価射を\(sumAlg\)とすると、この射は次のようになる。
sumAlg :: Algebra (ListF Int) Int sumAlg Nil = 0 sumAlg (Cons e acc) = e + acc
さらに射\(m\)を\(cata \ alg\)としよう。ここで、\(alg\)は評価射である。次のようになる。
cata :: Functor f => Algebra f a -> Fix f -> a cata alg = alg . fmap (cata alg) . unFix
ここまでのプログラムはまとめると次のようになる。
type Algebra f a = f a -> a newtype Fix f = Fix ( f (Fix f)) unFix :: Fix f -> f (Fix f) unFix (Fix x) = x cata :: Functor f => Algebra f a -> Fix f -> a cata alg = alg . fmap (cata alg) . unFix data ListF a b = Nil | Cons a b instance Functor (ListF a) where fmap f Nil = Nil fmap f (Cons e lst) = Cons e (f lst) sumAlg :: Algebra (ListF Int) Int sumAlg Nil = 0 sumAlg (Cons e acc) = e + acc
それではプログラムの動きを見てみよう。
最初は何もない状態から始まるので、次のようになっている。これはF-代数の圏なので可換図式である。
まず左下のところから説明しよう。ここは始対象が入る場所だ。\( N il \)がそのような役割を担うが、不動点であるので\( Fix \ N il \)となる。この値を求めたいのだが、下側の射\( (cata \ sumAlg) \)からは直接求めることができないので、上側の経路を経て値を得る。
すなわち\(unFix (Fix \ N il) \)を利用して、左上の\(N il\)を得る。次に\(fmap \ (cata \ sumAlg) \ N il = N il \)によって、右上の\(N il\)を得る。これを評価射\(sumAlg\)で値を得ると、右下の0となる。
それでは、これに\(e\)という値を加える場合を考えてみよう。下図のようになる。
左下は\(Cons\)によってこれまでのものに\(e\)を追加するということになる。これまでのものは先ほどの\(Fix \ N il\)である。またここは不動点であるので、前のときと同じよう\(Fix\)をつけて\(Fix \ $ \ Cons \ e \ (Fix \ N il) \)となる。
これを\(unFix\)で持ち上げると、左上の\( Cons \ e \ (Fix \ N il) \)となる。これに\(fmap \ (cata \ sumAlg) \) を施すと、
\begin{eqnarray}
&& fmap \ (cata \ sumAlg) \ (Cons \ e \ (Fix \ N il)) \\
&=& Cons \ e \ ( (cata \ sumAlg) \ (Fix \ N il)) \\
&=& Cons \ e \ N il
\end{eqnarray}
より、右上は\( Cons \ e \ N il \)となる。これを評価射\(sumAlg\)で値を得ると、右下の\(e\)となる。
さらに、\(d\)を加える場合の可換図式は以下のようになる。
そして一般化した可換図式は次のようになる。
例２ フィボナッチ数
次はフィボナッチ数を考えてみよう。これは、\(1,1\)で初めて、先行する二つの数の和を次の値とするものだ。すなわち\(1,1,2,3,5,8,13,21…\)である。
それではこれをCatamorphismを利用してプログラムを作成しよう。用意するデータ型は自然数と同じように、最初の値を決めるものと、その後の続きを決めるものとを用意する。
data NatF a = Zero | Succ a
これは自己関手なので\(Functor\)のインスタンスとする。
instance Functor NatF where fmap f Zero = Zero fmap f (Succ a) = Succ (f a)
評価射を\(fib\)とすると
fib :: Algebra NatF (Int, Int) fib Zero = (1,1) fib (Succ (m, n)) = (n, m + n)
プログラムを実行するために、不動点を次のように定める。
lstFib :: Fix NatF lstFib = Fix $Succ (Fix $ Succ (Fix $ Succ ( Fix $ Succ (Fix Zero))))
実行してみよう。
４．５ Anamorphism
これまでに説明してきたCatamorphismに対して双対なのが、Anamorphismである。F-代数の矢印を全て反対にすると、次のようにF-余代数を得ることができる。
用語の定義
AnamorphismがCatamorphismに対して双対であることから、Catamorphismの中で用いた用語に対して、双対の用語を定義できる。それらをまとめると次のようになる。
F-余代数：\(F\)を圏\(\mathcal{C}\)上の自己関手\(F: \mathcal{C} \rightarrow \mathcal{C} \)とするとき、\(\mathcal{C}\)の対象\(A\)と射\(α:A \rightarrow F(A) \)の組\( (A,α) \)の組である。
F-余代数の準同型：F-余代数\( (A,α:A \rightarrow F(A) ) \)から別のF-余代数\( (B,β:B \rightarrow F(B) ) \)への準同型の射とは\(\mathcal{C}\)の射\(m:A \rightarrow B \)であって、これは\( F(m) \circ α = β \circ m \)を満たす。これよりある自己関手\(F\)に対して、F-余代数全体は圏をなす。そしてF-余代数の準同型射を一般にAnamorphismという。そして準同型を射として構成した圏をF-余代数の圏と呼ぶ
F-終余代数：自己関手\(F\)に対するF-余代数の圏が終対象を有するとき、その終対象をF-終余代数と呼ぶ。F-余代数の終対象は、不動点である(不動点には最大なものと最小なものがあり、厳密には、Catamorphismのときは最小不動点、Anamorphismのときは最大不動点である)。
下図で、左側はF-終余代数で右側はF-余代数である。
用語の定義が住んだので、Haskellでプログラムを作ってみよう。最初に余代数\(Coalgebra\)を定義しよう。
type Coalgebra f a = a -> f a
次に準同型射\(m\)を定義する。ここではCatamorphismのときと同様に、評価射\(α\)を\(coa\)とし、\(m\)を\( a na \ coa \)としよう。
ana :: Functor f => Coalgebra f a -> a -> Fix f ana coa = Fix . fmap (ana coa) . coa
Catamorphismのときは、\(ListF\)を用意したが、今度は\(StreamF\)を用意しよう。\(ListF\)は空のリストから始まったが、\(StreamF\)は無限な長さのストリームだ。次のように定義する。
data StreamF e a = Stream e a
\(Functor\)のインスタンスにしよう。
instance Functor (StreamF e) where fmap f (Stream e a) = Stream e (f a)
それでは素数を得ることを考えよう。エラストテネスは自然数のリストがあったとき、素数にたいしてその倍数を除くということを原理にしている。より詳細に説明すると、２で始まる整数のリスト\(lst\)を用意しておき、\(lst\)の先頭を素数としておりだし、先頭を除いたリストからその倍数を除いたリストを新たなリストとして、この操作を繰り返す。そして得られた素数の列はストリームの中に納める。
それではプログラミングしてみよう。ここでは上の図の右側のF-余代数の部分の評価射を考えることにしよう。\(A\)のところは整数のリスト\(p:ps\)で、先頭\(p\)は素数である。\(ps\)はそれを除いた残りのリストである。
これに対して評価射を施したのが\(F(A)\)である。ここではエラストテネスの古いを施すこととなるので、評価射を\(era\)となずけよう。データ型はストリーム\(StreamF\)となる。ストリームの最初の要素はもちろん素数の\(p\)だ。次の要素は倍数を除いたリストだ。倍数を取り除く処理を\(filter\)を用いて表すと次のようになる。
era :: Coalgebra (StreamF Int) [Int] era (p:ps) = Stream p (filter (\a -> mod a p /= 0) ps)
これより素数の列\(primes\)は
primes = ana era [2..]
しかしこれはストリームになっているので、表示することができない。ストリームをリストにするためには、Catamorphisumを用いる。これは次のようになる。
ary :: Algebra (StreamF Int) [Int] ary (Stream e a) = e:a
