圏論勉強会ではない方の圏論勉強会 第3回に来ました。資料とustreamは公開されています。
- 今回からヘッドセット完備
- 中高生も見ているらしい(のでプログラミング以外のネタも)
第3回: 様々な圏 / 講師 @9_ties さん
- 視野が狭くならないよう、プログラムに関わらず色々な圏を見る
- 定義の復習: 圏〜自然変換まで。(自然変換はまだ雰囲気だけでOK)
- 主役級の圏を紹介
- Sets*1
- 対象が(小さい)集合、射が関数、関数合成
- とんでもなく巨大な圏
- 整数論とか実数論とかと規模が違う。色々問題が起こる
- 宇宙(universe) : 基礎論の分野なのでそこまで詳しく知らなくてもOK
- Mon(モノイドの圏): 対象がモノイド、射がモノイドの準同型
- Grp(群の圏): 対象が群、射が群の準同型
- MonとGrpは「構造と準同型からなる圏」
- これらは全て「具体圏」 → Setsと同一視が可能な圏(稠密な関手による定式化は別途行う)
- 型の圏 : 言語Lにおいて、対象がL内の型、射はLにおける関数
- 証明の圏 : 今日は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}より、{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次元での三角形で分割したもの
- 圏論はこの分野で育まれた学問である。群の間の不変量を色々調べる
- 実は論理の世界と関係する
- AかつBをベン図で書く=集合は空間的な概念。空間の構造と論理が対応する。空間が変わると別の論理となる
- 直感論理と関連する
- 年を取った人はいまさらこんなこと勉強できないけども、高校生も見ているので
