㌦の時間じゃん

Wordle 273 5/6*

⬛🟨⬛⬛⬛
🟨⬛⬛⬛⬛
⬛🟩🟨⬛⬛
🟩🟩🟩🟩⬛
🟩🟩🟩🟩🟩

#Wordle

オウム後継団体の資産、２年前の６分の１に…収益事業を報告せず（読売新聞オンライン） - Yahoo!ニュース
https://news.yahoo.co.jp/articles/b810a85afc9e05335f1f807a5eb35533de4aaca2

> アレフは２０年２月以降、収益事業に関する資産などを報告しなくなり、２１年５月以降は構成員などの報告も拒否。

そんな不穏なことになっとったんか
怖いな

btrfs で "block group XXXX has wrong amount of free space" が毎回同じブロックグループに対して出てきて、しかもこれ -oremount,clear_cache しても直らず次のブートで毎回出てくる……

よくわからんので remount ではなく fstab 弄って s/space_cache/clear_cache/ してみます

このアカウントは、notestockで公開設定になっていません。

1番目が最初の次の要素でないこと自体が異常でしょ (異常者並感)

0が O で 1 が Succ(O) なんだから最初の要素は0番目に決まってるでしょ、異常な人間社会の調教に負けないで理性働かせてもろて

えっ、自然数が加算について閉じていない世界があるんですか？？？

まあ冗談はさておいて (100%本気だけど)、 0-based index については C から入った人の意見だけに反論しようとすると「『ポインタとの加算だから……』とか言ってるしポインタのある言語固有じゃん」などとなりがちなんだけど、本質はそこじゃなくて「n回最初の要素を捨てたらn番目の要素が出てくる」の方がモデリングとして適切 (cf. Haskell)

それは自然言語が腐ったモデルの上に作られてしまったからであって、自然言語から離れた「作り直せる」世界でそのようにする必然性がない

言ってみれば「プログラミング言語だからといって無理に自然言語っぽい文法にする道理はない」に近いですかね

2000年が20世紀で2001年が21世紀なんですよ (?)

0を “発見” できなかった文明における「区間」の扱い、前が開いていて後ろが閉じている半開区間になりがちで異常

iterator.nth(n) が iterator.skip(n).next() と等価であるということです

べつに「人間の †直観† に近い方が良い」という派閥の有用性もわかるにはわかるんだけど、それはあくまで人間が汚いけどしょうがないよねという妥協の上での最善を求めるものであって、つまり「人間世界の汚さを輸入する」ことに合理性のある文脈でしか受け入れたくない設計だということですね

たとえば事務員が扱う言語であればこそ、自然言語に近い文法を使うことが正当化されるということです

もっと適切に言うなら、「データのモデルを構築する専用の訓練をさせたくない人の利用を想定しているなら」とかになるかもしれない (ﾁｸﾁｸ言葉か？)

我々はバナナを扱っているのではなくバナナを表現するデータを扱っているし、そういう「翻訳」は情報システムのあらゆる場面に暗黙に存在しているのだから、敢えて特定の場所でだけその「翻訳」を許さないという決断をするなら、相応の理由がほしい

大抵の場合は「教育コストかけたくない」、次点で「既存リソースの翻訳をしたくない」あたりがありがちな理由なのかな。知らんけど。

「論文が全部 1-based index 使ってるからミスがこわいし翻訳したくない」とかは相応の合理性を与えられている例

ｺﾛ試合するか

ｺﾛ試合とはコロシアムでの試合のことです

型システムは迂闊に強力にしすぎるとコンパイルに100倍の時間がかかったり型を決定不能になったりするので、まあその辺りは必要に応じてコストかけてもらう形で

型システム、すーぐチューリング完全になったり NP 完全になったりするので

既存の言語でもガバ型をもうちょっと厳密にしたいじゃん？ みたいな話はちょっぴり研究で手を出したやつなので

強力な型システムほしい……

s/強力な型システム/強力で多項式時間で決定可能で現実的に高速な型システム/g

あとついでに推論も楽だと嬉しいな

型検査器の裏で SAT solver が動くのは嫌だ！！！

このアカウントは、notestockで公開設定になっていません。