2017年2月11日

黒木玄先生のモナド談義(#数楽)

黒木玄先生の数日にわたるモナド談義を一箇所にまとめました。
16
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ slideshare.net/yoshihiromizog… 圏論のモナドとHaskellのモナド Yoshihiro Mizoguchi

2017-02-06 20:07:44
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ math.uchicago.edu/~may/VIGRE/VIG… A folkloric proof of Beck's manadicity theorem and several examples of monads C.Berger

2017-02-06 20:54:38
黒木玄 Gen Kuroki @genkuroki

#数楽 リンクメモ www-kb.is.s.u-tokyo.ac.jp/~asada/papers/… K.Asada Arrowはprofunctorsの圏におけるmonad with strengthだった。

2017-02-07 04:21:02
黒木玄 Gen Kuroki @genkuroki

#数楽 モナド話続き。monadについては少しは知っていた。HaskellのApplicativeそのものは知らなかったのですが、弱い意味で直積を保つ函手と同じものなので「全然知らなかった」とは言えない感じ。続く

2017-02-07 20:14:44
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。さらにHaskellではArrowが定義されていてどういうものか全然理解できなかったのですが、profunctorsの圏におけるmonad (with strength)と同じものだと書いてある文献が見つかった(まだ読んでいない)。現時点ではこんな感じ。続く

2017-02-07 20:18:12
黒木玄 Gen Kuroki @genkuroki

#数楽 対象の掛算が定義されていれば自然にモノイドのような代数系を定義できる。圏Cからそれ自身への函手全体の圏End C(射は自然変換)は函手の合成という自然な掛算を持っている。End Cにおけるモノイドをモナドと言う。これがモナドの定義。定義だけを見ても有用さはわからない。続く

2017-02-07 20:24:56
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。随伴函手の対からモナドは自然に構成される。よく出会う随伴函手の対の典型例は(モノイドや群や環などの)代数系の圏から集合の圏への忘却函手Uと集合をそれから生成される自由代数系に対応させる函手Fの対です。典型的なモナドはM=UFと構成されます。続く

2017-02-07 21:31:19
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。そのとき、集合Xに対してMX=UFX=(Xから生成された自由代数系の台集合)、たとえば代数系としてモノイドを選んだ場合にMXはXを文字集合とみなしたときの(有限の長さを持つ)文字列全体の集合になります(空文字列が単位元)。続く

2017-02-07 21:35:16
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。以下、例として、MX=(Xを文字集合とみなしたときの有限の長さを持つ文字列全体の集合)の場合を扱います。集合間の任意の写像f:X→Yに対して、MX内の文字列をfによって置換して得られるMY内の文字列を対応させる写像M:MX→MYが自明に定まります。続く

2017-02-07 21:59:35
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。こんな感じのMは函手(functor)の典型例でかつモナドの典型例になっています。 このとき、MMX=(MX内の各文字列をひとつの文字とみなし、それらを並べてできる「文字列」全体の集合)=(MX内の文字列を連結せずに単に並べたもの全体の集合)となります。続く

2017-02-07 22:04:12
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。文字列を連結せずに単に並べたものに対して、それらを連結した文字列を対応させる写像μ_X:MMX→MXが自然に定まります。さらにXの元を1文字だけの文字列に対応させる写像η_X:X→MXも自然に定まる。μとηが函手Mのモナド構造です。続く

2017-02-07 22:10:19
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。η_X:X→MXはHaskellではreturnと書かれています。さらに写像f:X→MYには写像f^*=μ_Y⚪︎Mf:MX→MYを自然に対応させることができます。Haskellではηがreturnで、f↦f^*が=<<:(X→MY)→(MX→MY)です。続く

2017-02-07 22:21:40
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。モナドMではMを2回作用させたMMXをμ_XによってMを1つだけ作用させたMXに戻せます。どから、Mを複数回作用させた結果を常にMを1回だけ作用させた場合に戻すことができる。そういうことを自然にできる設定がモナドの定義だと思っても問題ないと思います。続く

2017-02-07 22:25:44
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。集合Xから集合MXを作る操作は、Xの元を有限個並べたもの全体の集合を作る操作です。Xの元を有限個並べたものたちにはそれらを連結する演算が自然に定義されます。その演算がMの操作を2回繰り返したMMXから1回だけのMXへの写像μ_Xになっているわけです。続く

2017-02-07 22:29:54
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。これは一般のモナドのケースでも同様で、一般のモナドX↦TXのモナド構造μ_X:TTX→TXはTXに何らかの「演算」が定義されていることを表しているものとみなせます。続く

2017-02-07 22:33:08
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。自由モノイドの(すなわち「文字列」全体の集合を与える)X↦MXの話に戻る。モナドが与えられるとそのモナドに対応する「代数系」の概念が自然に定義されます。MXの代数系の構造(文字列が連結できること)はたった一つの写像μ_X:MMX→MXで表現されるのでした。続く

2017-02-07 22:38:50
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。同様に集合Aにモノイドの構造が入っていれば、集合Aの元を並べたものにAのモノイド構造を使って連結して得られるAの元を対応させる写像α:MA→Aが得られます。写像αはAのモノイド構造の情報をすべて持っている。このような(A,α)をM代数と呼びます。続く

2017-02-07 22:46:53
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。M代数の満たすべき公理系はモノイドの作用の公理系と完全に同じなので省略。モナドMはそれ1つだけでM代数と呼ばれる代数系のみたすべき条件をすべて知っているわけです。集合にそれから生成される自由モノイドを対応させるモナドはモノイドのみたすべき条件をすべて知っている。続く

2017-02-07 22:53:18
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。これは自由群を作るモナドなど他のたくさんの代数系についても同じです。 随伴函手の話に戻る。一般に圏C上のモナドTとT代数の圏C_T (C_TにはEilenberg-Moore圏という権威ありそうな名前が付いているが名前にびびるのは非数学的)のあいだには〜続く

2017-02-07 23:00:26
黒木玄 Gen Kuroki @genkuroki

#数楽 続き〜、T代数にT代数の構造を忘れたもの対応させる函手U_T:C_T→Cと、Cの対象Xに自由T代数TXを対応させる函手F_T:C→C_Tが自然に定まり、随伴函手対になり、自明にT=U_T F_Tとなります。T代数の正体がわかっていればこれで基本設定は〜

2017-02-07 23:07:37
黒木玄 Gen Kuroki @genkuroki

#数楽 続き〜終了なのですが、そうでないときには、具体的な随伴函手対U:D→C、F:C→DでモナドをT=UFと作ったとき、DがT代数の圏C_Tといつ同値または同型になるかを知る方法が必要。それがBeckのmonadicity定理です。MacLaneの圏論の教科書に書いてある。

2017-02-07 23:14:58
黒木玄 Gen Kuroki @genkuroki

#数楽 証明を読んだこともないし、詳しくもないのですが、DeligneさんはBeckの定理を「群」の概念を理解するためにもっとも基本的だと思われる淡中圏の理論の整備に使ったそうです。

2017-02-07 23:38:45
黒木玄 Gen Kuroki @genkuroki

#数楽 続く。群の定義は数学を少しかじった人達にはおなじみのものだと思いますが、実際に応用されるときには群そのものよりも、群の作用や表現の方が役に立つことが多いのです。群の作用や群の表現のように見えるもの達の方から群を作る方法があるのらば、群概念の応用範囲は大きく広がると〜続く

2017-02-08 00:09:17
黒木玄 Gen Kuroki @genkuroki

#数楽 続き〜考えられます。実際にそういう理論は作られており、現代ではそれらを総称して淡中双対性と呼ばれているようです。淡中先生は私が学生時代に習った先生達の先生です。各種の淡中双対性については→ ncatlab.org/nlab/show/Tann…

2017-02-08 00:12:34
黒木玄 Gen Kuroki @genkuroki

#数楽 続き。群の表現のように見えるもの達(群の表現の圏のような圏)の中には条件を弱めると対応する群が無くなり、群概念を拡張する必要が出て来ます。量子群はそのような意味での群概念の一般化になっています。群では記述できない意味のある「対称性」が1970〜80年代に発見されました。

2017-02-08 00:18:25
残りを読む(308)

コメント

七誌 @7shi 2017年2月11日
本職の数学者がHaskellを見るとどう感じるかというのが垣間見えて興味深いです。
0