文字列の長さの分、かけられる文字列を結合するってだけですけどね
% perl -le 'print "abc" x length("de");'
abcabc
% perl -le 'print "de" x length("abc");'
dedede
と非対称な演算になる。長さをみれば、普通のかけ算なので 6 で同じ
Perl では x という演算子で計算できる。文字列のかけ算という認識なわけだな
何の問題もない普通の文字列のかけ算だよね。数学的にはモノイド上の乗算で、非可換ってだけ
これが反順序たちにとっては阿鼻叫喚らしい
こんなのかけ算じゃない!
みたいな話ね。なにやってるんだかね
リストを使ったかけ算は非可換になるってのは、2024の最初辺りには書いてるんだが、
反順序たちはわからない
っていう問題があるらしい。目で見える掛順の非対称性ってわけですが、これに拒否反応を出してしまうのがだめなところなわけね
算数の教科書の最初の「かけ算の絵」自体も、これと同じ構造を持っているわけだが、見えない人たちには見えない
もっとも、PV=nRTの瓶三本
PV=nRT → P(3V)=(3n)RT
にも文句をつけるのが反順序。P(3V)=(3P)Vだが、瓶三本で圧力3倍にはならないだろ? これで掛順を理解しない人たちとの話なのでね〜
Seeker's eye
Saturday, 5 April 2025
Friday, 4 April 2025
ガンダム Gqux
そういえばブックレットを配っているから、もう一回観にいくんだと思ってたら最終日に
ブックレット豪華と思ったら、中はスクリプトが大半でした
券を買うときに席をみたら「自分一人」
最後に特典映像がついていた
また、魔女なのか
Thursday, 3 April 2025
Wednesday, 2 April 2025
Graph から CCC の普遍問題
Graph から CCC を作るのはできたので、普遍問題をやってるんだが
直積やCurry化の構造は、グラフ/公理の外にある
なので、その部分は「単にコピーするだけ」になるらしい
確かに、元の圏 A と、そのCCC である CCC A は別なので、まぁ、そうなんだけど
なので、CCC functor が単なる普通の関手でいいことに。なんだそれ? それでいいのか?
直積やCurry化の構造は、グラフ/公理の外にある
なので、その部分は「単にコピーするだけ」になるらしい
確かに、元の圏 A と、そのCCC である CCC A は別なので、まぁ、そうなんだけど
なので、CCC functor が単なる普通の関手でいいことに。なんだそれ? それでいいのか?
Tuesday, 1 April 2025
Graph からCCC
昔、Graph から圏はできたんだが、CCCをPostive logic経由で作るっ4てのができなくて、
Sets への関手を作って終わらすって技を出してたんですが、
それだと、Setsの部分圏がCCCになってるかどうかわからない
なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた
Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん
f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)
という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は
fmap (g ∙ f) z ≡ fmap g (fmap f z)
という分配則があって、それを使うと証明できた。そういうことなのか
それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、
e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]
が、うまくいかない。でもじっとみてると
関数外延性を仮定するといける
らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです
で、まぁ、Graph から CCC はできた。
https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda
このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは
で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる
Sets への関手を作って終わらすって技を出してたんですが、
それだと、Setsの部分圏がCCCになってるかどうかわからない
なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた
Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん
f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)
という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は
fmap (g ∙ f) z ≡ fmap g (fmap f z)
という分配則があって、それを使うと証明できた。そういうことなのか
それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、
e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]
が、うまくいかない。でもじっとみてると
関数外延性を仮定するといける
らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです
で、まぁ、Graph から CCC はできた。
https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda
このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは
で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる
Friday, 28 March 2025
Subscribe to:
Posts (Atom)