iijmio 使いきり

iPhoneのlogを見たら、facebook が50GBとかでてる...

だから、動画に引っかかっちゃダメってことね

9/28あたりから、きれてたらしい。どうりで、遅いと思ってました

Ingress には差し障りがないらしい

最近のビール

まぁ、CPAPのせいか薬のせいか知らんけど、血圧と体重が減ってて...

しらばくは調整中な感じですね

Wordle 400

まぁ、運がよいだけですが...

茶店で Agda を書きながら Ingress

ってな感じです

mlock

どうも、macOS だと System のSecurityを落とさないと使えないらしく... SIP を切るってやつね

Recovery mode から csrutil disable するだけだが...

まぁ、そもそも、macOSの機能として 大量のメモリを確保してもある程度は動いてしまうらしい

OSの課題の一つだが、いろいろ問題あるものの一つ

Linux kernel gdb の続き

commit 59a2ceeef6d6bb8f68550fdbd84246b74a99f06b
Merge: d2f38a3c6507 0e9beb8a96f2
Author: Linus Torvalds <torvalds@linux-foundation.org>
Date:　　 Tue Nov 9 10:11:53 2021 -0800
　　　　Merge branch 'akpm' (patches from Andrew)
　　　　Merge more updates from Andrew Morton:

これで

　　　　git diff 0e9beb8a96f21a6df1579cb3a679e150e3269d80 59a2ceeef6d6bb8f68550fdbd84246b74a99f06b -- Makefile
　　　　@@ -847,44 +850,6 @@ ifdef CONFIG_ZERO_CALL_USED_REGS
　　　　 KBUILD_CFLAGS　　+= -fzero-call-used-regs=used-gpr
　　　　 endif
　　　　
　　　　-DEBUG_CFLAGS　　 :=
　　　　-
　　　　-ifdef CONFIG_DEBUG_INFO
　　　　-
　　　　-ifdef CONFIG_DEBUG_INFO_SPLIT
　　　　-DEBUG_CFLAGS　　 += -gsplit-dwarf
　　　　-else
　　　　-DEBUG_CFLAGS　　 += -g
　　　　-endif

とばっちり消されてるっのはわかったんだけど...

ここからさきは、どうすれば良いの?

OSの補講

ChatGPTもあるので、割と提出されていてよろしいです。Discord にも割と応答がある

のだが、 教科書の問題がなぁ

ChatGPTで採点しろって書いてあるんだが、

　だめだめな解答をぼろほめ

で、それに本人が気がついてない… これは痛すぎだろ…

Linux Kernel Debug の Kernel 6.11 はあきらめ中です…

Linux Kernel Debug

去年はさぼったので、今年は update しようと思ったが...

Kernel 6.11 で vmlinuxを -g をつけてコンパイルすることはできないの?

ansible script があるので楽勝だったはずなんだが

kdb / kgdb を今からいろいろいじる気はないかなぁ

はずれな台風シリーズ

水曜日は昼に歯医者さんにいったら土砂降りで、その後は鳴かず飛ばず

おかしいなぁ、台風直撃なはずだろ〜

Agda の続き

千行分くらいを書き直しているんだが、Invariantの構造にそって再帰を書いてっていう方法でいけそうなんですが、

場合分け12個あるうちの4個までかけた。残りがなぁ...

やりかた間違えているようなんだけど、まぁ、いいかな。いや、分量自体は増えるんですけど...

とにかくできることはわかってるので、やればよい

で、この Invariant の計算が両方向で成立することがわかると、insert だけでなく delete も書けるようになるらしい

モフモナの本棚

まぁ、そのうちダメになるとは思うんですが、10年もってはいるんだよな

工夫するとよい説もあるらしいんだけど、うちのいくつかの本棚も同じような感じ

台風ハイ

まぁ、沖縄良くある話なんですけどね

それほど大きくもなさそうなんだが、9月の台風は迷走することが多いからなぁ

なんとなく、飲み屋さんでも微妙に盛り上がっているような...

怪獣8号

シンゴジからの流れなのかな。解体班の話で進むわけもなく…　そっちの話も面白そうだったんだけど

フリーレンは漫画の方が先だったんですが、こっちはアニメの方を先に観ました

十分楽しいですけど、いろいろ急ぎすぎなのがな

まぁ、おっさんが出てくるのは良いんだが、声がタイバニのコテツと似てるのはどうなのかな

https://kaiju-no8.net

かけ算の話

なんと、信じられないことに、まだ続いていたりするんですけどね

かけ算の本質が何か

それはもちろん対称なかけ算もある

でも、

＊ 加算の繰り返し、しかも、高階の意味を持つもの

って方が本質なことは当たり前。それは少し考えればわかる。実際、掛順によって意味が異なることは簡単に理解できる

