Koji Miyazato
@viercc.bsky.social
Twitter(X), GitHubなどにいるのと同一人物です
openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6
興味: Haskell, 数学
openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6
興味: Haskell, 数学
アルファベット"a,b,c,...,x,y,z"を葉にもつ二分木を、ポーランド記法を使って文字列で表記することを考えます。
「2つの部分木`X,Y`をもつ木`(X,Y)`を作る」演算を、前置のドット(`.`)で表すことにします。例えば、"..x.yz.zx"は ((x, (y,z)), (z,x))を意味します。
ある語の_長さ_を、それがもつ葉の数とします。
長さnの、つまりn個の葉をもつ語は、いずれもn-1個の`.`を追加して書くことになります。
「2つの部分木`X,Y`をもつ木`(X,Y)`を作る」演算を、前置のドット(`.`)で表すことにします。例えば、"..x.yz.zx"は ((x, (y,z)), (z,x))を意味します。
ある語の_長さ_を、それがもつ葉の数とします。
長さnの、つまりn個の葉をもつ語は、いずれもn-1個の`.`を追加して書くことになります。
October 13, 2025 at 1:47 PM
アルファベット"a,b,c,...,x,y,z"を葉にもつ二分木を、ポーランド記法を使って文字列で表記することを考えます。
「2つの部分木`X,Y`をもつ木`(X,Y)`を作る」演算を、前置のドット(`.`)で表すことにします。例えば、"..x.yz.zx"は ((x, (y,z)), (z,x))を意味します。
ある語の_長さ_を、それがもつ葉の数とします。
長さnの、つまりn個の葉をもつ語は、いずれもn-1個の`.`を追加して書くことになります。
「2つの部分木`X,Y`をもつ木`(X,Y)`を作る」演算を、前置のドット(`.`)で表すことにします。例えば、"..x.yz.zx"は ((x, (y,z)), (z,x))を意味します。
ある語の_長さ_を、それがもつ葉の数とします。
長さnの、つまりn個の葉をもつ語は、いずれもn-1個の`.`を追加して書くことになります。
Day convolutionの"双対"みたいなものがありそうだけど、これ何だろ？疑似コードだけどこんな奴
data Day (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDay (exists x y. (C(x ⊗ y, z), f x, g y))
data DualDay (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDualDay (forall x y. C(z, x ⊗ y) -> (f x, g y))
(existsとforallはそれぞれcoend, endのつもり)
data Day (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDay (exists x y. (C(x ⊗ y, z), f x, g y))
data DualDay (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDualDay (forall x y. C(z, x ⊗ y) -> (f x, g y))
(existsとforallはそれぞれcoend, endのつもり)
September 20, 2025 at 4:39 PM
Day convolutionの"双対"みたいなものがありそうだけど、これ何だろ？疑似コードだけどこんな奴
data Day (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDay (exists x y. (C(x ⊗ y, z), f x, g y))
data DualDay (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDualDay (forall x y. C(z, x ⊗ y) -> (f x, g y))
(existsとforallはそれぞれcoend, endのつもり)
data Day (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDay (exists x y. (C(x ⊗ y, z), f x, g y))
data DualDay (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDualDay (forall x y. C(z, x ⊗ y) -> (f x, g y))
(existsとforallはそれぞれcoend, endのつもり)
親がノートPCを買い替えたので、古いほう(2012年~)を貰った。Windowsは11がインストール不能だったのでXubuntuを入れる。スペックはそこそこ。
September 18, 2025 at 8:43 AM
親がノートPCを買い替えたので、古いほう(2012年~)を貰った。Windowsは11がインストール不能だったのでXubuntuを入れる。スペックはそこそこ。
Bash詳しくないからChatGPTくんにとあるスクリプトの改善案を出させたら、すごい色々と一般化してくれたけど微妙に元スクリプトのユースケースを外してしまっていた。「そこまで一般化しなくてもいいし、元スクリプトのままの挙動ができないよ」と言ったら、*一般化したケースを残して*元スクリプトの挙動もできるように直してきた。
せっかく書いたから削除したくないってか？
せっかく書いたから削除したくないってか？
September 5, 2025 at 3:23 AM
Bash詳しくないからChatGPTくんにとあるスクリプトの改善案を出させたら、すごい色々と一般化してくれたけど微妙に元スクリプトのユースケースを外してしまっていた。「そこまで一般化しなくてもいいし、元スクリプトのままの挙動ができないよ」と言ったら、*一般化したケースを残して*元スクリプトの挙動もできるように直してきた。
せっかく書いたから削除したくないってか？
せっかく書いたから削除したくないってか？
100万回は言われてそうなことだけど、「バニラ」が「何も付け加えられていない」を意味するの、バニラアイスはバニラエッセンスを入れたからバニラなんじゃなかったのかよ！と思ってしまう
August 20, 2025 at 12:47 PM
100万回は言われてそうなことだけど、「バニラ」が「何も付け加えられていない」を意味するの、バニラアイスはバニラエッセンスを入れたからバニラなんじゃなかったのかよ！と思ってしまう
有理数rについて[r]をrに一番近いDouble型の値、sqrt(2)を√2に一番近いDouble型の値として、floor(r√2) == floor([r] * √2) が常に成り立つ[r]の範囲ってどの辺だろう
|r| < 2^49 ぐらい？
|r| < 2^49 ぐらい？
August 19, 2025 at 1:13 PM
有理数rについて[r]をrに一番近いDouble型の値、sqrt(2)を√2に一番近いDouble型の値として、floor(r√2) == floor([r] * √2) が常に成り立つ[r]の範囲ってどの辺だろう
|r| < 2^49 ぐらい？
|r| < 2^49 ぐらい？
型クラス(a la Haskell)とimplicit(a la Scala)は微妙に異なる意味を持っているし、更に「名前のオーバーローディング」であってそのどちらでもない用法や、「型クラスだがオーバーロードしてほしくない」「implicitだがオーバーロードしてほしくない」ケースもある
これら3つは交差部分がほとんどを占めるベン図だけど、ちゃんとどの領域にも実例があって、何かが別の何かを不要にしない
これら3つは交差部分がほとんどを占めるベン図だけど、ちゃんとどの領域にも実例があって、何かが別の何かを不要にしない
August 19, 2025 at 2:38 AM
型クラス(a la Haskell)とimplicit(a la Scala)は微妙に異なる意味を持っているし、更に「名前のオーバーローディング」であってそのどちらでもない用法や、「型クラスだがオーバーロードしてほしくない」「implicitだがオーバーロードしてほしくない」ケースもある
これら3つは交差部分がほとんどを占めるベン図だけど、ちゃんとどの領域にも実例があって、何かが別の何かを不要にしない
これら3つは交差部分がほとんどを占めるベン図だけど、ちゃんとどの領域にも実例があって、何かが別の何かを不要にしない
最近、行ベクトルに右から行列を掛けるスタイルの良さがわかりつつある
August 13, 2025 at 12:17 PM
最近、行ベクトルに右から行列を掛けるスタイルの良さがわかりつつある
論文Aを引用している論文Bを読んでるんだけど、Aの主張する定理の一つ(X)を使うとBの主張するメインの定理の一つ(Y)はより強い結果が得られるし、Bの議論のうち数ページを単純化できる。なんで使ってないんだろう？？？
(X)に誤りがあるとBは主張してないし、(Y)が(X)で単純化できることはわりと明らかなんだけど
(X)に誤りがあるとBは主張してないし、(Y)が(X)で単純化できることはわりと明らかなんだけど
August 13, 2025 at 7:13 AM
論文Aを引用している論文Bを読んでるんだけど、Aの主張する定理の一つ(X)を使うとBの主張するメインの定理の一つ(Y)はより強い結果が得られるし、Bの議論のうち数ページを単純化できる。なんで使ってないんだろう？？？
(X)に誤りがあるとBは主張してないし、(Y)が(X)で単純化できることはわりと明らかなんだけど
(X)に誤りがあるとBは主張してないし、(Y)が(X)で単純化できることはわりと明らかなんだけど
Reposted by Koji Miyazato
【津波警報 発表】
津波警報に切り替えました。ただちに避難してください。
＜津波警報＞北海道太平洋沿岸、東北地方太平洋沿岸、関東地方、伊豆・小笠原諸島、東海地方、和歌山県
weathernews.jp/news/202507/...
津波警報に切り替えました。ただちに避難してください。
＜津波警報＞北海道太平洋沿岸、東北地方太平洋沿岸、関東地方、伊豆・小笠原諸島、東海地方、和歌山県
weathernews.jp/news/202507/...
July 30, 2025 at 12:42 AM
【津波警報 発表】
津波警報に切り替えました。ただちに避難してください。
＜津波警報＞北海道太平洋沿岸、東北地方太平洋沿岸、関東地方、伊豆・小笠原諸島、東海地方、和歌山県
weathernews.jp/news/202507/...
津波警報に切り替えました。ただちに避難してください。
＜津波警報＞北海道太平洋沿岸、東北地方太平洋沿岸、関東地方、伊豆・小笠原諸島、東海地方、和歌山県
weathernews.jp/news/202507/...
投票先どうするかなぁ、選挙区のほうは決まってるが比例の方は「最悪」と「普通にダメ」と「各論ではまあ賛成できるところもあるが・・・」と「表面的にはよさそうだけど不安材料多い」からの選択
July 19, 2025 at 1:16 AM
投票先どうするかなぁ、選挙区のほうは決まってるが比例の方は「最悪」と「普通にダメ」と「各論ではまあ賛成できるところもあるが・・・」と「表面的にはよさそうだけど不安材料多い」からの選択
唐突に日本語が思いつけなくなって "Yay! That's exactly what I've intended." を直訳した
July 5, 2025 at 5:32 AM
唐突に日本語が思いつけなくなって "Yay! That's exactly what I've intended." を直訳した
Xで見たけど「飼い猫は人間のことを大きな猫だと思っている」みたいなやつ、「人間は猫を〇〇という点が違うだけの人間だと思っている」し、そもそも他者の理解というのは「〇〇という点が違う、自分と同じような存在」以外にありえない
July 4, 2025 at 11:34 AM
Xで見たけど「飼い猫は人間のことを大きな猫だと思っている」みたいなやつ、「人間は猫を〇〇という点が違うだけの人間だと思っている」し、そもそも他者の理解というのは「〇〇という点が違う、自分と同じような存在」以外にありえない
"char"をヒャーみたいに発音している人も探せば居そう
June 30, 2025 at 10:04 AM
"char"をヒャーみたいに発音している人も探せば居そう
チャットAIに数学的な事項を聞く→AIくん「これは難しいけど(有名人)が有限ケースを、(有名人)が無限ケースで反例があることを示してるよ」→おお！凄い！それが書かれた論文どれ？→AIくん「これ(実在の論文, 書誌情報完璧, URL付き)」→読む→全然書いてないじゃねえか！！！
June 5, 2025 at 3:57 AM
チャットAIに数学的な事項を聞く→AIくん「これは難しいけど(有名人)が有限ケースを、(有名人)が無限ケースで反例があることを示してるよ」→おお！凄い！それが書かれた論文どれ？→AIくん「これ(実在の論文, 書誌情報完璧, URL付き)」→読む→全然書いてないじゃねえか！！！
BDFFのリマスターまじ？と思ったけどもう10年以上経ってるからそうか・・・
June 4, 2025 at 4:39 AM
BDFFのリマスターまじ？と思ったけどもう10年以上経ってるからそうか・・・
数値リテラルを(それが表す数値ではなく)元の文字列表現に1対1対応する型で表したいことあるよなあ
June 4, 2025 at 4:13 AM
数値リテラルを(それが表す数値ではなく)元の文字列表現に1対1対応する型で表したいことあるよなあ
ChatGPT、ちょとふわふわした議論（設計のよしあしとか）を自分で明晰に分析してくれない感じがする。「コードを交えて説明して、最後に簡潔に要約して」みたいな指示をすると一気にシャープになるような・・・
June 3, 2025 at 12:31 AM
ChatGPT、ちょとふわふわした議論（設計のよしあしとか）を自分で明晰に分析してくれない感じがする。「コードを交えて説明して、最後に簡潔に要約して」みたいな指示をすると一気にシャープになるような・・・
eq : あるequivalence relation x ~ y
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと
May 30, 2025 at 9:19 AM
eq : あるequivalence relation x ~ y
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと
あーそっか、EquivalenceってGroupoidじゃないんだ
それはそうだ
それはそうだ
May 29, 2025 at 1:17 PM
あーそっか、EquivalenceってGroupoidじゃないんだ
それはそうだ
それはそうだ