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

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

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

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

圏論勉強会ではない圏論勉強会 第1回に来ました。資料ustreamは公開されています。

@seizans さんより

  • ekmett勉強会でekmettさんが圏論勉強するといいよというから開催
  • 日本始まったな

講師 @9_ties さん

  • 圏論だけではなく、圏論を題材に色んなことを学ぶ会
  • 関数型言語を学ぶ会ではない。前提知識はなし
  • 教科書はSteve AwodeyさんのCategory Theory。数学専攻してない人向け
    • 記法などは「圏論の基礎」。数学専攻者向け。リファレンス
  • 今日は、圏論とは何か。随伴までいく
  • 対 → (A, B)とかPair A B
    • (double, double)だと複素数型になる
    • a << 16 | b という自然数もpair
    • 対の具体例はいくらでもある
  • 抽象概念を考えるには、定義が重要
    • 定義を飛ばしては行けない
    • 抽象的な定義。より多くの具体例を持つもの
  • 対P
    • first : P → A, second : P → B 中身を取り出す関数
    • firstとsecondを持つPはいくらでも考えられる
    • firstとsecondもいくらでも考えられる
    • f : X→A、g:X→Bを考える。
    • fとgをまとめるu : X → Pがあるはず
    • f == first . u, g == second . u → 図式が可換(commutative)である
    • 可換 → 合成結果が全て等しい
    • 唯一性が必要 → Pに余分なデータがない、と言えるだろう
  • 等式を図式で表現できるのが圏論のいいところ。等式を弄らなくて良い
  • P、first、secondの"普遍性"。「一意的に分解」
    • Pを定めるとuが一意に定まる
  • 定数1は、const 1として表現する*1
  • 抽象化 → "型"、"関数"、"関数合成"で説明したが、その具体的性質は使ってない
    • "物"と"矢印"。
    • "物"を部分集合、"矢印"を包含関係としてみてみる → {1, 2}と{1, 3}の対は{1}。対=共通部分
    • "物"を自然数、"矢印"を大小関係 → 4と6の対は4。対=min
    • 「積(product)」という → 無関係と思われるの概念が繋がった
  • 内部構造ではなく、外部との関係で物事を特徴付けている
  • 圏論は「良い言葉」。Haskellを使う時はもちろん、それ以外の場面でも役に立つ
    • 何かを考える時は、矢印で考える
  • Q. なぜ3は1と4の積じゃないの? → 4 を分解できない
  • 圏の定義
    • 対象(object)、射(arow, morphism)、合成(composition)
      • dom, cod : 射の元の対象と先の対象 : f : A→Bならdom f = A、cod f = B
      • 合成 g . f
    • 結合律(associative law) : (h.g).f = h.(g.f)
    • 恒等射(identity) 1 : A→A、f.1=1.f=f
  • 「対象と射の集まりで、合成ができ、合成の順は気にしなくて良く、恒等射がある」
  • 恒等射を1_Aと書くのは? → 対象Aについて一意に定まるから(複数個ない)
    • 証明 : 1_A と 1_A' があるとすると、1_A = 1_A . 1_A' = 1_A'
    • 圏論の証明はdiagram chasingと呼ばれる
  • 同型 : "等しさ"の定義の1つ。
    • {0,1,2}と{1,3,5}は"等しい"だろうか?
    • 数が同じ。「ある意味等しい」だろう
    • 圏論には色々な等しさの定義がある*2
    • g . f = 1, f . g = 1 であるときfは同型射(isomorphism)。gは逆射(inverse)
    • 同型射があるなら、2つの対象は同型
  • 「この圏では同型である」「この圏では同型ではない」ということが起こる
    • 集合が対象、射が恒等関数とすると、{0,1,2}と{1,3,5}は同型ではない
    • 集合が対象、射が任意の関数とすると、{0,1,2}と{1,3,5}は同型(同型射は6つある)
    • 周りの関係性から、"等しさ"を考えている
  • 逆射は一意に定まる
    • gとhが逆射とすると、g = g . 1 = g . f . h = 1 . h = h
  • 関手(functor) : 圏から圏へ構造を保つマッピング
    • 構造とは? → 対象、射、合成、恒等射
    • F(g . f) = Fg . Ff, F 1 = 1
    • 定義を音読して訓練
  • 関手は可換図式を保つ
    • 同型射、逆射も保たれる
  • sizeは有限集合と包含関係の圏から自然数と順序関係の圏への関手となる
  • Listは関手 (型Aを型[A]に移す)
    • map (show . (* 2)) == (map show) . (map (* 2))
    • 数学的には同じだが、(一般的には)メモリ効率が違うと予想される。運算に使える
  • 双対性 : 表裏一体
    • 双対圏 射を引っくり返したもの
    • 双対圏でminをとるとmaxになる
    • 双対圏で共通集合をとると和集合になる
  • 積(product)の双対は余積(coproduct) *3
  • 対の双対は? → 貼りあわせ Either
  • 代数的データ型 → 対は直積、貼りあわせは直和と呼ぶ
  • AとBの積は、全部同型 → 同型を除いて一意、という
    • 一意なのでA×Bと書ける*4、一意の射を<f, g>と書ける
  • 自然性
    • sumとlength、リストの概念において自然と言えるのはどちら?
    • sumは要素の方で決まる。lengthは型に依存しない
    • 関手Fは、元の圏の対象をパラメータに持つ概念だと思える
    • 「自然」とは、対応関係がパラメータの構造に依存しないこと
  • 自然変換 (natural transformation)
    • 概ね、多相関数のこと → length : [a] → a
  • 自然変換は関手と関手の対応
    • 関手圏 : 対象が関手、射が自然変換
    • モナドは単なる自己"関手の圏"におけるモノイド対象だよ?」
  • 様々な抽象概念は随伴(adjunction)という概念で統一される
    • 積圏C×C内のf, g と 圏Cの<f, g> と1対1の対応関係がある(全単射がある)
    • この対応関係は自然である
    • F X = (X, X)とG (A, B) = A×Bで定義される2つの関手は随伴となる
    • π_1とπ_2は、id_A×Bを考えれば、余単位元(counit)として現れる
    • 単位元(unit)というものもある
    • 随伴は関手と自然変換で語れる。具体的な対象、射に基づかない。汎用的
    • 随伴に関する定理を知っておくと、様々な例に適用できる
    • 全てのモナド、コモナドは随伴から作れる

*1:次の次の会くらいに詳しくやるらしい

*2:圏論はnatural equevalanceの考え方から産まれたとも言える

*3:coはsinとcosみたいなもの

*4:weldefined性。同型であれば、色んな議論を滞りなくできる