Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

今日は 圏論勉強会 第10回 の日です

今週も圏論勉強会ではない方の圏論勉強会 第10回に来ています。資料ustreamは公開されています。

coq4ios / 講師 @keigoi さん

  • たまに仕事でcoq使う
  • 大体の機能使える
  • 開発中なので、ビルド方法とかリプライ飛ばして聞いて下さい
  • Mac OSのシミュレータ上でも動きます

第10回: 始代数・終余代数と不動点,型函手 / 講師 @9_ties さん

  • 復習: Lambekの補題(F始代数は同型射)
    • List は F X = 1 + A * X
    • [A] = F ([A])ということ。右辺は、 1 + A * [A] = Maybe (A, [A])
    • つまり [A] = Maybe (A, [A])。
    • f Nothing = , f (Just (a ,as)) = a:as。f' = Nothing, f' (a:as) = Just (a, as)。
    • F Tが定義部、Tが定義したもの。同型なのは当たり前
  • T = F T ・・・不動点ぽい!
  • 始代数をμF、終余代数をνFと表す(一般的な記法)
  • 始代数と終余代数の復習。catamorphismとanamorphism。帰納的データ型、余帰納的データ型
  • 待遇を取ると、不動点がなければ始代数、終余代数はない
  • 復習: cpo D上の連続関数Fの最小不動点は、lim F^i(⊥)
    • 一般化すれば、μFを具体的に構成できる
    • 例えば、F X = 1 + Xの始代数は自然数、というのを具体的に構成できる
    • μFも最小不動点とも呼ぶ
  • 自己関手Fのinitial ω-chain → !:0→F0について、0→F0→FF0→...と構成
    • 「反応がないということはついてきてないということですね」「とても入門でやる話ではないですね」
    • cpoの始対象は⊥、射は≦なので、一般化になってる
  • 例: Setsにおいて、 F X = X + {*}とすると、始代数が自然数になっている
    • 始対象φ、終対象{*}
    • φ→{*}→{* *}→...
    • 射は、!、!+1、!+1+1
  • 始対象のあるω余完備の圏Cと、ω余連続な自己関手f:C→Cについて、μF=lim F^i(0)
    • 例としてはcpo
    • initial ω-chain について、余極限があり、それを保存すると弱めてもOK
    • ωより大きな基数を使うように弱めてもOK
    • 「数学って美しいなと思ってくれれば」
  • 証明
    • μF:=lim F^i(0)が始代数であることを示す
    • 余連続なので F(μF) = F(limF^i(0))=limF^(i+1)(0)=μF
    • 余極限なので、錐を(lim F^i(0), q_i)とおく
    • Fで写したF(μF)の錐も余極限になる。(FμF, F(q_i))から(μF, q_i)への唯一の射をinとおく
    • x:FX→Xを任意のF代数とする
    • initialω-chainからX→FX→FFX→...を経由させることで、Xを頂点とする錐が作れる
    • この錐への唯一の射uがとれる。これを使いμ.inとx.Fuを作れるが、F(μF)が余極限なので唯一性からこれらは等しい
    • uの唯一性も同様に示せる
  • 終余代数は最大不動点となる(すべて先ほどの双対)
  • 具体的な構成方法が得られるのが重要
    • 圏論では「・・・を満たすもの」とよく言うが、通常はどんなものか例示されない
    • 具体的な構成方法があれば、証明に利用しやすい。
    • 理解も深まる。数学では直観が大事
  • Haskellでの例
    • data ListF a x = Nil | Cons a x (注: 再帰使ってる通常の定義でない)
    • deriving Functor すると、fmap (+ 1) (Cons 0 1) == Cons 0 2 が使える
    • data Fix f a = f (Fix f a)・・・と書きたいが、data Fix f a = In {out :: f (Fix f a)}
    • type List a = Fix (ListF a) とすれば、リストができる
    • nil = In Nil、cons a as = In (Cons a as)。Showのインスタンスは自分で作る
    • 図式から、cata :: Functor f => (f a -> a) -> Fix f -> a、cata phi = phi . fmap (cata phi) . out
    • このcataがfoldになっている。
  • 型関手
    • 不動点とは関連なし。データ型に関係。モナドにも?
    • catamorphismに基づいて定義可能。mapのようなものの運算
    • 双関手(bifunctor) F:D×C→Cが材料。Cが同じなのがミソ
    • Dの部分を固定して、F_A:C→Cを得る
    • F(X, Y) = 1 + X * Yとすると、F_A X = 1 + A * X
  • F_Aの始代数(T_A,in_A)が存在するとする
    • 対象AをT_Aに写す
    • f:A→BをT(f) = (| in_B . F(f, 1_B) |)
  • 例: F(A, X) = 1 + A × Xとすると、T_Aは[A]
    • (|in . F(f,1) |) == (| [nil, cons] . (1 + f * 1) |)
    • == (| [nil, cons . (f×1) |) == foldr (cons . (f * 1)) nil 。これはmap
  • Listだけでなくいろいろな型に使える。型関手と呼ぶ
  • catamorphismの反射と融合則の復習
  • (|f|).T(g) = (|f.F(g,1)|)
    • マップしてからの畳込みは1つの畳込みにできる
    • 例: foldr (+) 0 . map (+ 1)をfoldr (\a x -> (a + 1) + x) 0 とできる
    • 証明は、f.F(g, (|f|))の分解順序を変えればよい
    • これを使えば、関手となることの証明は簡単
  • 練習として、二分木の型関手、融合則の導出。map f.map g == map (f. g)の導出(今回で初めて示せるようになったフュージョン)
  • 来週からはガラっと新しい話題