読者です 読者をやめる 読者になる 読者になる

北海道苫小牧市出身の壮年PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

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

レポート math

元祖圏論勉強会ではない方の圏論勉強会 第13回の最終回です。資料ustreamは公開されています。

第13回: 随伴・モナド / 講師 @9_ties さん

  • モナドが途中で終わるのは嫌でしょう」「随伴を説明しないわけにはいかない」
  • 随伴のHom集合による定義
    • 随伴→2つの圏の間の2つの関手における関係
    • 単位元(余単位元)→恒等射をマッピングしたもの
    • 対象的で覚えやすい。双対性が見えやすい。普遍性との関連がわかりにくい
  • unitによる定義
    • あるη:1→GFが、任意のf:X→GYについてf:FX→Yが唯一存在するとき(満たすべき可換図式は略)
    • counitによる定義は双対なもの
  • 例: Δ(X)=(X, X)の右随伴をcounit definitionで調べる
    • counitの成分はC×Cの射なので、(π1,π2)として可換図を書き下す
    • 積の可換図式が現れる。Δ|-×
    • 同様に+|-Δ
  • Q. +と×が双対なのはたまたま?
    • A. 一般には違う。Δの双対がΔなのでこうなる
  • Q. |-はいつまでもチェーンになる?
    • A. 随伴は存在しないこともある。無限に随伴が続くことがあるのかはわからないので各自調べて
  • Q. テキストは向きが逆だけど?
    • A. テキストは-|らしいので、読み替えて
  • 例: 一般の対角関手: ΔJ:C→C^JはΔ_J(X)(A) = X、ΔJ(X)(f) = id_Xで定義
    • colim J |- ΔJ |- lim Jとなる
  • 例: (-)×A|-(-)^Aをcounit definitionで考えてみる → counitがevaluation mapとなる
  • 例: 自由モノイドをunit definitionで考えてみる → 忘却関手の左随伴Fが存在するための条件となる
    • counit definitionで考えてみる → counitがfold。foldMap f = fold . map fが出てくる
  • Fの右随伴、左随伴は、同型を除いて一意
    • 米田の補題で証明できる
    • 随伴を用いて定義するとwell definedになることを意味する
  • F|-Gの時、Fは余連続(colimを保存)、Gは連続
  • 右随伴はlimを保存するので、1^A =~ 1、(B×C)^A =~ B^A×C^A
    • 左随伴はcolimを保存するので、0×A =~ 0、(B+C)×A =~ B×A+C×A 分配則
  • Q. 随伴のイメージとは?
    • A. トドのつまり、というのは言い難い。「イメージできないものを得た」。Hom集合による定義がイメージ
    • 随伴とはシンタックスとセマンティクスの関係(自由モノイドとか)?最適化問題
    • わかるまで練習問題を解いてみて下さい
  • モナドはもともと圏論の概念。それが計算機に応用されたもの
    • 純粋に圏論的なモナドはコンピュータと結びつきにくいかもしれない
  • 自己関手Tとη:1→T、μ:TT→Tで、モナド則を満たすもの
  • 例: リストモナド
    • Setsにおいて、T(A)をAの要素の列の集合、TfはTAの要素全てにfを適用する関数
    • モナド則をghciで実際に確認してみる
  • モナド圏論的な文脈
    • 随伴F|-Gについて、GFとunit、G(ε_F)、の3つ組はモナド
    • 証明については「GFGFGFとかでてきて読むのが嫌になりますね」
  • リストモナドは、自由モノイドFと忘却関手Uとすると、UF
    • G(ε_F)を考えると、concatを忘却したものになる
  • (-)×S |- (-)^Sからはstateモナドが出てくる。stateモナドはカリー化と関連している
  • モナドから随伴を作れる。ただし、モナドと随伴は1対1ではない
    • Eilenberg-Moore圏。T代数の圏
    • 随伴の場合は圏Dが必要。このとり方に自由度がある
  • モノイド対象
    • モノイドをSetsにおける圏の言葉で定義できる
    • 前提条件「直積があること、結合的であること、1×MとMが同型であること」
  • モノイダル圏
    • 関手(*)があり、(X(*)Y)(*)Z =~ X(*)(Y(*)Z)、I(*)X =~ X =~ X(*)I
    • コヒーレンス条件も必要(ほとんどの場合成り立つらしい)
    • Setsでモノイド対象を考えると、モノイドが出てくる
  • 自己関手の圏でモノイド対象を考えると、モナド
    • 自己関手の圏 → 対象は自己関手C→C。射を自然変換。
  • モナドはモノイドと思ってよい
  • 理論計算機分野でのモナド
    • 表示的意味論の分野で、Moggiによる提案が始まり
  • Computational effect
    • 計算とは、「インプットがあってアウトプットがあるもの」。関数として表現しようとする
    • computational effect。計算作用
    • 例: 値を返さない、複数の計算結果、副作用、エラー、継続
    • 計算作用を自己関手Tで表す。A→T B。Kleisli arrowと呼ぶ
  • 表し方
    • 値を返さない → TB = B + 1
    • 複数の計算結果 → TB = P(B)
    • 副作用 → TB = (S×B)^S。A×S→B×Sをカリー化したと思えばよい
    • 例外 → TB = B + E
    • 継続 → TB=(R^R)^B
  • 計算は合成できる A→TB、B→TCを合成するとA→TB→TTC
    • 計算作用が二度起こると考えればよいが、計算作用の種類が違ってよくない
    • μ:TT→Tでたたみ込める
    • 計算作用の畳み込みは結合的 → TTTの畳込みは結合的になるだろう
  • 何もしない計算があった方がよい。η:1→T
    • 何もしない作用は単位的になるはず。ηは単位元になるだろう
  • Haskellでは、ηはreturn、μはjoin
    • return 1の[Int]、Maybe Int、IO Int、State () Intなどの例
    • joinの例
  • モナドのありがたさ
    • 数学的な表示により、計算機作用の数学的な解析が可能になる
    • プログラムの検証、最適化などに使える
    • カリーハワード対応により、理論計算機分野以外への貢献も
    • haskellにおけるdo記法。並べられた文の合成法を与えている
    • プログラムの設計にも(いいか悪いかはともかく)影響を与えているだろう
  • Q. 学校でモナドが出てこないのなんで?
    • A. 新しい。教えられる人が少ない。抽象的過ぎるので必要となることは少ないかもしれない。圏論型理論などを統一的な枠組みで捉え直したもの
  • Q. 数学からもっといい抽象化が?
    • A. ありうる。モナドより広いArrow、狭いApplicative、など
  • Q. 違う種類のTとT'を合成することができるのか
    • A. 同じ種類のものしか合成できない。モナド変換子がそのようなもの。TとT'を合成した一つの関手T''を作る
  • Q. 層圏トポスに圏論だとスッキリって書いてあったけど本当?
    • A. 集合論で証明するのは難しいって話か、もしくはトポスの話??圧倒的に楽になる理論があるのは確か。すべてがやさしくなるわけではない
  • この回は入門なので、本を読み、練習問題をやってほしい。理論計算機分野の論文も読むと良い


お疲れ様でした。それにしても、東京で13回かけて話された内容を去年名古屋で2時間で話したのだから、名古屋の怖さがよくわかりますね!

まだ物足りない方は、コンセプタンや元祖圏論勉強会に出席されるとよいでしょう。

最後になりますが、講師を勤めてくださった@9_ties さん、どうもありがとうございました。大変勉強になりました。