F-algebra と catamorphism を Haskell で理解する(2)

前回の続き。

wikipedia の F-algebra のページ http://en.wikipedia.org/wiki/F-algebra 参照。

上記ページに F(X) = 1 + X という関手の F-algebra の例で (N,[zero,succ]) が出てくる。Haskell で書くと

type N = Int

a :: Maybe N -> N
a Nothing = 0
a (Just x) = x + 1

本当は N は自然数なので負の数も入っている Int とは違うけれどここでは Int でごまかしておく。
a Nothing = 0 の部分が zero に、a (Just x) = x + 1 の部分が succ に対応する。

さて F-algebra (N,a) から別の F-algebra (B,b)
b :: Maybe B -> B
に対する射 f はどんなものになるだろう。
a は全単射なので逆写像 inv_a をとることができる。 

inv_a :: N -> Maybe N
inv_a 0 = Nothing
inv_a x = Just (x-1)

写像なので
a・inv_a == id
F-algebra の射 f が満たすべき性質
f・a == b・F(f)
に右から inv_a をつなぐと
f・a・inv_a == b・F(f)・inv_a
a・inv_a == id だから

f = b・F(f)・inv_a
これと Maybe の fmap f の性質
fmap f Nothing == Nothing
fmap f (Just x) == Just (f x)

を使って

f 0 == b $ fmap f $ inv_a 0 == b $ fmap f Nothing == b Nothing
f x == b $ fmap f $ inv_a x == b $ fmap f (Just (x-1)) == b (Just (f (x-1)))
    == (b.Just) (f (x-1))
つまり
f :: N -> B
f 0 = b Nothing
f x = (b.Just) (f (x-1))

具体的にみていくと

f 1 == (b.Just) (f 0) == (b.Just)$b Nothing
f 2 == (b.Just) (f 1) == (b.Just)$(b.Just)$b Nothing
f 3 == (b.Just) (f 2) == (b.Just)$(b.Just)$(b.Just)$b Nothing
...
なので
f x は b Nothing に (b.Just) をx回適用した値、
つまり iterate を使って書くと

f :: N -> B
f x = (!!x) $ iterate (b.Just) $ b Nothing

例えば B として Int、b として

b :: Mabye Int -> Int
b Nothing = 1
b (Just x) = 2 * x

とすると F-algebar (N,a) から F-algebra (Int,b) への射 f は

f :: N -> Int
f x = (!!x) $ iterate (2*) 1

と一意に定まる。(実際には f x = 2^x である)


この F-algebra (N,[zero,succ]) ように任意の F-algebra に対して射が必ず存在して一意であるときこの F-algebra は initial algebra と呼ばれる。initial algebra は F-algebra のなす圏での始対象(initial object) であることと同じ意味である。
また initial algebra からの射(必ず存在して一意)を catamorphism と呼ぶ。
上の例でいえば

f :: N -> Int
f x = (!!x) $ iterate (2*) 1

は F-algebra (Int,b) への catamorphism である。


ところで F-algebra の射 f が満たすべき性質
f・a == b・F(f)
の両辺を Just x に作用させると
f (a (Just x)) == b (Just (f x))
Just は空気のような存在だと思えば大体
f・a == b・f
である。この式や「x回適用」という方法どこかで見たことがあると思ったら圏論勉強会 でやった Conceptual Mathematics の session 11 1 S○圏(実際はSの右上にくるっとした矢印)圏の定義や session 15 3 Naming arbitrary elements にでてきていた。
Conceptual Mathematics 深いなあ。


多分また続く。