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で色々試してみたら、このコードでいう ≅-elim が JMeq_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に関する定理も示したっぽいが詳細は真面目に読まないと分からなそう…)

今週のHaskell :haskell: Weeklyから！ :tada: :blue_book:
https://np.reddit.com/r/haskell/comments/9q6edo/category_theory_for_programmers_by_bartosz/

@ has joined the channel

このペーパーに記述されている数式（表現？）をわかりやすく解説している書籍/資料ってありますかね。。
https://cardanodocs.com/files/formal-specification-of-the-cardano-wallet.pdf

@lotz OK! 書いた本人に聞いてみます。何かわかったら共有するね。

ありがとうございます :ok_woman:

ゲーテルの不完全性定理を数学ガール読んで触れてるんだけど
「形式的体系に矛盾する文を公理として入れると、任意の文が証明可能になってしまう」というの
「単純型付きラムダ計算の意味論に無限型を入れると、任意の式が型付け可能になってしまう」というのにめっちゃ似てる気がする

@ 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.

@shigeo has joined the channel

Free objectについてはこのスレッドで初めて知りましたが、Free monadとの関係は確かに興味深いですね、勉強してみたい

理解できていなかったら申し訳ないのですが、 η が identity natrual transformation だとすると x は U(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 のネストの深さを表す）

おお、確かに x は Free 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."

@mi-chang has joined the channel

@jeedo has joined the channel

@ has joined the channel

@rot has joined the channel

@fumi has joined the channel

@kilo has joined the channel

@take-cheeze has joined the channel

https://identicalsnowflake.github.io/Cantor.html
カントールの対角線論法をHaskellのコードで解説

:tada: :books: 本になったんですね！ https://damepo-lab.booth.pm/items/1051034
https://twitter.com/mod_poppo/status/1088487524433981440

圏論関係の記事を書いたんで載せときます https://hexirp.github.io/blog/articles/category_theory_for_traversable

めっちゃ興味あります！！！
ありがとうございます！！
後で読みます！！！

@koyama41 has joined the channel

「合成射の結合律」を圏の公理の1つというのに違和感がありますが、皆さん的にはどうでしょう？？

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

上記を定めて、それらによって結合律が導出されるという方が、思考の流れとしてはしっくりくるかなと

可換性というのはそれ単独で公理化できるようなものなのでしょうか？　あれはどちらかというと「常に成り立つものではないが、成り立つ時に限りいいことがあるよ」というシロモノに感じるのですが…

もちろん、射 f: a → b , g: b → c , h: a → c が存在したからと言って、 h が f , g の合成射とは限らないですが、2つの射 f , g の作用や関係性を合成射 g ⚬ f は1つで表すとするわけですよね？

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

ただ単独で公理化できるの？というのは確かにわからんですね…

そもそもで、 合成射は、合成元の射それぞれ (がたどる経路) と可換 とならないような合成射って考えることができるんでしょうか？ (もし考えることができるのであれば、可換性は公理として必要なくなるなと)

(あまり議論を理解してないのですが)その2点を認めると結合律が導出できる、というのがよく分からないです

@myuon_myon
「合成射の存在」と「合成射の可換性」をこの図式によって「公理」として定めれば…
(本当は唯一性は可換であることから言えるのでいりませんが)

@myuon_myon
「結合律」は以下のように「定理」として導出できるのでは？ということです

@Guvalif ありがとうございます、論点理解しました :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) が等しいってどうして言えるの？みたいな疑念はあると思うんですよね