mikamix/catamorphism.md

## catamorphism.md

      
    Raw
  

              catamorphism.md
            
          
    始代数とcatamorphism


自己紹介


三上遼
0x20歳
IoTの会社でスマートロック作ってます
数学弱いです
twitter @mikamix
facebook Ryo Mikami


今日のお話


(だいたい) foldの話です


始代数とは


(だいたい) List a = Nil | Cons a List のことです


Catamorphismとは


(だいたい) foldのことです


今日話すこと


始代数とCatamorphismをListに具体化してお話しします
(なるべく) 簡単にしました
(なるべく) 圏論を知らなくてもわかるようにしました


今日話さないこと


(たぶん) List以外のCatamorphismについて
Catamorphismの一般化
圏論の深い話


fold的な

(b, a -> b -> b) を取って [a] -> b を返す関数
fold :: (b, a -> b -> b) -> [a] -> b

len :: [a] -> Integer
len = fold (0, inc)

sum :: [Integer] -> Integer
sum = fold (0, (+))

つまり

foldに(f, g)を渡すと [a] -> b が返る
     [A]
      |
      | fold (f, g)
      v
1 -> Int <- A * Int
  f       g


[A] はどうやって作られるか

  nil    cons
1 -> [A] <- A * [A]
      |
      | fold (f, g)
      v
1 -> Int <- A * Int
  f       g


あらあら

なんか上と下似てますね
  nil    cons
1 -> [A] <- A * [A]
      |
      | fold (f, g)
      v
1 -> Int <- A * Int
  f       g


一般化してみましょう

  nil    cons
1 -> [A] <- A * [A]
      |
      | fold (f, g)
      v
1 ->  B  <- A * B
  f       g


下の部分をいっぱい作ります

  nil    cons
1 -> [A] <- A * [A]
      |
      | fold (f, g)   <-- (f, g)に対して一意に定まる
      v
1 ->  B  <- A * B     <-- ココをいっぱい作る
  f       g


これは圏じゃ!

  nil    cons
1 -> [A] <- A * [A]   <- ココも対象
      |
      | fold (f, g)   <-- ココが射
      v
1 ->  B  <- A * B     <-- ココが対象
  f       g 


上は始対象


任意の対象に対してちょうど一つの射が存在するような対象

  nil    cons
1 -> [A] <- A * [A]   <- ココが対象で
      |
      | fold (f, g)   <-- 下の対象に対して一意
      v   
1 ->  B  <- A * B     <-- ココも対象
  f       g 


上はF-始代数


上と下をF-代数と呼ぶ
fold (f, g) はF-代数の射
F-代数の圏における始対象をF-始代数と呼ぶ
始代数からの射をCatamorphismと呼ぶ

  nil    cons
1 -> [A] <- A * [A]   <- F-代数の圏の始対象
      |
      | fold (f, g)   <-- F-代数の射
      v
1 ->  B  <- A * B     <-- ココがF-代数
  f       g 


左と右を繋げます

Before
  nil    cons
1 -> [A] <- A * [A]   <- F-代数の圏の始対象
      |
      | fold (f, g)   <-- F-代数の射
      v
1 ->  B  <- A * B     <-- ココがF-代数
  f       g 

After
    (nil, cons)
[A] <---------- 1 + A * [A]
 |
 | fold (f, g)
 v
 B  <---------- 1 + A * B
    (f, g)


整理します

Before
    (nil, cons)
[A] <---------- 1 + A * [A]
 |
 | fold (f, g)
 v
 B  <---------- 1 + A * B
    (f, g)

After
  in
X <---------- 1 + A * X
|
| (|phi|) <- バナナ
v
B <---------- 1 + A * B
  phi


もう少し整理します

F(X) = 1 + A * X
Before
  in
X <---------- 1 + A * X
|
| (|phi|) <- バナナ
v
B <---------- 1 + A * B
  phi

After
in
X <---------- F(X)
|
| (|phi|)
v
B <---------- F(B)
phi


今日は(たぶん)この辺で

  in
X <---------- F(X)
|             |
| (|phi|)     | F((|phi|))
v             v
B <---------- F(B)
  phi