haskell-jp / math #6

:thinking_face:.oO(定理証明器関係のchannelも作ろうかな...)
https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification-draft.pdf
これですかね。
誤解していたらすみません。
どんな時でも型がちゃんと付いておかしなことにならないことを証明した?
ありがとうございます!読んでみます!
pdf斜め読みした感じだとtype soundness示したっぽいですね
この話について「あれ?JMeqはCoqでも普通に定義できるよ?」って思って、Coqで色々試してみたら、このコードでいう ≅-elimJMeq_eq (このコードでの ≅→≡) を仮定しただけでは証明できず、 eq_JMeq (このコードでの ≡→≅ 。公理なしで証明可能) が JMeq_eq の左逆射になることを仮定する必要があるっぽいなど、色々面白いことが分かりました
https://haskell-jp.slack.com/archives/C5666B6BB/p1538806549000100?thread_ts=1538705462.000100&channel=C5666B6BB&message_ts=1538806549.000100
ちなみにJMeqが定義できるというのはこんな感じ (ソースコード: https://github.com/Hexirp/progra-gist/commit/c2f3c7eebd1a465517af912e740f6864d9280486)
Inductive JMeq (A : Type) (a : A) : forall B : Type, B -> Type :=
| JMeq_refl : JMeq A a A a
.
つまり
どんな時でも型がちゃんと付いておかしなことにならないことを証明した?
のことですかね。
type soundnessは一度型が付けばおかしなことにはならない、であって、型がいつでもつくことは含まないです(今回もそれは無理だと思います)
(あとtype checkerに関する定理とinterpreterに関する定理も示したっぽいが詳細は真面目に読まないと分からなそう…)
@yuya.gt has joined the channel
このペーパーに記述されている数式(表現?)をわかりやすく解説している書籍/資料ってありますかね。。
https://cardanodocs.com/files/formal-specification-of-the-cardano-wallet.pdf
@lotz OK! 書いた本人に聞いてみます。何かわかったら共有するね。
ありがとうございます :ok_woman:
ゲーテルの不完全性定理を数学ガール読んで触れてるんだけど
「形式的体系に矛盾する文を公理として入れると、任意の文が証明可能になってしまう」というの
「単純型付きラムダ計算の意味論に無限型を入れると、任意の式が型付け可能になってしまう」というのにめっちゃ似てる気がする
@dimension.sf has joined the channel
英語ですみません、解答がくれた方いたら日本語でも英語でも大丈夫です
<

nLab says:

a free C-object on x consists of an object y ∈ C together with a morphism
η : x -> U y in D there exists a unique g : y -> z for every f : x -> U z ∈ C

https://ncatlab.org/nlab/show/free+object paragraph 4 of section 1.

And I knows, though not 100% sure, that for a endofunctor f, the Free f is the y, and the C is the category of monads, and D is the category of endofunctors, U is the forgeful functor simply forgetting the identity and the composition of monad.

My question is, what is the x and η : x -> U(Free f)?
It seems that x can be the identity functor, and η is just the identity natrual transformation of Free f monad, is that right?
If it is not right, what is x and η?
If it is right, is there any other possible definition of x and η?

Thanks in advance.
@sean.westfall has joined the channel
Free objectについてはこのスレッドで初めて知りましたが、Free monadとの関係は確かに興味深いですね、勉強してみたい
理解できていなかったら申し訳ないのですが、 η が identity natrual transformation だとすると xU(Free f) では?
質問の意図がよくわかってないですが
C がモナド圏、D が自己関手圏、U が忘却関手の場合の自己関手 x に対する a free C-object on x は
Free x と η: x -> U (Free x) からなる組

ではないですかね。
data Free f a = Impure (f (Free f a)) | Pure a

とすると、具体的には η は次の liftF(「haskell lifF」でググれば見つかるのと本質的に同じやつ)
liftF :: x a -> Free x a
liftF = Impure . fmap Pure

ここで U は忘却関手なので U (Free x) と Free x を同一視して書いています。

x が Identity関手ならば free C-object on Identity は
Free Identity と liftF: Identity -> U (Free Identity) からなる組
ではないかと。
ちなみに Free Identityモナドは自然数の加算モノイドによる Writerモナドと同型のような気がします。(自然数が Impure のネストの深さを表す)
おお、確かに xFree f の f なら η : f -> Free f の方がidentity よりよっぽど意味があると思う。

ちなみに最初のスレッドの identity functor はHaskellのIdentityではなく、本物のIdentityの方。つまり type I a = aの方、残念だがHaskellにはこれを定義してもinstanceを定義できない

ありがとうございます
やはりちゃんと順番で勉強しなきゃだめなのね。。。

https://ncatlab.org/nlab/show/free+functor#free_objects
補足:
C がモナド圏、D が自己関手圏、U が忘却関手の場合の there exists a unique g : y -> z for every f : x -> U z ∈ C の g を f から構成するのが
g = foldFree f

だと思います。
foldFree http://hackage.haskell.org/package/free-5.1/docs/src/Control.Monad.Free.html#foldFree
この関数のコメントが "The very definition of a free monad is that given a natural transformation you get a monad homomorphism."
@mihchang has joined the channel
@jeedo has joined the channel
@e1q18048 has joined the channel
@aayhrot has joined the channel
@fmr23s has joined the channel
@kilo7998 has joined the channel
@takechi101010 has joined the channel
https://identicalsnowflake.github.io/Cantor.html
カントールの対角線論法をHaskellのコードで解説
圏論関係の記事を書いたんで載せときます https://hexirp.github.io/blog/articles/category_theory_for_traversable
めっちゃ興味あります!!!
ありがとうございます!!
後で読みます!!!
@koyama has joined the channel
「合成射の結合律」を圏の公理の1つというのに違和感がありますが、皆さん的にはどうでしょう??

1. 合成射が存在しなければならない
2. 合成射は、合成元の射それぞれ (がたどる経路) と可換 ⇒ 可換性に関する公理

上記を定めて、それらによって結合律が導出されるという方が、思考の流れとしてはしっくりくるかなと
可換性というのはそれ単独で公理化できるようなものなのでしょうか? あれはどちらかというと「常に成り立つものではないが、成り立つ時に限りいいことがあるよ」というシロモノに感じるのですが…
もちろん、射 f: a → b , g: b → c , h: a → c が存在したからと言って、 hf , g の合成射とは限らないですが、2つの射 f , g の作用や関係性を合成射 g ⚬ f は1つで表すとするわけですよね?

これを簡潔に言おうとすれば「可換であるとは何か?」が必要になりますし、なおかつその他の議論でも可換図式は頻繁に登場するわけですから、公理として必要じゃないかなと思った次第です

ただ単独で公理化できるの?というのは確かにわからんですね…
そもそもで、 合成射は、合成元の射それぞれ (がたどる経路) と可換 とならないような合成射って考えることができるんでしょうか? (もし考えることができるのであれば、可換性は公理として必要なくなるなと)
(あまり議論を理解してないのですが)その2点を認めると結合律が導出できる、というのがよく分からないです
@myuon_myon
「合成射の存在」と「合成射の可換性」をこの図式によって「公理」として定めれば…
(本当は唯一性は可換であることから言えるのでいりませんが)
@myuon_myon
「結合律」は以下のように「定理」として導出できるのでは?ということです
@tkskzyk0925 ありがとうございます、論点理解しました :hand:
それを証明とするには「合成はf,gを先にしてもg,hを先にしてもよい」が必要で、それが結合律ですので真ん中の射を経由するところで暗黙的に使っているのではないかと思います
ちょっと可換図式の書き方がまずかったかも知れないですね

ここで自分がずっともやもやしているのは、

- 可換性によって、合成射がミニマムな射の組み合わせ ( h ⚬ (g ⚬ f) であれば、 h , g , f ) に分解できる
- 同じようなミニマムな射の組み合わせを持つ合成射 ( h , g , f から構成できる (h ⚬ g) ⚬ f) ) は、可換性により等しい

