毎度おなじみ、圏論勉強会ではない方の圏論勉強会 第11回に来ています。資料とustreamは公開されています。
- ワークスアプリケーションズさんに感謝
第11回: 指数対象・デカルト閉圏 / 講師 @9_ties さん
- 今日からはがらっと話が変わるので、前回までの話は忘れて良い
- 指数対象は極限、余極限で表せない。が、普遍対象
- 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)
- 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対応
- 形式的証明(formal proof) → 証明を、論理式(記号列)の推論(機械的な変更)の列で表したもの
- ∧⇒論理
- 「結局完全性定理があるからどうでもよい」
- カルテシアン閉圏との対応
- 論理式を対象とする
- judgement A1, A2, ..., An |- Aを射A1×...×An→Aとする
- それぞれの規則と、デカルト閉圏が一致する
- モデル → 記号列に数学的なオブジェクト(CCC)を割り当てる
- 型付きλ計算とデカルト閉圏
- デカルト閉圏との関係→対象は型、射は自由変数を持たないλ項。ただし、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)は証明できるので、プログラムは書ける。
- 次回は自然性と随伴