それが群、環、圏につながるのも当然

ってわけなんだが、それらを拒否する謎の人たちがな

でも、それらも面白くて

＊ 掛順は二つ別にある

までは良い。そこで「それらは同じもの」と思うのが間違ってる。「同じ意味の場合もある」くらいだよな

そこから「国語の問題」に陥ちると致命的になる。それを阻止するのが目標ね

国語の問題に関しては、トンデモ以下の話。単位ごとの交換で掛順も一つになるみたいな話がどこで通用する話になったのかが謎すぎる

しかも、それらが禁則と結び付いてる

単位のサンドイッチは単なるかけ算の意味の否定の作業で対称なかけ算にする作業でもあるのだが、それらが禁止ってのが変過ぎる

どうも「特定の世代」の話なんじゃないか説もあるっぽい

Ingress のやる気

どうも心臓の調子の問題だったらしく

アブレーションのあとで、回復しつつあるらしいです

どっかで見かけた車

どうすれば、こういうことになるのか

まぁ、単に放置されてしまったってことか

誰もいない大学

割と結構好きかな

昔の学生がたくさんいた頃は、必ず誰かがいたもんですけどね

今は、夏休みだし、学生もいない感じ

404をのぞいたら、学生が一人いてさ。「せんせ〜、なんか用ですか?」いや、なんにもないけど

CPAP

不整脈は

　　飲酒→無呼吸→高血圧→腎炎→心臓

という経路だって話で、学園通りの名嘉村クリニックへ。で、いろいろ話を聞くのだが

　　CPAPで治る

ってことらしい。で、CPAPを借りてくるわけですが、どうも保険には少し足りないらしい

最初は自費で保険料程度。

　　12月にもう一度、入院して検査で確定または、自費で継続

ってことらしいです。まぁ、facebookでも何人かいるからな

使ってみるんだが、なんか穴が開いてて、もれる。そこをテープで塞ぐと「息ができない」どうも穴のままで良いらしい

ちょうどアブレーションの手術と重なって、病院にも持ち込んだんですけどね。ま、寝苦しいわけですけど

なんだが、二週間くらいで少し慣れたかも。といっても

　　効き目があるようには見えないんですけどね

少し圧力上げるかとか言ってたが

まぁ、でも効いてるっぽいっみたいな話もある。良くわからん

どうも、CPAP貸与は儲かるらしく、そこで研究がストップしている感じがあるな

水曜日のバス

「今日は無料です」と何回聞いたことか...

ってわけですが、確かに普通よりはバスに乗っている人が多かったかも

がきんちょが多かった気もするけど、キリ短から乗ってきた人とか

バスが無料で名護までいく人も珍しいとは思うけどね

まぁ、困るのは「ゆいレールの終着駅から沖縄市方面」のバスが少ないことだな

97とゆいレールとの連絡を意図的におとしているのはなんでなのか

不可能ってわけでもないのがなぁ

Ingress

普天間一周ではすまなくて、二三回廻ってますが...

途中で割り込んでくるのがな。暇だな

Playerが少なくなってるわけで、それで赤が混ざってきてるわけだけど

たまに、active なのが混じるのが面白い

Twitterのかけ算のまとめ

[1] かけ算の定義

　　(ひとつ分)x(いくつ分)
　　同じ数ずつを足し合わせて全体を得る

　　構文を定義して、その意味を記述する一階述語論理の標準的な定義の方法

　　これを書き写す問題もあります

　　最初は「同じ数ずつのもの」を特定する掛順問題になっています

　　実世界の中にかけ算を発見する作業です

　　https://x.com/shinji_kono/status/1823272447099179395

[2] 原理主義者たちの禁則

　　かけ算は累加で定義され、二つの異なる掛順による異なる意味を持つ

　　それを否定して「どっちでもいい」にするために導入される思考制約のこと

　　いろいろある

　　1) かけ算の定義が禁則

　　定義はないので計算できない。アレイ図を数えるだと思う

　　定義に順序があるので否定する


　　https://x.com/shinji_kono/status/1821709743989170514

[3] 原理主義者のリセット

　　「かけ算はどっちでもいい」に対していろいろ理屈はあるわけだが、議論していくと

　　かけ算には二つの線形性がある。mvなら
　　(ひとつ分)x(mいくつ分)
　　(ひとつ分)x(vいくつ分)
　　あることはわかってしまう

　　つまり掛順には意味がある

　　それでは、困るのでいろいろ理屈を出してくる


　　https://x.com/shinji_kono/status/1824645692855554134

[4] 記号論理による記述

　　小1,小2の数と足し算かけ算の導入は、もちろん、数学の定義とそれから導出する計算や性質自体を学ぶ事ことでもある

　　小2のかけ算の導入の章題は「かけ算の意味」

