Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

トップ > 技術 > 今日は 圏論勉強会 第7回 の日です

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

技術 数学

圏論勉強会ではない方の圏論勉強会 第7回です。資料とustreamは公開されています。

第7回: 様々な極限 | 代数的データ型 / 講師 @9_ties さん

  • 1時間で話せる内容ではないので、証明とかは家で読んで
    • 「ここまで生き残った皆さんなら」
  • 錐の圏の終対象、始対象がlimit, colimit
    • 空圏、離散圏は前回やった
  • イコライザ、コイコライザ
    • ２本の平行射からなる圏のlimit, colimit
    • この定義から詳細な定義を考えるのは良い練習問題
    • 「f.e = g.eで、f.x=g.xなる任意のxについて、e.u=xを満たすuが唯一存在」
  • Setsでのイコライザ
    • f.e=g.eなので、fとgで同じ所へ移る要素のみ集める。唯一性から包含写像
    • f(x,y)=x^2+y^2、g(x,y)=1とするとeq(f,g)={(x,y)|x^2+y^2=1}
  • Setsでのコイコライザ
    • q.f=q.gより同値関係でまとめたもの
    • f(n)=n,g(n)=n+3とすると、coeq(f,g)はZ/3
  • イコライザは部分集合→単射っぽい、コイコライザは類別→全射っぽい
    • イコライザはmono、コイコライザはepi
    • 証明はいい練習になるので読んでおいて
  • 引き戻し(pull back)は→←のlimit、押出(push out)は←→のcolimit
    • 定義を書き下す練習してね
    • pull backはよく使う。push outはそうでもない
    • pull back は×_Cで書く (_Cは分類集合*1を意味している)
  • Setsでの引き戻し
    • {(a, b) | f(a) = g(b)}
    • χ:A→{T,F}、1→{T,F}でのpullbackは{a|χ(a)=T}なのでAの部分集合
    • χは特性関数。トポスと関連
  • 引き戻しは積とイコライザっぽい性質
    • 実際そう。π.fとπ'.gのイコライザでよい
    • 任意にx:X→Aとy:X→Bをとる。
    • 証明: π.fとπ'.gのイコライザについて、uが唯一存在。これが要求される唯一の射
  • 押し出しは余積とコイコライザ
  • 任意の極限は積とイコライザで作れる
    • 任意の対象の集合の積、任意の平行射のイコライザが存在 → 完備。常に極限が存在
    • 終対象も必要。有限積のみであれば有限極限が、無限積も許せば無限の極限も
    • ω余完備という概念がプログラムの意味論に必要となる。高校数学での極限に近いのでわかりやすいはず
  • Q. pull backとpush outの語源は？
    • A.逆像がpull backの例なので、そのイメージ？
  • 「そろそろ使える知識を・・・圏論も使えますが」
  • 代数的データ型 → 半群やマグマの自由対象と同じアイデア
    • F代数、F余代数
  • 自然数を圏論で定式化したい
    • zero∈N、succ:N→N、succ n≠zero、succは単射
    • 有限の言葉で無限集合を定義。zeroも自然数とする
    • zero=1、succ n = 2nとすると{1,2,4,8...}になるが、Nと同型なのでこれでよい
  • 圏論ではzero:1→N、succ:N→Nと言える
    • 対象、射の中身は不明。外から自然数を特定する
    • 1→X←Xという図式がなす圏を考える。射は可換性を満たす(1, h:X→Y)
    • 射の可換性はh.c=d, h.f=g.h。ポイントワイズだとh(c)=d、h(F(x)=g(h(x))
    • hは構造を保っていると言える。準同型
    • 今までのモノイド、群などの例と違い、"演算が見える準同型"
  • Q. Yって何？
    • A. 何でもいい。私:1→人間、父:人間→人間とかでも
    • A. 何が自然数かわからないので、同じ形のもの全部集めてくるしかない状況
  • 1→X←Xという図式がなす圏の始対象が自然数
    • u:N→Xとして、u(0)=c, u(n+1) = f(u(n))を取ればよい
    • 帰納法によってすべての要素が網羅されるので、uが一意に定まる
  • 関数型言語の自然数型には⊥があり擬数や無限数が存在するのでめんどい。忘れる
    • seqとかヤバい関数があり、すべてを台無しにしている
  • 1→X←Xを余積により[c,f]:1+X→Xとできる。射はhと1+hに翻訳できる
    • 余積からの射はすべて[c,f]と書けるので、一般性を失わない
    • FX = 1+Xなる関手を考えると、FX→Xと書ける。射はhとFhと書ける
  • F-algebra X←FX:xなる射のこと。(X,x)と書ける
    • F代数の射は、h:X→Yで可換になるもの。
  • F-始代数。(T, in)などと書くことが多い
    • 一意に存在する射をcatamorphismと呼び、(|φ|)と書く。
    • Functional Programming with Bananas, Lenses,. Envelopes and Barbed Wire(バナナ、レンズ、封筒、有刺鉄線)という論文。
  • 多項式関手 : 積と余積で構成される関手
    • 射を写すときは、X以外は恒等射に写すこと
    • 自然数 FX = 1 + X、リスト FX = 1 + A×X、長さ1以上のリスト A + A×X、葉にA型を持つリスト A + X × X
  • リストFX = 1 + A×Xとcatamorphism
    • 余積を展開すれば、1→[A]←A×[A]
    • (|[c, f]|) = foldr f c となっている
    • 他の構造でもcatamorphismはfoldに該当するものが出てくる
  • catamorphismのような再帰を表す射 → 再帰スキームと呼ぶ
    • catamorphismはfoldの再帰スキーム
  • Q. Foldableと一緒？
    • A. foldが定義できれば同じになるはずなので一緒になるのでは？ちゃんと考えましょう
    • A. Foldableのインスタンスは必ずF-始代数になっていそう。恐らく。
  • 反射則、融合則 (!:0→Aとする)
    • 反射則: ! = id、融合則: f.! = !
  • catamorphismでは
    • (|in|)=id、h.(|f|) = (|g|)
    • 反射則 → foldr (:) [] = id
  • sum . filter even をひとつのfoldrで
    • filter q = foldr (\a x -> if q a then a:x else x)なのでcatamorphism。[nil, p]と書く
    • sum . [nil, p] = [c, g] . (1 + 1×sum)を満たすcとgを探せばよい
    • aが偶数ならg(a, x) = a + x, 奇数ならg(a, x) = x
    • foldr (\a x -> if even a then a + x else x) 0
  • 中間データ構造がなくなった。デフォレストレーション
    • Haskellはlazyでthunkがあるので速くならない
    • 正格な言語には有効
  • Lambekの補題 → (T, in)がF始代数なら、inは同型射
    • T = FT と定義を書いているのだから、そうならないとキモい

*1:subobject classifier