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

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

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

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

レポート math

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

  • 今回からヘッドセット完備
  • 中高生も見ているらしい(のでプログラミング以外のネタも)

第3回: 様々な圏 / 講師 @9_ties さん

  • 視野が狭くならないよう、プログラムに関わらず色々な圏を見る
  • 定義の復習: 圏〜自然変換まで。(自然変換はまだ雰囲気だけでOK)
  • 主役級の圏を紹介
  • Sets*1
    • 対象が(小さい)集合、射が関数、関数合成
    • とんでもなく巨大な圏
    • 整数論とか実数論とかと規模が違う。色々問題が起こる
  • 宇宙(universe) : 基礎論の分野なのでそこまで詳しく知らなくてもOK
    • Setsの対象すべてからなる集合Uを考えると、U∈U??
    • 対角線論法使ってごにょごにょすると、カントールのパラドクスにつながる。
    • 数学で必要な集合を全て含む"領域" U。もはや集合と呼べないもの。色んな宇宙がある
    • Uの要素を、「小さい集合」と呼ぶ
  • Mon(モノイドの圏): 対象がモノイド、射がモノイドの準同型
  • Grp(群の圏): 対象が群、射が群の準同型
  • MonとGrpは「構造と準同型からなる圏」
    • 構造を持つ集合と、構造を保つ準同型
    • ベクトル空間の圏: ベクトル空間と線形写像
    • グラフの圏: グラフとグラフ準同型
      • 計算機でよく扱う。WEBページのリンクとか、SNSの関係とか、状態遷移とか
      • グラフの構造を保つとは? → 辺と両端の関係
    • 実数の集合と連続関数の圏: 実数の位相構造とそれを保つ連続関数
    • 位相空間の圏: 実数の集合の圏の一般化。ドーナツと珈琲カップは位相同型(homeomorphism)
    • 順序集合と単調写像: 順序という構造と、それを保つ単調写像(monotone mapping)
      • 単調増加する数列は、インデクスから実数への単調写像
  • これらは全て「具体圏」 → Setsと同一視が可能な圏(稠密な関手による定式化は別途行う)
  • 型の圏 : 言語Lにおいて、対象がL内の型、射はLにおける関数
    • Haskはこの一種
    • ここで、型と関数はただの文字列。(同値関係で割る必要はある)
    • 例えば "Int" はただの文字列。集合ではない
    • 型の圏を具体圏(ドメイン((dom,codとは関係ない。スコットドメイン)))に紐づける関手は、プログラムに意味を与える事になる → コンパイラは関手。表示的意味論
  • 証明の圏 : 今日は5月(A)の晴れた日である(B)、ならば、今日は5月(A)である
    • A∧B→B 。これは∧除去の推論規則。
    • 論理式から推論規則により別の論理式へ変換する事を形式的証明。
    • 論理式が対象、証明が射。
  • 型の圏と証明の圏は重要。Coq、Agdaとか、定理証明支援系。
    • 証明とプログラムには強い関連がある
  • Cat(圏の圏) → 対象が圏、射が関手。ものすごく巨大な圏
  • 主役級はここまで。他、Rel(関係の圏)
  • 離散圏 : 対象は集合の要素、射は恒等射のみ
    • 恒等射と恒等射の合成は恒等射・・・と定義
    • 恒等射が何かは考えてはいけない。圏と呼ぶために形式的に必要なもの
  • モノイド、群: 対象が1つ、モノイドの要素が射
    • 群の場合は、全ての射が同型射
    • 対象は1つ・・・と定義。意味はないのでそれが何かは考えない。対象が1つ=全ての射が合成可能
    • 例: 列と連結からなるモノイド。列が射、合成が連結
  • 前順序集合: preordered set
    • 異なる対象同士の射が高々一個しかない圏(向きが違うのは別と数える)
    • 射→を≦と読めばよい
    • 半順序との違い : ループを許すかどうか
  • 反順序集合 : 全順序集合で、向きの違いも同じと考える場合
    • A<=B、B<=AならばA=B
    • 例: 集合の包含関係を≦と解釈すると、半順序集合
    • 例: A≦Bを、「BがAで割り切れる」と解釈すると、半順序集合
    • 例: 自然数、実数などで、≦を通常の大小関係とすると、半順序集合
      • この例は全ての対象の間に射がある(全ての対象が比較可能)。全順序集合(totally ordered set)
  • 半順序が重要 : データの階層構造を表現している。プログラムのデータも積み上げて大きな構造を作る
  • 空圏0 : empty category。射も対象もない
  • 1 : 対象が1つ、射が恒等射
  • 2 : 対象が2つ、その間に射が1つ(恒等射が他に2つあり、射は3つ)
  • 3 : 対象が3つ、それを順に結ぶ射が2つ(他、合成した射1つ、恒等射3つ)
  • なんの役に立つ?
    • 簡単な圏は練習用に使える
    • 関手とセットで考えると強力
  • モノ(対象や射)とマッピング(関手)が、同一視できる。モノをマッピングで表現する
    • F:1→Cなる関手。関手とCの対象を同一視できる
    • F:2→Cなる関手。関手とCの射を同一視できる
    • F:3→Cなる関手。合成可能な2つの射、と同一視できる
    • こういう側面が、数学だけでなく、ソーシャルサイエンス、認知科学とも関連する
  • 離散圏からの関手 → 重複を許して、特定個数の圏の対象を選ぶこと
  • 関手F:J→Cを考えたときに、Jを「型」と見なせる
  • 0からの関手は1つだけ存在する
    • 空集合から任意の集合への関数は空関数と呼ぶ。1つだけ存在する
    • 唯一存在する事は、数学的に証明ができる(スライド参照)
  • 圏から圏を作る
  • 積圏 C×D : 対象は圏C、Dの対象のペア、射は圏C、Dの射のペア
    • 積圏があれば、多変数関手が定義できる(積圏からの関手を考える)
  • 関手圏
    • 圏C、圏Dについて、対象はF:C→Dなる関手、射は関手の間の自然変換τ:F⇒G
    • D^Cと書く
  • 自然変換は関手と関手のマッピング
    • 横を繋ぐ射のコレクション
    • 可換になる
  • 例: C^1 → 関手はCの対象だった。自然変換はCの射となる。よってCと同型
    • C^1 と C は同型
  • 例: C^0 → 関手は1つしかない。自然変換は空の恒等射のみ。
    • C^0 と 1 は同型
  • この記法により、関手圏と指数法則が似た振る舞いをする。わかりやすく弄れる
  • 例: C^→ (=F:2→Cが対象) *2
    • 関手は射だった。自然変換は可換図式。これを射圏という
  • Q. 空圏から関手が1つあるのは、⊥から全てが証明できることに該当? それは公理に入る?
  • A. はい。証明体系によって公理になったり定理になったりする
  • 半群: 二項演算、結合則 (単位元を要求しないモノイド)。例えば(Z, max)は半群
    • 生成系 {a, b, c}に2項演算を0回以上適用したもの {a, b, c, ab, bc, ca, abc, ...}
    • 半群なので、括弧を外してもよい
    • これが自由半群 (他に満たすべき法則がない)。単位元がないので空列はない
  • マグマ: 半群から結合率を除いたもの
    • 生成系 {a, b, c}より、{a, b, c, (ab)c, a(bc), ...}
    • これは二分木の構造
  • 代数を考え、その自由〜〜を考えると、データ構造になる
  • 可換モノイド: 可換(ab = ba)なモノイド
    • 自由可換モノイドとは、{a, b, c, abc(=bca, cba), ...} マルチセット
  • 冪等モノイド: aa = a
    • 自由冪等モノイドは同じ要素が続かない列
  • 冪等可換モノイド: aa = a
    • 自由冪等可換モノイドは集合となる
    • wikipediaも参照
  • 例: class Magma a where magappend :: a -> a -> a
    • data FreeMagma = Leaf a | Node (FreeMagma a) (FreeMagma a) → instanseは略
    • newtype Kakko = Kakko String
    • instance Magma Kakko where Kakko x `magappend` Kakko y = Kakko ("(" ++ x ++ " " ++ y ++ ")")
    • foldMapMagma :: Magma b => (a -> b) -> FreeMagma a -> b
    • foldMapMagma f (Leaf x) = f x
    • foldMapMagma f (Node l r) = foldMapMagma f l `mappend` foldmMapMagma f r
    • foldMapMagma (Kakko . show) tree みたいにして畳み込める
    • newtype WrappedMonoid a = WrappedMonoid a
    • instance Monoid a => Magma (WrappedMonoid a) where WrappedMonoid x `magappend` (WrappedMonoid b) = WrappedMonoid (append a b)
    • WrappedMonoid . Sum, WrappedMonoid . Product みたいにマグマへのマッピングとしてfoldMapMagmaへ渡せる
  • 代数とデータ構造はリンクしている。空列が出てきたらモノイドが関係している、とか
  • 自由対象: 自由モノイドはMonの自由対象、自由半群Grpの自由対象・・・など
  • 忘却関手。構造を保つマッピングについて、構造を忘れて集合と関数と見なす
    • 生成系Aについて自由対象FAを作る。i:A→FA埋め込みを備えている
  • 今後繰り返す話なので、今回分からなくてもOK
  • おまけ:やわらかい話(位相幾何学)
  • 圏論の話をするのに位相幾何学を知らないのはまずい。
  • 3つの図形△、□、A、は全て位相同型。点の数引く線の数は0
  • 別の例では、点の数引く線の数は1。位相同型
  • オイラー標数。n単体。n次元での三角形で分割したもの
    • 位相同型な図形では等しくなる。不変数。
    • S^2は 点4 - 線6 + 三角4 = 2
    • T^2 トーラスは 点1 - 線3 + 三角2 = 0
    • 図形から不変量として代数的な構造(ホモロジー群、コホモロジー群)を取り出す。代数的位相幾何学(代トポ)
  • 圏論はこの分野で育まれた学問である。群の間の不変量を色々調べる
    • 実は論理の世界と関係する
    • AかつBをベン図で書く=集合は空間的な概念。空間の構造と論理が対応する。空間が変わると別の論理となる
    • 直感論理と関連する
  • 年を取った人はいまさらこんなこと勉強できないけども、高校生も見ているので

*1:マクレーン本だとSet

*2:C^2と書くとC×Cにも見えるのでこう書く