　　(ひとつ分)x(いくつ分)
　　同じ数ずつを足し合わせて全体を得る

　　と、かけ算の記号と構文、その意味を日本語で記述する。これが定義

　　https://x.com/shinji_kono/status/1825181763460854098

[5]　C で記述した場合

　　nt c;
　　int mul(int a,int b) {
　　　 int sum = 0;
　　　 for(int i = 0; i<b; i++) {sum += a;c++}
　　　 return sum;
　　}

　　とすると加算の回数を副作用として取り出せる。するとこの関数はa,bに対して対称ではなくなる。結合則は副作用を含めて成立する

　　これがモナドによる対称ではないかけ算の意味

　　https://x.com/shinji_kono/status/1823878507564556601

[6] 面積のかけ算

　　それは面積でも同じ議論があって
　　　 5cm x 2cm
　　を長方形のかけ算と見ることもできるし、平行四辺形の1cmの平行四辺形ブロックのかけ算と見ることもできる

　　後者は面積にはならない。それは

　　　長方形の1cm² には等方性がある
　　　平行四辺形の1cm x 1cmにはない

　　測度かどうかの差ね

　　https://x.com/shinji_kono/status/1828882640642162998

[7] 理解できない学生を放置しない

　　「かけ算かどうか」がわからない生徒がいる

　　　同じ数ずつの集まり

　　がかけ算なんだと理解してない。それを判定する問題が掛順問題なのに

　　それを○にする×にするではなくて、理解してない学生を放置しない

　　だよね?

　　https://x.com/shinji_kono/status/1828892049183215838

[8] かけ算はどっちでもいい

　　「かけ算はどっちでもいい」ってのは、そういうレベルでの理解ってことね

　　それはいろんなレベルがあるが

　　交換則があるからどっちでもいい
　　かけ算に定義はない
　　かけ算の定義は掛け合わせること
　　アレイ図を数える
　　かけ算は面積

　　程度の理解な人たちだと思われてる。言わないけどね

　　https://x.com/shinji_kono/status/1827851115473641765

[9] かけ算の意味

　　(ひとつ分)x(いくつ分)
　　が構文を定義し

　　同じ数ずつを足し合わせて全体を得る
　　が意味を定義します

　　交換則とも両立するし、欧米式とは構文が異なるだけで意味は同じ

　　単位いじりや、国語の問題とも、おさらば
　　SI単位系まで理解できる

　　https://x.com/shinji_kono/status/1828765274868424969

[10] かけ算の書き方

　　掛順はかけ算の意味なので、構文とは別。それはかけ算の値が3x5と5x3とは別なことと対応してる

　　それでは掛順はどう表すかってことだが
　　　 (ひとつ分)x(いくつ分)
　　ってのが小学校での方式

　　中高で記号が入ったら
　　　(ひとつ分)x(mいくつ分)
　　とすると良い

　　mに対する累加/線形性とも言える

　　https://x.com/shinji_kono/status/1828577437187518886

[11] オウム返し+否定

　　原理主義者の

　　　 オウム返し+否定

　　パターン。これは考えなくてもできる。yes/noの質問もそれなんだな

　　かけ算の線形性、包含除で、さまざまなものを理解できるのに捨ててるからおかしなことになってる

　　PV=nRTから空気バネのバネ定数を導出することさえ禁則なの?

　　https://x.com/shinji_kono/status/1793794029282611697

[12] リストは非可換モノイド

　　3人ずつの乗車リストを台数分結合する
　　すると全員分の乗車リストができる

　　もちろん、一人ずつトランプ配りで結合したリストとは一致しない。順序が異なる

　　これは小2のかけ算の定義に一致してて非可換な意味をもつ。人数を見ると交換則が成立する

　　https://x.com/shinji_kono/status/1820371601143276000

[13] 高校の物理や化学でも掛順による意味の違いはある

　　かけ算な量は(ひとつ分)x(いくつ分)で二つの掛順で理解します

　　偏微分なので、一つの量をいくつ分とする。それ以外を全部固定する。n個のかけ算ならn通りのかけ算の意味があります

　　いくつ分は変化させるものなわけ
　　https://x.com/shinji_kono/status/1810780092861403184

[14] かけ算の「どっちでもいい」は単なる勘違い

　　a)一つはアレイ図を数えるを定義だと思ってしまう

　　b)もう一つは国語の問題「5つずつを2つ」と「２つの5つずつ」が同じ意味だから、掛順を含めて同じというもの

　　c)かけ算には意味はなく値だけとか、ダメなかけ算の定義の発明は、後付けの理屈

　　https://x.com/shinji_kono/status/1806087052532109418

[15] 不快な議論

