haskell-jp / math #7

おそらく、暗黙のうちに「外延性の公理」は前提にしているのだと思います。というか、そういう前提をいれてようやく Hask圏は圏になる、というか。

そうですよね、射がそれぞれ等しいということって、本当は厳密に議論しなければならないですよね

奥が深いです :thinking_face:

逆に、「射の等しさは圏論のご都合に合う形でいい感じに定まってるものとする」みたいなもんだと思えばキラクなんじゃないでしょうかねえ^^;

圏論に限らず、「適当な同値関係で割るものとする」って書いてたりしますよね　＞その場に置ける「等しさ」の定義

@Koyanagi S has joined the channel

@Yugo Osano has joined the channel

@ has joined the channel

@mod_poppo has joined the channel

@ has joined the channel

@ has joined the channel

@yuukis123 has joined the channel

@y-shishikura has joined the channel

@Fintoo has joined the channel

well-bound(well-foundのtypoではない念のため)やwell-supportedの訳をご存知の方いらっしゃいませんかー？

どういう文脈で出てくるんですか。
単純にググって論文がらみっぽいのは
well bound: 製本された
well supported: (議論などが)充分な裏付けがある
というのがありました。

例によってAlgebra of Programmingに登場します

In set-theoretic terms, a preorder R is well bounded if every non-empty set has a minimum under R
とあります.
Show that R is well bounded if and only of R ∩ R^o, the strict part of R is a well-bounded (equivalently, inductive) relation.
などwell-boundedという一語にまとめられて登場.

A relation R is said to be well supported if
dom (∈) = dom (mnl R)
Show that well-supported is a weaker notion that well-boundedness.
という感じでwell-supportedも

いずれもwell-bounded preorderとかwell-supported preorderと書いてあるのでほげほげな前順序というもののようです.
もちろん整礎はwell-foundedで登場しているのでそれとは区別が必要だと思っています.

誤操作してエントリポイントのメッセージ消してしまった..

R ∩ R^o の R は関係で R^o は逆関係ですか？そうだとして ∩ できるということは R の domain と codomain は同じ？
関係 R を preorder として見るのは a R b を a <= b と見る？
∈ と mnl ってなんでしょう。

逆関係 ~> #t
dom/codom ~> #t
関係Rをpreorderとしてみるのはどんな関係であれpreorderならなんでもいいです。<=に限定しないです。でも<=と見て良いと思う。
∈はelemだと思ってください。
mnlはminimal(最小限?)のことです。
関係Rのもとで集合xのminimalな要素aとはa∈xで、bRaなるどんなb∈xについてもaRbとなるようなもの。
mnl R = min (R^o ⇒ R)となっています。

最近の foldable の話題の

Monoid ∀m => (a -> m) -> m = Free a

は

Nat(Hom_Set(A,U(-)), U(-))
 {- U は忘却関手。Freeとの随伴により -}
= Nat(Hom_Monoid(Free(A),-), U(-))
 {- 米田の補題により -}
= U(Free(A))
= Free(A)

という解釈で筋としてあってますかね。

集合圏上のモナド M に対して EM構成の随伴対 F と U として

Nat(Hom(A,U(-)), U(-))
 {- U と F の随伴により -}
= Nat(Hom(F(A),-), U(-))
 {- 米田の補題により -}
= U(F(A))
= M(A)

これが codensityモナド？

Monad m => ∀b. (a -> m b) -> m b = m a

mnl R は x の要素ということは dom (mnl R) は dom (x のある要素) ということですか？ (x のある要素) はどういう射でしょうか。
「R^o ⇒ R」はどういう意味ですか。

@GolDDranks has joined the channel

Hom(A,U(B)) = Hom(F(A),B) は随伴そのものだけど Hom(A,U(-)) = Hom(F(A),-) は改めて確認しないといけないですね。（ベーシック圏論の演習問題 4.1.32 に F -| U は Hom(-,U(-)) = Hom(F(-),-) と同値、というのがありました）

@ has joined the channel

@acoman has joined the channel

@kazuokiriyama_ has joined the channel

@ has joined the channel

@gksato has joined the channel

@kanimum has joined the channel

このチャンネルでも一時話題になったガロア体（ 多様体 有限体）の実装
https://github.com/adjoint-io/galois-field

ガロア体（有限体）？

間違えた！ :dizzy_face:

adjoint-io って金融の会社(?)が作ってるんですね :serval:

Adjoint, 数学とか暗号関係のライブラリーもりもり出しててすごい

Adjointは、"What I Wish I Knew When Learning Haskell"とかでおなじみの Stephen Diehlさん、たちの会社です:haskell:

@ has joined the channel

@kazup0n has joined the channel

@ has joined the channel

@mazamachi has joined the channel

@miau has joined the channel

@ has joined the channel

https://gihyo.jp/book/2019/978-4-297-10723-9
圏論の本が！

@ has joined the channel

データ構造の Set って内部では木とかハッシュテーブルで実装されていると思うんですが、こういうのを圏論で取り扱う話ってありますか？

なるほどこれData.Setの実装みるとほとんど二分木(Traditional Binary Treeの方)になってますね.
だからF(A,B) = 1 + A B Bの不動点として扱えるし,その場合についてはcataだのanaだのは簡単に計算できますよね.(Size = Intは無視してよいのかあるいはidでよいのかちゃんと考えてないけど)

でもたぶん @hexirp さんの疑問ってそういう意味じゃないですよね?
そもそもSetって集合だと思うんだけど,集合って冪等可換モノイドなので二分木ではなくて,そこに冪等や可換という則が追加されているはずで,その辺どうなの?ってことだと思うんですが.

具体的にはわからないのですが,冪等や可換も含めて構成子が表現できていれば同様にF代数としてとらえてその不動点だねって議論はできそうな気がするんだけど,そういうデータ型の宣言ってのは,たとえば冪等性を表現している構成子でいえば
constr :: a -> (xs :: Set a) -> a ∈ xs -> xs みたい(xsが最後に来ているのは怪しい.xsに対応するSet aな型を返すべき)な感じで書くような気がするけどこれ依存型ですね.
依存型の圏論的な扱いってのもあるとは聞いたし書籍もあるらしいけどよくわからない...

いずれにせよHaskellの実装では内部的には二分木にはなっているけど,これはもろもろの則が足りてないのでSetとしてはこのあたりの則をサポートする関数を使って構成するようなAPIになってて,TipやBinは公開してないので,このデータ型をみてSetのF代数だと思ってはいけないから二分木を圏論的に扱えてもそれはSetの圏論的な扱いとは言えなそうですね.

@igarash1 has joined the channel

クイックソートのピボットの選び方についての質問です。

ピボットとして先頭要素を選ぶよりランダムな位置にある要素を選ぶ方がよいという記述をみかけることがあります。例えば「珠玉のプログラミング」とか。
両者を比較すると（ソート対象はランダムな並び順とします）

- 比較回数の期待値は変わらない。
- 最悪パターンでの比較回数も変わらない。
- 最悪パターンが起きる確率も変わらない。
- 比較回数を確率変数とした確率分布も変わらない（上で書いていることはこのことの特別な場合でのこと）。
- 並び順を一つに固定して考えた場合、前者は並び順パターンによって比較回数のばらつきが大きいが、後者はすべてのパターンに対して同一の期待値になる。これが後者の（唯一の？）利点。
- 補足：これは、例えばソートされた並びを前者でソートすると必ず O(n^2) になるが後者では期待値は O(n*log(n)) になる的なことを言いたい。

と考えているのですが正しいでしょうか。