haskell-jp / math #8

確率関係は正しいと思います。利点としては、実用上ソート済みのデータがうっかり入ってしまう事が多々ある(意図的な攻撃含む)ので、そういう場合に容易にワーストケースに入ってしまうのが危険だからだと思います
確か内部でソートしてるサーバーにワーストケースを放り込む事でDoS攻撃するみたいな手法があった気がする
@oza777you has joined the channel
@9647142 has joined the channel
@moriwm77 has joined the channel
@takeru.t has joined the channel
hiroyuki.m.nishiyama
@hiroyuki.m.nishiyama has joined the channel
確率関係について,より正確な主張をすると,「列の長さを固定してありうる入力それぞれが等確率で出現する」と仮定すると,全て正しいです.入力の出現の確率分布が一様分布でないときに問題が起きるわけなので.
@stekitou has joined the channel
モノイド以上、群未満な構造の型クラス集だそうです。
https://github.com/blamario/monoid-subclasses
@wasabi.nvim.st has joined the channel
@yoshihiro503 has joined the channel
@yatiwataru has joined the channel
@inzembla has joined the channel
@momohatt10 has joined the channel
@tempxla.public has joined the channel
@selty524 has joined the channel
@koto.chiba.none has joined the channel
@nakayoshix has joined the channel
@takato.h0rikosh1 has joined the channel
@baavv914 has joined the channel
@nmjr31 has joined the channel
@las has joined the channel
またまたモジュラー演算のライブラリーが https://github.com/Bodigrim/mod
@takohati0821 has left the channel
@kai.tenyatendon has joined the channel
示せない定理があるので、分かりそうな方見てもらいたいです。よろしくお願いします
https://mizunashi-mana.github.io/blog/posts/2019/12/algebraic-compact-functor/
この件解決しました
TaPLすら読んでないので素人考えなんですが、
Hask is not a categoryってやつ、
「undefinedと何かの比較結果はundefined」とおけば、
「Haskは圏でなくはない」までなら示せるのではないでしょうか。

というか、直観主義からいうと比較できちゃってる方がおかしい気がする

https://wiki.haskell.org/Hask
直観主義論理、syntacticにはintermediate truthであることが証明できる論理式はないので、面白いとは思いますがどういう風に一般的に定義しようか迷いますね…。
以前このスレッドで話題になった不動点意味論を採用し、ある計算ステップに注目して示す、みたいなのを妄想してます

不動点意味論の計算ステップでは、⊥は「他の値に計算される途中」の場合もありますから、 () <> ⊥ などとできないのは自然だと思います
@ymdpharm has joined the channel
@kiboreeb9m14d has joined the channel
@ktsubota has joined the channel
@mathre314 has joined the channel
@stefan_pavikevik has joined the channel
@yohta.kimura has joined the channel
mealy machine って「関数プログラミングの楽しみ」10章の Auto と同じ型ですかね。そうだとしたら ArrowApply ではなかったはず。
「Auto 用の、型は合うこれこれの app を定義できるが外延性を満たさないことを示せ」という練習問題までありました。
Lugendre さんの Qiita の記事、ちょっと typo がありますね。
「右から左の」と「app :: a (a b d, c) d」。
私もそう思ってたんですが、ところがMerlyのArrowApplyインスタンスはあるんですよね https://www.stackage.org/haddock/lts-15.1/machines-0.7/src/Data.Machine.Mealy.html#driveMealy
ちゃんとlawを満たしてるか確認していないので明日あたりやってみます
@tanaq has joined the channel
やってみたところ、lawを破っているという事実が発覚しました https://gist.github.com/as-capabl/0bce5645f9eba1eae2cf7a83b3418626
• 原理的に不可能なのか?それとも単なるバグか?
• lawを満たすものについては、常に同型があるのか?もっと言うと、lawから同型を導けるか?
について、引き続き考えて行きたいと思います。
• 「関数プログラミングの楽しみ」に「Auto は(ArrowApply の)インスタンスではない」と書いてあるくらいなので原理的に不可能なのだと思いますが「存在しないこと」の証明は難しかったりしますよね。
• 型(関手?)としての同型があることが前提でその上で law を満たせばモナド同型ということではと思います。(検証してなくての想像)
@zionian693 has joined the channel
@shin1hi has joined the channel