　　不快な議論ではある。普通の人が参加しないのはそれ。原理主義者たちも、それを学習しているらしい。総攻撃みたいなのをくらったことがある

　　でも「交換則があるから、どっちでもいい」だと「循環論法ですね」で反論終了。公理だとかでも同じ

　　教科書のかけ算の定義のスクショで総攻撃は沈黙しました

　　https://x.com/shinji_kono/status/1827521568681160715

[16] 運動量やPV=nRTでの理解

　　運動量やPV=nRTを理解していれば、そこで使われている変数それぞれに線形性があり
　　　 (ひとつ分)x(いくつ分)
　　で考えられることがわかる

　　同じ数ずつを足し合わせて全体を得る

　　の同じ数ずつのものもなんだがわかる。そして掛順を理解する

　　Reboot/遠野/itachiは理解できてないので議論を続けられる

　　https://x.com/shinji_kono/status/1827401240348934306

[17] 素朴実在論とかけ算

　　素朴実在論者は、かけ算を自然にあるものと思いたい。自動的に対称になるもの

　　そこで計算し始めると、計算は対称ではないことに気がつく。でも交換則で値は対称になる。そこで、計算とかけ算の意味を忘れる

　　すると、本来の実世界のかけ算だったものは無意味な値になり、世界を説明してくれなくなる


　　https://x.com/shinji_kono/status/1826171991998578837


[18] かけ算とV=IR

　　かけ算な法則はいろいろある
　　　V=IR
　　はそのひとつ。かけ算の定義
　　　(ひとつ分)x(いくつ分)
　　　同じ数ずつを足し合わせて全体を得る
　　は述語でもある。つまり、これが成立する状況ってこと

　　オームの法則の導出を見るとわかるが、電流は電子の移動であり、それは導体が均一なら一様に移動する

　　https://x.com/shinji_kono/status/1825991786243772568



[19] (x - α)(x - β) = 0

　　ax² +bx + c　= 0
　　(x - α)(x - β) = 0

　　この二つの式から解と係数の関係が出てきます。かけ算の意味とは、かけ算の外にある論理式で記述された引数の性質のことです

　　この時にかけ算は対称で交換可能なので、α とβ は区別できません。つまり、α = β となります

　　どこか間違いました?

　　https://x.com/shinji_kono/status/1821449113004916931

[20] 同じなのは足し合わせた時の総数

　　2x5 は2つずつのもので
　　5x3は5つずつのもので分割する考え方

　　同じなのは足し合わせた時の総数

　　この区別がついてない。あるいは区別を禁止してる。なので、交換則が理解できなくなってる

　　5kg x 2m/s = 2kg x 5m/s を交換則でない
　　5kg x 2m/s = 2m/s x 5kg の分割が同じ

　　とかの間違いになってる

　　https://x.com/shinji_kono/status/1822049208679239790

[21] 単位とは

　　(基準の量ひとつ分)x(いくつ分)
　　で、基準の量には示量性相加性が必要

　　このかけ算の定義にそったSI単位系の当たり前に

　　「なにを言っているのか」
　　「支離滅裂」
　　「出鱈目」

　　と言ってくること自体が、原理主義者の単位のサンドイッチの禁則であり、彼らの勘違いの症状そのものなわけ



　　https://x.com/shinji_kono/status/1809380754683736186

[22] 間違ってるかけ算の定義

　　「かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる

　　0)値が同じなら式も同じ(式に意味はない)
　　1)定義はない (半環など未定義演算
　　2)アレイ図を数える (直積濃度
　　3) (いくつ分)x (ひとつ分)の両方が成立
　　4) (いくつ分)x (ひとつ分)との不定状態

　　https://x.com/shinji_kono/status/1789688104993055209

[23] 自分で本を読んで、自分で考える

　　それを勧めます

　　教科書を読んで理解する。問題を解いて理解したという安心感と自信を得る

　　才能とかと関係なく大切なことです

　　https://x.com/shinji_kono/status/1799567709493158199

Blueray へのコピーはだいたい終わったんですが

その後で index を読もうとすると 50枚中2枚読めない

で、一枚はこれ。もう一つは良くわからん

いや、書き込み終わったあとで確認しろと思うわけだが、なんか量が多いのでいいかな

テープは50TBなんてのがあるようですけど、NASのバックアップとして悪くはないかな

もっとも、個人で使うってのは微妙か

BD index

いや、そんな機能くらいついてろよってところなんですが

前回やったのは7月?! まぁ、いいんだけど

問題はすっかり忘れてるってことね

MBP ではだめで、GPD+ でやるんだが、Ubuntsu 側から見えないんだけど

まぁ、PowerShell のコマンドで読めば良いだけではある

Copy-Item -Path "E:\BDAV\PLAYLIST" -Destination "C:\" -Recurse

ですか