と言えないか?ということです
分解するタイミングでかっこをはずしてますが、そこにトリックがあると思われます
分解しても射はもとあった合成の順番を勝手に変えてはならず、 h ⚬ (g ⚬ f) であれば、 h , ( g , f )と必ず括弧を付ける必要があるのではと(この分解後、括弧の付け替えを許すのが結合律です)
なるほど、確かに括弧を一律ではずして良いという保証はないですね

ひとまず腑に落ちました、ありがとうございます :haskell:
なんとなく、可換図式って、そういう「本当は気をつけなくちゃいけない細かいところ」を忘れてしまいがちになる気がしています…
可換図式って要は単に「等式」を図に書き換えているだけなので、元の等式が何なのかを結局意識する必要があるんだと思います。
つまり「可換性により等しい」っていう言い方はたぶん意味がなくて、「等しいということを可換図式で表すことにします」っていうだけなんじゃないかなあ、と思います
で、「可換とは何か?」という疑念があったと思うんですが、それってつまり「(射と射が)等しいとはどういうことか?」っていう話なのでは、と思います。
実際、 Hask圏(Haskellの型が対象で関数が射となる圏)で、関数と関数が「等しい」といわれても、関数同士は Eq で比較できないし、 ((\x -> x + 1) . (\x -> x + 2))(\x -> x + 3) が等しいってどうして言えるの?みたいな疑念はあると思うんですよね