haskell-jp / math #4

@junji.hashimoto has joined the channel
Churchな自由モナド F を使うにあたって、
F $ \p f -> runF ... という変換を何度も適用する必要があるので、

modF mod x = F $ p f -> let (p', f') = mod (p, f) in runF x p' f'


というのを定義してやって、 modF mod2 (modF mod1 x)modF (mod2 . mod1) x に書き換えるRULEを書いてやると速くなりそう、という見通しを立てました。

https://hackage.haskell.org/package/free-5.0.1/docs/Control-Monad-Free-Church.html
で、ここで挙がっている論文によると、 F はCodensityという構成と同一視できるとありました。すると、 modF は圏論の言葉で一体何に相当するのか、というのに現在悩んでいて、件の論文を読み込んだり頑張っています。 https://www.reddit.com/r/haskell_jp/comments/81q83q/kan%E6%8B%A1%E5%BC%B5%E3%81%AE%E8%AA%AC%E6%98%8E/
kan-extensionsパッケージ辺りに、既に定義してあったりするのだろうか
F はCodensityという構成と同一視できる」というのは正確ではなくて、kan-extensionsパッケージを見る限り F fCodensity (Free f) が同一視できるような感じですね
論文を飛ばし飛ばし最後まで読んで、なんとか形だけは理解できました。自由函手と忘却函手の随伴関係により「忘却函手のCodensity」と「自由代数を忘却したもの」が同型である事が示せる、とのこと。
modF関数は、pureを勝手に触ってしまうとモナド則が保てないので、次のように定義すべき。

modF :: (forall x. (g x -> x) -> f x -> x) -> F f a -> F g a
modF mod x = F $ \pr fr -> runF pr (mod fr)

@nrskt has joined the channel
@voqn.tyrant has joined the channel
わたし、大学は芸術の専攻だったので高校数学の範囲までしか履修していなくて、いきなり圏論に向かう前に順序立てて独習したいものの、そのチャートがまだ分かっていないところがあります。
代数学に至る前に群論、群論の前に集合論、で、その前に線形代数学を理解できている必要がある?
圏論を学ぶだけでしたら、数学の論法に慣れている(これは強調してもしたりないくらいすごく大事)だけで十分学べると思ってます。対象が1つの圏はモノイドになるという意味で、大学入学レベルの丁寧な教科書で群論を軽くやっておくと練習にはなるのかもしれません。
圏論を勉強していると数学での具体例(前述のモノイドも含む)がたくさん出てきますが、それを理解するためには様々な分野の数学の知識が必要になりますね。私も勉強不足でほとんどわかりません。
一方で圏論の起源はホモロジーにあると聞いていますので、人間が圏論を発見したのと同じような道筋で勉強を進めたければホモロジーを勉強することになる気がしますが、すごく遠い道のりになりますし計算機やロジックで圏論を使いたい人にはあまり筋の良い進み方ではないように感じました。
@yosikawa has joined the channel
圏論をつかうと何ができるのか、応用面が気になっています。モナド、モノイド、アロー、コモナド以外で。
ひとつ recursion scheme 的な話はありますね。
ご参考:
https://www.slideshare.net/sakai/introduction-to-categorical-programming-revised
ありがとうございます。
あと、Computational Category Theory http://www.cs.man.ac.uk/~david/categories/book/book.pdf という本があって、古典的ですが unificationがcoequalizerだとか、仕様の合成がcolimitだとか、そういう話がちょっと書いてあります。
MLの話やExerciseもありますし、とっかかりがよさそうでね。読んでみます。
https://hackage.haskell.org/package/category-extras
limitもありますね。楽しくなってきました。
それから、 David I. Spivak が
Databases are categories http://math.mit.edu/~dspivak/informatics/talks/galois.pdf とか
Backprop as Functor https://arxiv.org/abs/1711.10455 とか言ってたりします。
そう見ることによる利点がそんなにあるかというと……という気もしますが。
@hiroto.shioi has joined the channel
IOHKのHaskell講義では先生全員がこの本を圏論の入門書として勧めてました(私はユージニア・チェンじゃないです)
数学教室 πの焼き方: 日常生活の数学的思考 ユージニア チェン https://www.amazon.co.jp/dp/4562052856/ref=cm_sw_r_tw_dp_U_x_H2qTAbKHN5JM7
Kindle英語版なら671円で買えるし、なんならYoutubeで公演を聴くこともできるのでおすすめしておきます。
第1部 数学
第2部 圏論

ってすごいっすね

http://www.harashobo.co.jp/new/shinkan.cgi?mode=2&isbn=05285-1
タイトルは大げさだけど、中身は半分料理の話です。
数学の話を料理を例に挙げて解説していく形式です。
なるほど
ポチった
圏論が全然わからないと先生に言った時に、「πの焼き方」を読めばいいよと言われた時には戸惑いました。(しかもチェン氏は現在シカゴ美術館附属美術大学で圏論の授業を開いてるそうです。。)
美大で圏論????????
正直、今の美術系(というかデザイン系)普通に数学の知識入れた方がいい局面とうに来ていますからね……
以前、初心者込みで圏論の勉強会をやっていた時にこの本を使ったことがあります。内容としては基礎的な用語の説明と例が淡々と挙げてあるという感じで、応用を知るという意味では物足りないかもしれませんが、予備知識を要求しないので一つの選択肢として参考になれば。
@telaoki has joined the channel
@ywataywatay has joined the channel
集合論に関していえば、「集合への30講」(志賀浩二, 朝倉書店) https://www.amazon.co.jp/dp/4254114788 はどうでしょうか。大変丁寧でわかりやすいといわれています。
有限体の代数をごにょごにょしていたときとか、位相空間の参考書を読んでいる時がそうでしたが、色々な集合の上に様々異なる構造を入れて、さらにそれら同士の関係を抽象的に記述したり議論したりしようとすると、圏のような言葉が欲しくなるのはわかる気がしました。論理式と自然言語だけで書こうとするとこんがらがってしまう。
30講シリーズですか…
@lelect has joined the channel
@kaorun343 has joined the channel
以前行ったものを参加人数を絞って再度開催するみたいです。
https://techplay.jp/event/665982
前回参加した人はいるかな?
その方の圏論のお話は以前一度聴講に行ったんですけど、少なくとも数学をやってる人向けではありませんでした。それっぽい用語に囲まれて雰囲気を掴んだような気分になりたい方向けです。
なるほど。じゃぁほかの勉強会とも被っているのでやめておきます。ありがとうございます。
@andes has joined the channel
@shohei.takaichi has joined the channel
@service has joined the channel
@s.hayashi.py has joined the channel
数学系の型クラスの継承関係を再設計したそうで https://github.com/tonyday567/numhask
@akirakawata1 has joined the channel
@ttaakkee has joined the channel
@cosmiafu has joined the channel
質問です。
「無理数は加算・乗算のついて閉じていない」とおうのは、「有理数が無理数集合内に含まれている」というのと矛盾すると思います。
どこが間違っているのでしょうか。教えてください。よろしくお願いします。