Pixel Pedals of Tomakomai

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

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

毎度おなじみ、圏論勉強会ではない方の圏論勉強会 第11回に来ています。資料ustreamは公開されています。

第11回: 指数対象・デカルト閉圏 / 講師 @9_ties さん

  • 今日からはがらっと話が変わるので、前回までの話は忘れて良い
    • 指数対象とデカルト閉圏
    • Curry-Haward-Lambek対応 → 圏論やってるのでLambekまで
  • 指数対象は極限、余極限で表せない。が、普遍対象
  • Hom集合に対して、ポイントワイズな定義で元の圏の構造が入る(第4回)
  • 指数対象とは → 関数空間の圏論的な一般化
    • 関数空間とは → 関数の集合に構造を入れて考察対象とする
    • B^A と書く。AからBへの射の集合に構造を入れたもの
    • Hom(A, B)はSetsの対象であることに注意
    • B^Aは圏Cの構造が入るので、圏Cの対象となる
    • internal homsetとも呼ぶ
  • Q. 関手圏をC^Dと書いたけど、同じ?
    • A. 同じ。Catにおける指数対象
  • Setsでの例 : B^A = Hom(A,B)
    • 圏の対象じゃないので、これは定義にできない
    • 任意の対象Xについて、g:X→B^Aを考える。どんな性質を持つ?
    • g(x)(a)∈Bという性質を持つだろう
    • f(x, a)=g(x)(a)と置くと、f:X×A→Bと1対1に対応するだろう
    • ε:B^A×A→B を ε(h, a) = h(a) で定義。Haskellではuncurry ($)
    • f(x, a)=g(x)(a) は、 ε . (g×1) == f、と書ける
  • べき対象の定義
    • (B^A, ε)が指数対象であるとは、
    • 任意のX、f:X×A→B に対して、ε.(g×1) == fを満たすf~:X→B^Aが唯一定まる
  • εを評価射と呼ぶ。evaluation map
  • 指数対象は同型を除いて一意(簡単な練習問題)
    • 「B^Aの性質を満たすものをもうひとつ作って縦に並べてぽんぽん」
  • 極限、余極限では、coneの頂点が定義されるオブジェクトであった
    • 頂点に向かうor出る、という構造
    • B^Aはconeの頂点ではない。違う種類の普遍性
  • Haskell的には、 f_tilda x = \y -> f(x, y) と思うと良い
    • uncurrying をg^_と書くと、g^_ = ε . (g×1) で定義できる
    • (-)~:Hom(X×A, B) =~ Hom(X,B^A):(-)^_
  • デカルト閉圏 (CCC)
    • 有限個の対象の積(つまり、終対象と任意の2個の積)が存在*1
    • 任意の対象についてB^Aが存在*2
    • CCCとは略記しない(Cauchy complete category とかあるので)
  • A^1 =~ A
    • 証明: 定義のA^1の部分に、Aを入れても当てはまることを示せばOK
  • C^(A×B) =~ (C^B)^A
    • 証明: 定義の(C^B)^Aの部分にC^(A×B)を入れても当てはまることを示せばOK
    • evalを具体的に構成するのがポイント。assoc:A×(B×C) =~ (A×B)×Cを使う
    • もっと簡潔な証明: C^(A×B) =~ (C^B)^AはHom(A×B, C)=~Hom(A, C^B)と見なせる
      • 米田の補題を使えば、by Yoneda、ですんでかっこいい! 来週
  • 同様に米田さん
    • Hom(A,1) =~ A → 1^A =~ a
    • Hom(A, B×C)=~Hom(A, B)×Hom(A,C) → (B×C)^A =~ B^A × C^A
    • 指数法則が成り立つので指数対象、と思うのも良い
  • 分配的な圏
    • 余積と積を持つ圏を考える
    • A×B+A×C =~ A×(B+C)が成り立つとき → 分配的であるという
    • 一般的には成り立たないが、「余積を持つデカルト閉圏は分配的)
    • 証明: Hom(A×(B+C), X) =~ Hom(B+C, X^A) → Hom(B,X^A)×Hom(C,X^A) =~ Hom(A×B,X)×Hom(A×C,X) =~ Hom(A×B+A×C,X)
      • ここから示したい式を取り出せる。詳細は来週
  • (-)^Aは関手になる → 対象XをX^A。射fを(f.ε)~
    • 証明は練習問題
    • Setsでの例。f^Aはfを左から合成する関数。共変Hom関手を圏の言葉で言い直したものがf^A
  • 例: Haskellだと、Data.Functor の instance Functor ((->) r)。
    • fmap = (.)。つまり左から合成
    • Readerモナド
  • 関数型フィールドが関手になってくれないと困る
    • Stateモナドとかでも関数型フィールドが使われている
    • 始代数、や終余代数も考えられない
    • べきが関手になることで、指数対象にもこれらの議論が使える
  • Curry-Howard-Lambek対応
    • Curry-Howard対応とは、論理の体型と計算の体型の同値関係
      • 論理、計算の種類によって異論な種類がある
      • 論理とは静的な現象、計算とはプロセス。興味が違う。
      • 「怖い人が来るので、あまり哲学的なことは言わないほうがいい」
    • Curry-Howard-Lambek対応とは、直観主義明大論理、型付きラムダ計算、デカルト閉圏、の同型
  • 形式的証明(formal proof) → 証明を、論理式(記号列)の推論(機械的な変更)の列で表したもの
    • 記号変形の問題と見なしている。意味を考えない
    • 経緯: 微分積分によって実数が発明された→集合はすごい→パラドックスの発生→人間の直観を排除すべき
    • 定理証明支援系につながっている。Coqとか
  • ∧⇒論理
    • 命題論理: 変数を持たない命題 「人間は哺乳類である」。アリストテレスが創始者
      • 述語論理は、「人間はXである」。1階、2階、・・・
    • 直観論理: 排中律「A∨¬A」を公理に入れないもの
    • 命題変数P、Q、・・・と∧、⇒からなる
    • 結合順位が∧の方が高いとする
    • 証明を書きなおす(judgement)ことで証明を導出 → id, ∧intro, ∧elim1, ∧elim2, ⇒intro, ⇒elim
    • A⇒(B⇒A)の証明の例
  • 「結局完全性定理があるからどうでもよい」
  • カルテシアン閉圏との対応
    • 論理式を対象とする
    • judgement A1, A2, ..., An |- Aを射A1×...×An→Aとする
    • それぞれの規則と、デカルト閉圏が一致する
  • モデル → 記号列に数学的なオブジェクト(CCC)を割り当てる
    • CCCはモデル、と言える。ソースコードコンパイルされた実行可能コードみたいなもの
    • 健全性(証明できるなら真)と完全性(真のものはすべて証明できる)
    • 証明できること(機械的な変形)と真(意味を考えたもの)は別
  • 型付きλ計算デカルト閉圏
    • λ計算 → 計算を数学的に考えたもの(他、チューリングマシン帰納的関数、など)
    • λ計算では、計算を式を書き換えたものとする
    • チューリング計算では、状態を更新するものが計算
    • 帰納的関数では、ある種に属す関数
    • 基本型:A,B,C...、A→B、A×Bを型とする
    • A型の変数x,y,z・・・:A、A型の項a,b,c...:A、(a, b):A×B、π_1 c、π_2 c、ca、λx.bが項
    • 計算の表現のため同値関係を入れる(公理)→この同値関係を L |- a = bと書く
  • デカルト閉圏との関係→対象は型、射は自由変数を持たないλ項。ただし、L|-a=bで同値類でまとめる
    • id=[λx.x]、g.f=[λx.g(fx)]、[f]~ = [λx.λy.f(x,y)]などなど
  • 例として、ε.([f]×1) = [f]の証明を手書きで
  • 形式証明なんて手でやるものでない(ヒルベルト流(証明が長くなるらしい)で693 stepの例)→Coqで
  • 論理学の世界と計算の世界がつながる
    • 論理の体型を見つけて、対応するλ計算を考えたり
    • 定理証明支援系がいい応用例。それぞれCCCの対象と射になっているのだから、証明とプログラムが対応する
    • Integer -> aはプログラムが書けないので証明できない。a -> (b -> a)は証明できるので、プログラムは書ける。
  • 次回は自然性と随伴

*1:これだけだとでデカルト圏。直積のことをデカルト積と呼ぶので

*2:Hom集合を含むことを閉じていると言っているのではないか。詳細は不明とのこと