今週も圏論勉強会ではない方の圏論勉強会 第10回に来ています。資料とustreamは公開されています。
- とびいりの話は大歓迎なので、面白い話がある人は面白くなくても言って下さい
- 13回目もやる(12回だとモナドに入れない。最終回はモナド)
- ワークスアプリケーションズさんに感謝
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の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になっている。
- 型関手
- 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]
- 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)の導出(今回で初めて示せるようになったフュージョン)
- 来週からはガラっと新しい話題
- 「カリー・ハワード対応をやります」
- べき対象
