RX

DXの琉球大学版らしいです

僕は関わなってないです。もちろん

がんばって〜

https://urdx.skr.u-ryukyu.ac.jp

会議用

スピーカーマイクとカメラ

カメラは四方を向いているらしく。円形に並んだ机を想定しているらしい

それは、日本的会議ってこと?

近寄りすぎると首から上が映らない

HP ARM Server Proliant RL300 Gen11

1U server ですけどね。うちは学生は macOS なのでサーバもARMだとコンテナとかを融通できる

なので評価機を持ってきてもらいました。128 Core 。Core数だけなら ARM がC/P良いらしい

HPの人も来てくれていろいろ聞くわけだが、まぁ、実機で評価しないとね。Ubuntu 22.05 support らしい

最近の新入社員が失敗を恐れて何もしないみたいな話もしてました。若いうちに失敗しないと

で、HPの人がいるうちに Server 設定にいくわけですが、まず、200Vがどこにあるから

　　現状のサーバが200Vなので、そのUPSに。「容量足りるのか?!」って話もあったが、GPU全力でなければ

HPは iLO なので、それから上げるわけだが、Display/Keyboard だと、

　　なんか画面が小さい。状況表示の一部に iLO が出てる。大きくできない

なんかLEDのボタン押せとか書いてあるんだがだめ。で、

　　その小さな画面からIP addressを設定して、ネット経由の iLO で接続成功!

そして、Ubuntu install !!! なのだが、

　　画面が黒いまま
　　HPの人「いや〜、立ち上がりに時間がかかるんですよ。Firm のチェックとか」

そのあほは切れんのか? 確かに時間がかかるが、

　　Ubuntu kernel tty00

で、また数分止まる。そこで HP の人は帰ってしまったんですが、続行

のんびり Ubuntu 22.05 ARM の install は進むわけですが

　　apt-cache READ error

くそ〜　いろいろ、みたけど、どうしようもなく、もう一度、そのまま。

　　で、今度は Ubuntu 22.05 install完了!

おお、何もしてないのに治った。次はネットワークね

　　これがぜんぜんつながらない。容易した旧サーバのGBICが、なんか認識しない

で、生きてるGBICを入れ替えたら接続できたらしい。理由は不明。ハードウェアではなくて、Switchの設定の問題らしいが...

で、とりあえず、ssh できるところまできました。よし、あとは

　　うちのサーバの ansible から設定だ!

その前に、HPのドライバといれて、Ubuntu 24検証して... まだまだ続きます....

腰のいぼ

取ってもらいました。足の指の方は先週見てもらった時にさっさと取ってもらったんだけど

抜糸って、何にもせずに抜くだけのね。少し痛いだけだけど。絆創膏もなし

なんかチーとか音してたので「レーザー」って聞いたら止血がとかいうので電気メスだったらしい

特に痛くもなく、そのまま大学に行ったんですが、帰ってきたら少し痛いな。ジーンとする感じ

そういえば、盲腸の時も麻酔きれたあとは、こんな感じの痛みだったっけ

ロキソニンはたくさんあるので要りませんって言ったんですが、かなに

　「ロキソニンはいくらあっても良い」

と怒られました。この程度なら要らんな。やせがまん好きなので

毎日書くから日記

いつも、ネタはないわけですけどね

酒飲んで起きたら、こんな時間だった

移行結果

http://cr.ie.u-ryukyu.ac.jp/cr-stack/

pukiwiki / growi からの移行はできたんですが、pukiwiki って誰が書いたのかわからないのか

growi は一応 user あるんだが、対応つけるのめんどい

なので、Author なしだな

Hugo は、やっぱり Frontmatter が邪魔。せめて別ファイルにして欲しい

あと、配置がだめ。Stack theme が post/hoge/index.md 形式なのが辛すぎる

なんか、別なのないかな。Markdown based static web のましなの。 いくつかは見かけましたが

自動タグ付けツールとかないのかな?

課金を惜しまないなら、全部、AIに突っ込で「タグつけて」だろうけど

local AI がこれから流行るのか?

Hugo / Pukiwiki / Growi

学生が残した Pukiwiki / Growi の Serverをメンテする気もないので、

　　Hugo に変換

なんだが、Hugo がかなりのあほでな〜 Stack のThemeが割とよさそうんなんだが、

　　Hugo のexternded modeを使う

いや、いいんだけど、なんで、それ default じゃないの? singularity containerを作り直し

Pukiwiki は、Ruby な変換 script を見つけたのでそれで。でも、

　　Hugo は Front Matter というゴミ

が必要。このゴミを Markdown の中に入れるというのがダメな設定で、結局、書き換えが必要

でも、他のツールと混ぜるのもな。そこまでは動いて、次は Growi

これは、Markdwon までは落としてくれるのを Anatouf が書いてるんだが、日付がない

それは、なんか JSON にdumpしてあるぞ。なんだそれ。元は MongoDB なはずですが

ところが生成した Front Matter な YAML が変な記号がとか文句言ってる。今日はここまで

デイリーミッションの奴隷感

コロナが収まってプレイヤーが増えたんだが、緑に二人転向したとかもあって

　割と多勢に無勢

それに、奴隷的にプレイしている人もいてなぁ。それに合わせると奴隷感がちょっと

デイリーミッション良くないよね。原神もIngressも

カードの切り替えで課金止めたってのあってさ

そんなわけで、Ingressは絶賛さぼり中です。割と自由です

真栄原の青の応援でもあれば再開するかも

ブルージャイアント

なんか、フードフリーにいくまで暇なので

上映中はいまいち気が乗らなくて。上原ひろみなのは知ってたんですけどね

ジャズ? まぁ、好きな方だけど、自分の守備範囲ではないな的なところがっあってさ

でも、こういう若い才能の突っ走る話はいいかな。フリーレンもそうなんだけど

　年寄りからの視点

みたいなのが結構入っててさ。全然知らないところから始めるドラマー。その成長を見る楽しさってそれだよね

才能で突っ走るのが、努力で行き詰まってる奴に言い放つ冷たい言葉とかさ

　でも、その行き詰まっている時が成長している時

だとかさ。自分も確かに突っ走っていた時あったよなとか

アンコールのシーンは原作にはなかったらしいんですが、もしかして本当に左だけでやってるの?

そんなわけで、結構良かったです

https://bluegiant-movie.jp/#modal

Mercurial の移行

さすがに2011もののサーバーをいつまでも使うわけにも

で、学科サーバにお引越しなわけですが、

　hg はそのまま使えない。singurality container の中

pyenv だと apt install python3.10-venv を要求するのか。まぁ、行れても良いんだが

　各人の$HOMEが汚れまくる

のは見えてる。まぁ、それでいいならいんだが。container で共有しろとは思う

で、~/bin/hg を作って、

singularity exec hg.sif hg "$@"

で良いらしい。はい、解決

次は pukiwiki と growi か。自分では使わないものだけどね。static に変換するんだが...

つけナポリタン

はちれんの新メニュー

オリーブオイルな麺をトマトソースにつけて食べます。チーズたくさん

自分ではパスだがな。でも、結構おいしい。学生には、とっても美味しいものらしいです

今日から授業かと思ったら明日からだった

今年も、なんかソースコード読むんですが、何を読むのか考え中

去年は Python + Numpy + Cuda でわりとだめだったので、自分の好きなもの読むかな

新兵器

T-fal って、あんまりお行儀良くないじゃないですか

カップめんとかにお湯入れるとき、結構こぼしてしまう。まぁ、お湯なんだから拭けばいいだけなんだが

で、なんか、新兵器を買ってもらいました

これなら、大丈夫。な、はずです

おでき

足と背中のところに... で、皮膚科に行ったんですが

　背中は座ると傷口がさける恐れがある

いや、別にさけても、またくれば良いんでしょとごねたんですが、

　形成外科送りに

んーがー。ちょっと大きくなるまで放置しすぎたか

なんかやらかした

宜野湾そばで、骨汁頼んだら、これ

まぁ、そこそこ、がんばりましたけどね。食べるところ、それほど多いわけでもないし

880円

お休み

まぁ、こういうの嫌いではないんだが

野嵩の中華そば

3/15オープンだったらしい。ソニーボーイから、少し横道にはいったところですね

そこそこ広いけど、二人で廻しているので、まぁ、時間はかかるようです

煮干しだしで、麺も良い。少し高めだが、むしろそれくらい取る方がいいかな

で、あえ玉なるものがある。替え玉が油そばっぽくなってる感じ。300円

頼んでみたんだが、ひと玉は多いな。半分できるのってきいたら「値段は変わりません」だそうです

麺少なめ+あえ玉半分とか良さそう

インストール大会

コロナ後の平常運転ですね

なんと今日の0時にセンタからの新入生用のアカウントが到着。間に合った

どうも手作業してるらしい。なんとかして欲しいなとは思いますけどね

今年はWindows組が数名。Let's note と Surface 。メモリさえあればWSL2 + ubuntu でなんとかなります

良い時代ではある。残りは MBP / MBA

PC高いのは大変だけどな

結構、2年次が来てくれてすばらしい。3年次編入組もがんばれ

かけ算の順序 (高階関数編)

かけ算の定義は、(一つ分)x(いくつ分) 教科書に載ってる。明確に順序がある

交換則の証明は数に対して成立するわけですが、一つ分は数とは限らない。なので

　小2のかけ算の定義は、数のそれより広い

そう言われてみれば、教科書には、きらびやかな絵で書いた例がたくさん載ってる。このかけ算は

　5個ずつお皿に乗ってるのが3枚

とかを直接扱っているわけ。それは実は

　高階関数であって、その変えす値はお皿と飴の構造

だったりする。これは、x=vt や PV=nRT でも言える。そして、それはかけ算の意味なのね。つまり

　かけ算は意味を返す高階関数でありえて、それは可換とは限らない

型が違えば可換の意味もないからな。そして、

　高階関数の意味には、かけ算の定義にそった凖同型がある

これは便利。

　x=vt や PV=nRT の性質は、t や V だけを増やすと、そのまま線形に増える

もちろん、交換法則は、その証明に十分な性質がかけ算の意味にあれば示せる。つまり、

　かけ算の対称性はただではなくて証明されるもの

まぁ、当たり前といえば当たり前

原理主義者たちの対称なかけ算は、対称性をちゃんと証明すれば良い。そういうものもある。結局、

　原理主義者たちが失う対称なかけ算は、それが証明されるならそのままある

でも、ただでは得られない。そこで、

　なんでって僕に言われても、かけ算の定義は変えられません

そこで変えたら、とんでも一直線じゃん。そういう人もいるけどさ

いろいろ、やらかし

4/1になったら教務情報システムにアクセスできない。聞いたら

　今年から更新は紙からメールになった

ちょっと。聞いてないんですけどと思って pick -subject したら、3通きてた。読まんだろ

で、のこのこセンターにいくわけですが

　職員証の期限が切れてます

げげ、なにそれ。自分はここの職員ではないのか?! まぁ、そんなに真面目に仕事してないからなぁ

そういえば、なんか二つ出てきた時に片方捨てたような。まぁ、再発行かなあ

　単なる紙

ですけどね。でも、センターのアカウントは再発行。勝手にパスワードくれるのか。紙で

いや、意外にセキュリティ高い方法かもしれん

金沢でみかけた変なものシリーズ

ガウティっぽいビル

この手のは住むといろいろ問題がでるものだけど

スペインもガウディの建物は観光名所だが、わりと迷惑がられているらしい

葬送のフリーレン

そういうblog書いてなかった不思議

なんか Kindle に入ってて、面白いと言われていたんですが、読み始めたら

　　なんか、とろい話で

のんびり進むのかと思ったら、いきなりヒンメルがおじいちゃんに

アウラでびっくりというパターン。出てるところまで読み終わった時点でアニメがスタート

　魔族とはわかりえない

みたいなテーマがあるわけですが、まぁ、自分はあまり共感できないが、それも変わっていくのかも

アニメは魔術師試験までですが、2期のあれも楽しみではある。アニメの戦いの描写は結構良かったので

アニメと漫画の乖離が少ないのも良いかな

学生も結構はまっているらしいけど、自分たちとは視点が異なるんだろうな

https://frieren-anime.jp

金沢でみかけた変なものシリーズ

まだまだ続くのか。今日はわらびーず

なんか、シャーレで、味噌とか塩とか売ってる

店員さんが白衣なのが点数たかい

大学でお散歩

金沢の増加分を徐々に落としたい

まだ、涼しいからいいけど、暑いときの方が効率はよい

Dune part2

観てきました。堪能しました


　ね

　た

　ば

　れ


といっても、読んでる人には関係ないか。第一部の終わりまでで、ちょうどいい感じ

小説にそって控えめな感じな描き方も良いかな。戦闘シーンとかは原作でもあっさりしたものだし

チャニが怒りまくってる。お母様とスティルガーは逝ってしまってるわけなので、ある意味楽しそうなんだが

日本語でも何回か読んだし、英語でも読んでるんだが、それでも

　え、そんな話しあったか?

なところが若干

続きは救世主だとだいぶ地味な話になるので、いろいろ変えてくるかも知れないですね


https://wwws.warnerbros.co.jp/dune-movie/

金沢でみかけた変なものシリーズ

え、全部、カタン? カタン大会か?!

さすが JAIST だな

自分的には少し苦手なゲーム。このゲームで勝ちたいかと言われると少し違うような

そして、そう思っている人と一緒にゲームするかというと、自分でも少し微妙

でも、他の人の戦略を見て「なるほど」と思うのは楽しいです

金沢でみかけた変なものシリーズ

割とアートが多い。金持ちなのか、そういう文化なのか。沖縄は那覇でもそんなにない

これは県立図書館のオブジェ。回転してる。動画で撮るほどのものでもないですが

図書館は入り口には特に何もなくて、オープンなのが良い感じ

いった時は、かなり天気が悪くて、図書館見学くらいがちょうど良かったです

金沢で見かけた変なものシリーズ

コンビニの山盛りカップ麺。安売りしてるらしい

地震で崩れたにしては、ずいぶん時間が経ってる

737で沖縄

JTAって737しかないの? 昔は737だと少しがっかりしたものだが

でも今はむしろ良い感じ

Class Jのシートが良くなったからかな

金沢はたくさん酒が飲めて良かったです

石川県立図書館

順調に飲んだくれてますが、図書館にも行ってきました。バスで30分

広くてセンスがよい。ほこりくさくない。やっぱり金持ちの街って箱物が豪華。JAISTもそうだけど

本の選択は、まぁ、市民向けだとこんなものかも。大学とか各学科のとは違うよね

ただ、カフェが一つしかなくて行列してました

ASDと脳科学みたいな講演をしてたな

JAIST

金沢からでも、相変わらずの陸の孤島っぷりが... 車なら35分なんですが

　　能美根上から「のみバス」で40分

小松からの予約バスなんていう手もあるらしい。まぁ、バスでいけるだけましか。OISTなみだな

まぁ、そういうの嫌いなわけでもないので、お昼ご飯食べてからのこのこと

OISTと違って公用語が英語だったりはしないんですが、研究室が広いのは良いな。

昔のさきがけの関係の先生とか、学生さんとか何人かと話してきました

キャンパスがオープンなのは陸の孤島のせいかも。この時期なので人は少なかったんですが

のみバスがぐるぐるいろんなところを廻るので少し車酔いしたかも

しばらく金沢

で、のんだくれているらしいです

得に予定なし

そうか、金沢というとおでんなのね

Godiva 買い占め

ライカムだと Godiva に寄ることが多くて、

　「カレ、ダーク20枚」

っていったら、最近は4枚入りの箱があるらしく。10枚じゃないのか。ところが

　「20枚ありません」

とかいってる。じゃぁ、ある分でいいです

　「ホワイトデーで、かなり出てしまって」

そうのかと思って、つつんでもらおうとしたら

　いやいや、20箱じゃないから

5箱でいいんですよ。20枚なんだから。危うく買い占めてしまうところだった

まぁ、明治のブラックでも良いんですけどね

マクドトラブル

わざわざ見にいったんですが、モバイルオーダーは停止中

店内のパネルからのオーダーは可能ですが、決済には1-2分かかってました

なんか、ビッグマックのソース増しが可能になってました。アプリからもできるようになるかも

少しすいてて、品物は割と早く来ました

原因の話はいろいろでるんでしょうけど、ネット関係みたいですね

Godzilla - 1.0

見てきました。そんなにゴジラファンじゃないし、あんまり気が進まないところもあって見送ってました

まぁ、賞も取ったし。いろいろ噂は聞いてたが、割と涙腺緩い方なので、泣きが入るのは良かったかな

予算制約なんだろうけど、そこそこ凝った作戦なんだから、ゴジラの変形はもう少しあるべきだったような

米軍がまったく関与しないってのもそれだろうけど、変だよな。米軍の士気高い頃だろうし

伏線なしでそれですかとか、バレバレなのとか、雑なんだが、まぁ、ゴジラ映画ってのはそういうものかも

でも、あの飛行機とか戦車とか軍鑑とかが動くってだけでうれしい人も多いんだろうな

　＊　＊　＊

これ登場人物は父母の世代。モブの服装がそれっぽいとか、子供の服装とか。バイクとか

街のスケール感がスタジオ的なのは、むしろわざとなのかも。昭和感は楽しめたかな

そう言えば白黒上映って話もあったっけ。確かにそっちの方が映画自体の昭和感がでるのか

確かに演技自体も昔風な感じだったし

gitgub copilot

何か知らんうちに切れてる。Agdaだとそれほどうれしくもないんだが、たまにばっちり当てるので

neovimのpluginをgit pull して終わりですか

この前の財布騒ぎで、いろいろカード関係が切れたのを良いことに切りまくってます

GPT4もしばらく要らんかな。Claud3 も試してみてます

なんか来年度も授業が多いんだよな

琉ラボ

普通に午後から出勤したら、なんか飯尾先生みたいなのが... 近寄ってみたら本人でした

学生連れて琉ラボ(地域振興館1F)にいくというので、少し冷やかしに。近所だし

起業支援系の施設らしく、そういうお話でさ。喉が不自由で質問しなかったが twitterにはいろいろ書いた

学生も「起業のリスクは?」とか聞いてたし、その辺は分かってる感じ

飯尾先生も「(社会的に必要とされていても)赤字な民間団体みたいなのはどうなの?」とか聞いててスルーされてましたが

Shadow Works も「金銭的に評価されない社会に必須な仕事」なわけで、

　起業して、金銭的に儲ける

という評価軸が完璧にずれてるという感じ。アンケートでニーズを確かめるなんて話もあったけど、

　Apple 1 を作った時に、50人にアンケートしたら、全員、「そんなもん要らん」

というと思う。そもそも、それがなんなのかもわからない。つうか、

　起業の話をするのに Apple を例にあげるんじゃない

と思いました

Nginx の IPv6

なんか気になってたんだが、どうも学科のWebにIPv6が通ってない。そういう課題を出してたりするんで気がついたんですが

pdoman / nginx に切り替えた時からだから、放置がひどい。ping6 が通らないところから..

結構いろいろあって

1) podman network が defulat IPv6 off なので明示的に ebable する
2) podman v4 で、また、IP4/IP6 のアドレス設定のやり方が変更 ( -ip ではなく -network のパラメタになった)
3) そもそも nginx の方でも、IPv6 の待ち受けの設定が必要
4) Fortigate で IPv6 Virual IP の設定が必要

最後のあたりですったもんだしたんですが、まぁ、通ったらしい

で学生に自慢するんですが

　みてもわからない

なんだが、「IPv6しか通らないAdroidスマホ」な学生は「おぉ、見れるようになった」とよろこんでました

卒業ハリーズ

このコロナ騒ぎでいろいろKnow Howが失われてて。僕もうっかりしてたんですが、

　　誰も段取りしてなかったらしく

いや、あの「一人二千円でお願いします」くらい言えなかったのか? (お酒抜き)

なので、少し高くついた気もしますが、普通に豪華なカレーだったので良かったです

幸地インターの工事

トンネルと橋はできてるっぽい。まだ、かかりそうだな

これだと、高速バス停は移動しないかも知れない(といいな)

坂道

バスの時間があわないと、1/3しかバスに乗れない。そこで

　　あえて、坂道を選択する

これでしょ

This page was intentionally left blank

週末は、おとなしく寝てる予定です

うちのひょうたん継ぎ

良く見ると継目が見えます

ガジュマルが倒れるとはね

あの台風はすごかった

PostgreSQL version 16

KEA-DHCP に久しぶりに触ったんですが、Rest API が動かない。まさかと思って、Docker image あげたら、keactrl がちゃんとあってそれ

なんですが、DB構造が合ってなくて、schema version が13でなくて18だとかいう

まぁ、それはKEA-DHCPの問題でDB初期化すれば良いだけだが

　　PostgreSQLのversionは?

どうも今、使ってるのは13で最新は16らしい。これ上げるとなると

　　Akatsuki / PowerDNS / KEA-DHCP / FreeRadius / Gitlab

あたりが関係する。これ、どうするの? まぁ、サーバ切り替えの時に一気にやるのはありだが、

そもそも、コンテナimageを PosgreSQL 16 で統一できるのか?

それとも、みんな 13 で知らんぷり?

咳

なんか長引いてて... 続く人は続くらしい。別に咳止めでもいいんだが、割と薬は飲まない方針な人なので

酒飲みにいかないのでお金かからないし、体重は減るしでいいことばかりです

熱はないんだが社会の迷惑ではあるな

雨男

まぁ、別に沖縄に戻ってきて、雨続き

別に僕のせいではないですけどね

今日は、琉大は霧がすごかった...

最近のWordle

Streak 192 です。前回は 117 ぐらいで落ちました

最初の 4 word 固定派。よほど大量にでない限りは、そのまま入れるかな

ここでそれを晒してもいいけど、まぁ、普通なはずです

NY Times は購読しているので解析がついてる。安全寄りにやってるので、そんなもん

アプリ側が word として認識するのと、解析が word と認識するのとのずれがある

つまり、解析があと 1 word とか言っても、別な word が accept されて外れる

いや、それもひどいよね。

最近ので苦戦したのは

　psalm repel verge ember

あたりかな。j k q は割と引っかからなくなった。

かけ算の順序 (右かけ算と左かけ算編)

かけ算原理主義は

　かけ算は対称だと言う教義(根拠は素朴実在論=神)
　それに反するものは禁止、あるいは暴力で阻止
　包含除/累加(一つ分xいくつ分)や式の意味の禁止

という社会問題で数学的なものじゃない

(一つ分)x(いくつ分)でかけ算を理解するのは、足し算の繰り返しでの計算や操作を中心とした構成数学的な手法で手を動かして理解できる

この定義では、引数の片方で問題を分割する。つまり、片方を固定して、他方を増加させて計算する

これは、それでそのままある。これで問題解けるし、実数や複素数までの拡張も問題ない。かけ算の非対称性は線形代数や量子力学に自然に対応する

否定する必要はないし、それは無理

(ひとつ分)x(いくつ分)の定義と両立しない原理主義者の間違いのパターンがある

0)値が同じなら式も同じ
1)定義はない
2)アレイ図を数える
3) (いくつ分)x (ひとつ分)の両方が成立
4) (いくつ分)x (ひとつ分)との不定状態

この中でまともなのは 3 だけで、その他はかけ算の計算手続きを放棄してしまっている

つまり対称なかけ算の定義でまともなのは(一つ分)x(いくつ分)と(いくつ分)x(一つ分)、
つまり右かけ算と左かけ算を両方用意する方法だけ。半環とか実閉体とかも対称性を要求すなら、これと同じになる

右かけ算と左かけ算には異なる意味がある。かけ算の意味とは、かけ算の状況をさす。明示的なまとまり、単位、
定義域の制約などである。

実際、PV、nRT、vt、ne、お皿と飴
対称でないかけ算たくさんあって
トランプ配りみたいな言葉まである

PV=nRT で、
　Pを固定してVを増やすかけ算
　Vを固定してPを増やすかけ算
の意味は異なる。操作が違う。これが左右のかけ算になる

原理主義者の対称性の根拠はアレイ図によるかけ算の理解だが、 アレイ図は実は向きがある
　→→→
　→→→
0があるから数える向きがある。これだと回転しても同じ形にはならない

　皿の上の飴を数える局所的な計数
　皿を越える緩い計数

の二つの向き(足し算)がある。トランプ配りは計数の強度が逆なので変に感じる

向きを無視する、あるいは両方あると思うと原理主義者的になる

なので別に(一つ分)x(いくつ分)と対称なかけ算は両立する。対称な状況/かけ算の意味の時、あるいは
単位のサンドイッチに変形したり、値だけに注目すると対称なかけ算に変換できる

でも、それは元の式に意味や順序がなくなることとは違う。式の意味は、大雑把に単位と思って良い

それでも「値は一緒なんだから同じでしょ」と言ってくる人がいる。それは式の意味とか状況が対称だと決めつけてるだけ

意味を考えると左右のかけ算が区別できる違うっていう認識はある。それらの意味を外して値として計算すれば対称

そこで「だって」とか「でも」が出てくる余地がよくわからん

お休み中

去年は位相空間論やってたんだよな

Red black tree の残りを片付けようと思ってるんですが、やる気が微妙

なんか、Agdaの式が頭に入ってこない

酒量多めなので、少し控える予定

Queen のIMAX映画

行ってきました。音良いです。Gameの頃のかなぁ。We will rock you を何回も

4人だからな。シンプルといえばそう。テープレコーダー使ったのも控えめ

Under Pressure が印象に残ったかな

ボヘミアンラプソディーのオペラパートはテープ。いや、それでいいし

むしろ、ハイテクで重厚なのが聞きたい気もする。アダムランバートのどうなんだろ!

でも、Talking Headsの方が良く練られてるかな。人数多いし。物語感がある

フレさんが観れるだけで素晴らしい。どんどん脱いでくし

池袋のあれシリーズ3

西武線と京急

なんで、この二つなんだろ

やる気の問題

1,2月の風邪の影響かな

まぁ、卒論修論終わった学生と一緒に遊んでます

なんか、やるか? 暇そうじゃん

大学の会議への文句

いや、だいたい出てないんですけどね。お互いうれしくないし… まぁ、シス管関係だから仕方ないか

＊　オンラインじゃない

これだけでだめすぎ。なんで、わらわら集まってるんだよ。集まるのは飲みにいく時と遊びにいく時でいいです

＊　資料が紙

ちょっと。文書管理いろいろあるでしょ。Teams は最低だが、Google drive よりはましか

そもそも先に共有してよ。そこに書いて終わりでしょ

＊　議事録がない

おいおい。次が困るでしょ。なんで、ワークフローがないんだよ。そもそも出席者記録してないじゃん

いや、シス管ミーティングなら、こんなの許さないわけですよ。なにせ

　　シス管のメンバーは来年度はいないのが普通

なんだから。「これは、そこのSctapboxに書いてある」でだいたいすむ。毎年、毎年、何もしらない学生がゼロから始める

だから、

＊　僕を呼ぶとうるさいだけっていったでしょ

池袋のあれシリーズ 2

エレベーターの中の非常箱

中身がなんなのか気になる

ひたすら

うちで寝てます。熱も咳もおさまったが、まぁ、今日はおとしなく

ひたすら、猫のけつをたたいてます

まぁ、もててると言えなくもない

38度

神戸東京で風邪拾ってきたらしく

咳は収まってきたが熱がな

もっとも、38度くらいだと動けるのがなぁ

また週末、風邪でおとなしくしてるパターンです

先月もこのパターンだった

東京で一緒だった人は、そういう意味でごめんなさい

池袋のあれシリーズ

シリーズなの?

なんで、いまさら、ガラケーってあたりに人のセンスがでるかな

Stop making sense 4K

飛行機の時間まで余裕があったので、シネマサンシャインで観てきました

やっぱり、IMAXの音だよね。

去年、アメリカンユートピアのあとで、アマプラで見直したんだけど「まぁ仕方ないかな」

でも、その辺がばっちり。あのNYパンクのイケイケなリズムだな

また、デビットバーンが若いから走りまくってるんだよね。

ただ、字幕は微妙だった

でも、もう終わりか。観れただけよし

プレファボーレで宴会

いつもの研究室OBとなんですが、前回と同じミリオンにしようとしたらお休み

なので、要町の街のイタリアンのプレファボーレにしました

シェフ一人なので「おまかせで」

こういう普通なのいいかな。その後は、いつもの行きつけの店へ

さて、もう明日は沖縄

映画でも見てから帰るか

Theory and Theory Luxe

東武デパートを散策してたら、いきなり Theory とな!

いや、女性向けブランドですよね。なんか、30年くらいの歴史のある NY ブランドらしい

Thoery Luxe ってのは、おば..日本人向けの独自ブランドだそうです

メンズもあるのか。シンプルだけど、少しとがってて、面白い

まぁ、ブランドの名前は、なんでもありだからな

https://www.theory.co.jp/theoryluxe/

イリイチ温泉2日目

酒飲ながら文系本の議論は、なかなかハード。もっとも、朝から飲んだりはしないんですけどね

水とH₂Oは、人口湖を作るので立ち退きとかあたりの水と社会の関係の話

Just Cultureは、ミスを罰すると、情報が隠れて accoutablity が取れなくなる話

Shadow work は金銭が絡まないから、その辺の問題を避けられてるみたいな視点も

Small is beautiful は、懐かしい話。でも、あの頃は女性の間の流行みたいにとらえていたかも

　お金という単一な尺度で最適化すると、全体としての幸福度やバランスは低下する

こう書くといつものあれだが。スケールするのが正義ってわけでもないってことかな

High Tech Heroin はタイトルだけ

なんか、六甲保養荘は3月で閉まってしまうらしく、近所の大阪のあばさんが200円でお風呂に入れてたのにとがっかりしてました

この手のものを維持できない、建て直しできないってのは残念だな

イリイチ勉強会

別名イリイチ温泉ですが、自分の担当の Shadow Work は2時間は無理だったが、まぁ、終わりました

26pageで2時間はな

でも、Tools for convivality を含めてぶっとばっしてて楽しかったです

イリイチの問題意識は70年代では先行してたけど、今は2020年代だからな

システム管理は、Shadow work だよね? ってな話をしてきました

明日もお昼まであるので、がんばります

酒とつまみと、温泉。すばらしいです

大阪

明日は六甲です

イリイチと辞書

Shadow work と Tools for Conviviality なんとか読了

やっぱり、文系論文だからな。辞書引くのが結構あって。昔は macOS の service menu にあったんですが

　出たり出なかったりする

おいおい。AppleScriptもうっかり書いたんですが、Shortcut という手があるらしい。Automaton もあるはず。

この似たり寄ったりのがあるのどうにかならんのか。でも、Shortcut で Dictionary.app を開けるのを Menu bar に出るようにしました

keyboard shortcut もあるはずのに動かない。わけわからん。

Kindle に入れても良いんだが、英語設定なので日本語訳がでない。KindleはUIだめだからなぁ

読んでるのは Zotero ですが、Kindle よりはましかなくらいです。Emotinal な単語とか貧乏の同義語をたくさん見たかも

肝心のイリイチですが、一通り読んだんだが、まぁ、はっきりしたイメージができるわけでもなく

でも、ちゃんと読めているとも限らないので、読み会でなんか発見があるかも知れないです

学生のプレゼン

ちゃんと指導してるつもりなんですけどね

　まず、MindMap、いきなりスライド書かない

なのだが、MarkdownなMindMap使うやつがいてな...

　そして、プレゼンをいきなり書き始める

そうじゃなくて、MindMap は、やったこと、目的、関連研究、ぜんぶ網羅的に書くんだよ

なので、うちでは Markdownな MindMap は禁止

　論文とプレゼンは別もの。論文の目次でプレゼンするな。
　研究目的なんてスライドタイトルにするな、もったいないだろ

いや、単なる手抜きなんだよな。プレゼンが「人に見せるエンターテインメント」だってのがわかってない

そこで、MindMapの一つの枝にプレゼンってのを作って

　そこに物語りを作る

多少嘘が入っても「ハッピーエンド」に作るんだよ。いろいろ苦労しましたが、研究目的を達成しましたってさ

なんだが、学生ってのは

　研究目的を忘れて、ツール作りに没頭する
　そこで自分がおもしろいと思うものを作る

まぁ、いいんだけど。それを楽しんでもらえれば。そこで、僕の登場で…

　やったことと研究目的のつじつまを合わせる

まぁ、ハッピーエンドは大切だからな.…

Illich and Tokyo

イリイチの読み会/宴会が六甲であるので行ってきます。2/17

2/18-21 は東京の予定。東工大には寄るんじゃないかな

というわけで、Shadow work と Tools for Conviviality を読んでるんですが

　　集中力がなぁ 10page続けて読めん...

70年代の文系論文だからな。どちらかというと教育寄り。数式ないし

でも、共感するところは多い。Teal 組織とも少しつながる感じ

一応、六甲では Shadow work を担当します

猫のお注射

こたが、お爺ちゃんなので「糖尿病」。猫には割と良くあるパターンらしい

カリもかかったんだが、なんと、猫の糖尿病はなおることもあるので、なおってました

で、インスリン注射ってわけね。

　　アルコールで首根っこを拭いて、注射器をぶっさして、押し込んで終わり

そこには痛覚はないらしく、とくに文句もなく。なんか

　　よたよたしてたのが改善

良かったね。大半は寝てるだけですが

はちれん復活

長く閉めてて、あきらめてたんですが

　　オバーのワンオペで復活

佐真下公園横です。梅つけ。まともなラーメン素晴らしい

民謡スナック

割と沖縄民謡歌う方なので、スナックのママが行こうというので、中大謝名の花に

なんかそこの娘さんが民謡練習しているらしく。これも良くあるパターンだな

なんか40年前の民謡番組とか見れたな。知名定男とか激若

娘さんは安里屋ユンタからだったけど、ナークニと恋ぬ花、歌ってもらって、で、こっちにお鉢が...

まぁ、仕方ないよな。情の唄と加那ヨーにしました。もっといろいろ歌っても良かったが、この辺で

カラオケと違うし、やっぱり、歌詞覚えないとだめだよな

まぁ、そこまではやらないんだけど。玉城史郎先生とかやってたな

もしかすると、また呼び出されるかもしれん

大平の Vintage

老舗のBarですけどね。いや、だって

　　看板なくなってる

から閉店かと思ったら、元気に営業中らしい。下のビアンコも

ってのを、公栄の新しいママさんから聞きました

そこで、Bar やるの? がんばれ〜 カラオケあり

卒研発表

今年も2並列。二日にして全部聞けるようにしてって言ってるんですが、通らないですね
メインイベントだとは思うんだけどな

OSやプログラミング言語系は減ってて、機械学習な認識系が多い

Zoom 入れてくれないの? プロジェクタとか、もはや時代遅れで「見えないんですか」

Zoom だと手元で見えるし画質もよいのに

まぁ、自分も Black on white にしてるのはプロジェクタで見やすいから見たいな理由があったんですけどね

うちは、いつものMarkdown からの Web slideなので、修正は容易。でも夜中までかかっていたようです

普天間 禮二

お寿司ですね。すだちなづけですか

いや、ぜんぜん気がつかなくって。かなに聞いたらいったことあると

江戸前そんなに嫌いじゃない。最近の寿司って味ついていること多いしな

ネタはいいんだけど、やっぱりづけは人を選ぶかも

自分的には微妙かな... 沖縄の気候にあってるとは言えるかも

なれてないだけかもね

卒業アルバムの写真

を撮る日でした

いや、そんなの撮った記憶ほとんどなくて。でも、謝恩会がコロナでなくなって

　　実は写真があんまりない

ってことに気がついたのかも。自分的も、若い頃にもっと写真を撮っておけばおけば良かったとは思う

父のRetinaの蛇腹結構良かったので、白黒フィルムだけで現像だけとかすれば安かったはずなんだよな

なので、自分では意図的に学生の写真を撮って、Google Photosの共有アルバムに上げてたりします

オープンキャンパスとかも撮ってるので「オープンキャンパスに写っている高校生」で自分を発見する人も

実際、卒業アルバムの需要は増えてるのかもな

でも、ほぼ元に戻りつつあることも確かで、少し残念な気もする

　　オンラインですませてた、あの快適な頃が懐かしくない?

卒研追い込み中

まあ、ここまで来たら、やったこと書いて発表するだけだけだから

浦添パブリックゴルフクラブの倒福

歩いていけるところにあるゴルフ場です。ゴルフはしないんだけどさ

そのクラブハウスのレストラン

いや、この黄色い懐かしい麺のラーメン。台湾麺とあるけど、胡椒辛いだけな気も。でも

　　普通にうまい

この寂れたクラブハウスのレストランだと、母の通ってたゴルフクラブを思い出すな

行きは電車なんですが、帰れないのでタクシーで帰ってきちゃう。まぁ、それも

　　今となっては笑い話

です

podman and singularity

githubは、packageの配布もできるんだけど、Dockerですか? homebrew は容易してあるんですけどね

singularity の sif image から Docker image を podman で作るという方法を試してみる

　singularity build --sandbox cbcdsand/ cbclang.sif

で書き出して、 Dockerfile

　　FROM scratch
　　COPY cbcdsand/ /

それを使って

　podman build -t cbclang .

なるほど。ところがぜんぜん終わらない

User mode podman が遅いのはそうなんだが、それにしても。で、ChatGPTと話しながら..

　podman info

で、~/.local/share/containers/storage を使っているらしく。そこ Ceph だから。

それは無理。いったい何重に file system 重ねてるんだよ。で、

　　[storage]
　　driver = "overlay"
　　graphroot = "/mnt/hogehoge"

で、切り替える。これで、まぁ、10分くらい、で、

　 podman run -it -v $HOME:/root　cbclang /bin/zsh

一応、動いた。image size は15GB。llvm x 2 なので、もう少しは削れるとは思うけど...

あぁ、やっぱり、singularity に比べるといろいろだめね。User mode で使うなら singularity の方が合理的ね

なので、github packageも .sif をあげられるようになると良いかも

CbC package

debian packageは fpm で作ればよいってのは2021くらいにやってたんですが、なんかうまくいかない

debs
├── Release
├── dists
│   ├── stable
│   │   └── main
│   │       └── binary-amd64
│   │           └── Packages
└── pool
    └── main
        └── c
            └── cbclang
                ├── cbclang_13.0.1_amd64.deb
                └── cbclang_18.0.0-1_amd64.deb

と展開する必要があり、md5/sha1/sha256と計算する。Packagesの署名しろとか言われたが、その
鍵どこに登録するわけ? とりあえずはいらんか

で結局、Packages/Release を生成する Perl script を書くことに。いや、gitlab ci でやってよ...

明日は podman image のことを書くかも

fpm -s dir -t deb -C /usr/local/cbc_llvm  --prefix /usr/local/cbc_llvm --name cbclang 
    --version 18.0.0 --iteration 1 --description "Continuation based C on LLVM" 

dpkg-scanpackages  .

原理主義者からみた掛順問題 -- かけ算に順序はない

もちろん、かけ算は

　(一つ分)x(いくつ分)
　なにを何回足すか

で定義されるのだが、ここで累加はあまり強調されない。ここで筆算を導入するには定義から自明な右分配則で

　17x21 = 17x(20+1) = 17x20 + 17x1

と足し算で計算できる。筆算の本質はこれである

しかし教科書ではアレイ図を使った比較的複雑な展開を行う。ここで、交換則もアレイ図で導入する
これは、かけ算の筆算を交換則を同時に証明する形で計算したいからだと思われる(インド式)

そこで

　○○○○
　○○○○
　○○○○
　アレイ図を数えることがかけ算

という直観が出てくる。これは間違いで教科書の定義とは異なる。しかし、学生あるいは親に発見されてしまう
すると、縦横を回転して形が同じなので「かけ算に順序はない」「どっちでもいい」ということになる

定義では「アレイ図を(一つ分)x(いくつ分)に分解して、足し算の繰り返しで計算する」あるいは
「二桁のかけ算をインド式でアレイ図を使って計算する」なのだが、これが落とされてしまう

これで面倒な筆算は「その時だけ」で忘れてよくなる。これが「かけ算に順序はない」かけ算原理主義者の本質だと思われる

アレイ図を数えるのは集合の直積濃度に相当するし、計算する必要がなければ合理的にも思える

# なにがよろしくないのか

アレイの分割を忘れるとかけ算の計算ができなくなる。これは致命的。筆算を思い出す指針は累加なので、累加を強調する必要がある

かけ算の本質は(一つ分)x(いくつ分)という分割であり、これは面積以外の非対称あるいは非可換なかけ算にも当てはまる

これらの非対称性は「5個ずつ飴が乗ってる皿3枚」とかでもある。実際これを聞いているのが掛順問題である。これを

　「かけ算に順序はない」「どっちでもいい」

とすると、直観が「アレイ図を数える」に落ちてしまう

実際、集合P,Qの直積 P⊗QとQ⊗Pは異なる集合であり可換ではない。行列演算P x Q は非可換だが、その行列式あるいは跡は可換に振る舞う

(一つ分)x(いくつ分)ならば、いくつ分を追加することで自明な線形性(右分配則)がある。また

　単位量 x 数量 = 単位量

という単位のサンドイッチが自然に導入される。また、かけ算の整数や分数への拡張も容易

これらの有用な直観が「アレイ図を数える」で失われてしまう。これが問題で、実際に、かけ算の定義を捨てて

　かけ算とは抽象的な対称な演算

に落ちている人が実際にいる。これを本来の「かけ算とは線形性で世の中を分析する考え方」に戻す必要がある

# 本質は掛順ではなく、包含除で分解する方向/線形性

原理主義者のかけ算の定義は「アレイ図を数える」で攻撃はその理解を否定する掛順問題、累加、単位のサンドイッチに向かう

しかし、重要なのは、その個々の問題ではなく

　　かけ算をかけ算としている状況での「いくつ分」(線形性を持つパラメーター)を見つけること

であり、そのパラメータとして、まとまりの個数、繰り返しの回数や時間がよく使われることを強調する

昨日は爆睡

だいぶ元気になったので、加藤食堂でご機嫌にワイン飲んでたら

　　帰ってから、そのまま爆睡

まぁ、blogのネタはないしな 飛ばしても良いだろう

卒論修論がんばれ〜

英語の授業

持ち回りの英語でやる授業。まぁ、だいぶさびついててな

Zoom でやれよと思わなくもないですが、対面

今季は対面はこれだけ。咳は、まぁ、なんとかなった

あの教室、プロジェクタがとらぶるんだが、今回はばっちり。ただし

　　MBP16のHDMI直結は動かない

なんだそれ。アダプタ経由ならいく。謎すぎる。学生がもってるのを一つもらいました

琉大 GameJam

発表見てきました。え〜、一組だけ? しかも、うちの研究室で見る面子か

いや、そういうことなんだよね。結局、会って引っ張らないと来ないもん

それでも、今年も成立したので良しというところか。会社の人も来てくれて

　もしかして業務?
　いや、僕は趣味、でも、こっちは業務にしてもいいと言ってます

いや、上司太っ腹! IT系に限らず

　勉強や実習、人脈作りは必要だし、それは業務時間内にはやりづらい

それは「業務時間内しか絶対やらない」も違うし「自宅で毎日1時間」とかも違うし...

それぞれだしなぁ。少しの時間あるいは、なんかのイベント、それにちゃんとお金がでる

そんな感じがいいかも

ゲーム自体は、おばあちゃんが昇天するみたいなゲーム。Unity で UniTask 使ってますとか。

3Dだけど、動きは2D。見栄えするし、作り安い。プレイしやすいもある。正しい選択で、学生主体な感じで
完成に持っていってる。さすがですね。

僕はゲームには「オープニングとエンディングは作れ」と言ってるので、それはちゃんとクリアしてました

　　偉い!

(いや、あのUnity背景は消そうよ... おばあちゃんは$5で買ったらしい。自分的には炸裂するようなプロジェクトが好き)

Text Replacement 続き

いや、まぁ、Twitter(自称𝕏) でも MathJax くらい使わせろと思うんですが

この前のでもだいたい動くんだが「時間がたつと動かなくなる」謎すぎる。iCoundで同期しているわけだが

　iPhone 側ではちゃんと動くが、macOS側ではだめ

なんだそれ。\^2 で ² がでるようにしてるんだが、⁰ はでるが ² はだめ。DB側は正常

なので、macOS側で on memory な DB を壊してるのではないかと。

手動で入れても壊れるし

% sqlite3 ~/Library/KeyboardServices/TextReplacements.db
SQLite version 3.39.5 2022-10-14 20:58:05
sqlite> .sch
CREATE TABLE ZTEXTREPLACEMENTENTRY ( Z_PK INTEGER PRIMARY KEY, Z_ENT INTEGER, Z_OPT INTEGER, ZNEEDSSAVETOCLOUD INTEGER, ZWASDELETED INTEGER, ZTIMESTAMP TIMESTAMP, ZPHRASE VARCHAR, ZSHORTCUT VARCHAR, ZUNIQUENAME VARCHAR, ZREMOTERECORDINFO BLOB );
CREATE TABLE ZTRCLOUDKITSYNCSTATE ( Z_PK INTEGER PRIMARY KEY, Z_ENT INTEGER, Z_OPT INTEGER, ZDIDPULLONCE INTEGER, ZFETCHCHANGETOKEN BLOB );
CREATE TABLE Z_PRIMARYKEY (Z_ENT INTEGER PRIMARY KEY, Z_NAME VARCHAR, Z_SUPER INTEGER, Z_MAX INTEGER);
CREATE TABLE Z_METADATA (Z_VERSION INTEGER PRIMARY KEY, Z_UUID VARCHAR(255), Z_PLIST BLOB);
CREATE TABLE Z_MODELCACHE (Z_CONTENT BLOB);
sqlite>

いや、ZTRCLOUDKITSYNCSTATE こういうのやめようよ...

かけ算の順序のまとめ

Twitter での議論も尽きたみたいなので、まとめ。今までにも何回か書いたけど

# まず、かけ算の定義を確認する

初めて習うなら、もちろん、大きくなったなら、数学的にも日常言語的にも言えるべき

　1) (一つ分) x (いくつ分)

包含除と呼ばれる。数えられるものを分割し、分割の一つ分の数と分割の数でかけ算になると理解する。
お皿の上の飴の数とお皿の数。

　2) 何を何回足す

累加と呼ばれる。足される数(かけられる数)とその回数。最初はゼロ。1)を実際に計算する時に使う
この二つは表裏で、分割する方と回数の方向性がある

# かけ算の性質

分割側と回数側で自明に右分配則が成立する ( 3 x (2 + 5) = 3 x 2 + 3 x 5)

交換則が成立する (3 x 5 = 5 x 3)

かけられる数の単位は、包含除や累加では保存する

　5cm x 4 = 20cm

単位のサンドイッチと呼ばれる

# 筆算の方法

かけ算九九なら、実際におはじきなどを並べて数える(アレイ図を数える)ことが許されるが、
二桁以上は工夫がいる。45 x 24 では、23を 20 + 3 と考えて、

　45 を20回足す、さらに3回足す
　45 x 20 = 900
　900 + (45 x 3) = 900 + 135 = 1035

アレイ図だと交換則と分配則を使うので複雑。上の方法は累加だと割と当たり前だが分配則は使ってる

これらの定義と計算方法は対称性はないが、かけ算に対して常に正しい。また、分割側回数側を自然数にとると
整数、小数、分数、実数、複素数、あるいは拡大体やベクトルや行列に対しても成立する。

# かけ算は値だけではない -- かけ算の定義の非対称性の原因と数学との関係

かけ算は現実世界の「かけ算的な性質」であり、それがなぜかけ算なのかは、包含除と累加の定義から
決まる。そこには対称性はないので、実際に非対称な演算が含まれる

　　5m/s x 3s = 15m
　　3m/s x 5s = 15m

は経過する時間が異なる現象であり、同じなのは値だけ。これは副作用や誤差あるいは揺らぎなどに影響が出る。
これは突き詰めれば、時間経過は量子力学的な現象であり非可換な行列演算だからとも言える。

もともと非可換な現象(加群とか)の一種の射影としてスカラーで可換なかけ算が見えている。物理法則

　　PV=nRT

には、Vやnは分割や回数として現れている。これは「自然な方向」という言い方もできる。分割や累加は問題の
自然な方向(線形性)を示してる。

# 累加を通したかけ算の拡張

累加の定義を左辺に拡張するのは容易で、足し算さえ定義できれば容易にかけ算を拡張することができる

右辺を拡張するには

　　-3 x -5 = (-3 x 5) x -1
　　3 x 0.3 = (3 x 3) x 0.1
　　3 x 3i = (3 x 3) x i

のように結合則を使うと良い。x -1 , x 0.1 , x i などを定義するが、交換則を満たすように決める

非可換な行列などでも同様に拡張できる

# 可換則を任意に使っても、かけ算の順序のつじつまはあう

(3x5)x6 = 3x(5x6) でも自明ではないが累加での解釈が可能になっている

同様に式で交換則を使ったあとでも、もとの式のかけ算の意味がなくなるわけではない。
単位と一緒に交換するという考え方もありえる

また、計算する時に交換則が禁止されるわけでもない。順序があるのは式や考え方であって、
計算結果には交換則が成立する


# かけ算に順序はないという原理主義者の主張はなぜだめか

(一つ分) x (いくつ分)を問ういわゆる掛順の問題で、3つのお皿に4つずつの飴なら、4x3が
が答えだが、それに

　　どっちでもいい

と答える。その根拠はかけ算はもともと順序がないから。

これが問題を引き起こすのは、かけ算の定義や性質には対称性がないから

　　かけ算の答え(値)は順序に依存しない

なら、問題ないのだが、定義や性質に「順序はない」を要求し始めると混乱が始まってしまう。

# かけ算に順序はないという原理主義者の混乱

原理主義者には、さまざまな症状がある。

　1) かけ算の定義を否定する (計算できないが対称な演算とする。九九は良いとかの変種がある
　2) 式と値を区別しない (2x3 と 3x2 を同じと言い張る)
　3) 単位のサンドイッチを忌避する
　4) 累加の定義は認めるが「右かけ算と左かけ算の選択は保留する」という(自明な分配則を認めない

「かけ算はアレイ図を書いて数えること」あるいは「直積の濃度」だということが一つの根拠になる
一階述語論理では、かけ算の意味は Well defined な自然数の三重直積なので、それっぽい

あるいは、関数外延性で、右かけ算と左かけ算は同じと言い張る

右かけ算と左かけ算を同時に定義するとかの一見対称な定義も可能なのだが、両方同時に家庭する必要が
あり、両方の順序があることになる。否定するには　

　 右かけ算∨左かけ算

という方法があったりする。これだと右分配則が自明な直観にならない

これらが無害なら問題ないのだが、例えば

　5) かけ算は単位と一緒なら、交換しても同じ

なら、累加を認めていれば割と害はない。ところが、定義を否定するとか、計算を拒否する、あるいは
単位のサンドイッチを含む公式を一般的に忌避する人たちが実際に存在する

　　5m/s x 3s = 15m

を

　　5m x 3 = 15m

の単位のサンドイッチで理解することが許されないので、よく分からない複雑な解き方(はじきとか)を使う。
「はじき」なら、いきなり 5 x 3 を出せるので、かけ算の対称性は維持される

このように「かけ算に順序はない」を病的に避けることがはっきり害になっている。定義が怪しいので
不安があるので、攻撃的になることもある

# かけ算に順序はないという原理主義者の反ワクチン的な振る舞い

　教科書や先生は間違ってる ≈ 医者の言うことは間違ってる
　定義や証明を神への冒涜 ≈ ワクチンの有効性のエビデンスへの反発
　ペアノは危険 ≈ m-RNAワクチンは危険
　かけ算の順序を使うと高度な数学がわからなくなる ≈ ワクチンを打つと癌になる
　子供にこの問題でバツをつけるのは可哀想 ≈ 子供にワクチン打つのは可哀想
　無理な順序のない演算の定義 ≈ 反ワクチンの無理な理論付け
　反順序は反ワクチンと同じで、自分たちが思ってるほど多数派でも主流派でもない

これらは、一種のインテリ批判あるいは、体制批判でもあって原理主義者たちが攻撃的になるのもいつものことである

# かけ算に順序はないという原理主義者への対処

まず、かけ算の定義を明確にする

　1) (一つ分) x (いくつ分)
　2) 何を何回足す

掛順の問題で「自然さ」を強調しても良い。数を増やした時に単純な足し算で増える方(線形性が自明な方)を自然だという

これで折伏する必要はない。かけ算の定義がはっきりすれば、原理主義者の問題は、彼らの禁則事項の問題になり、
原理主義者たちが無意味に難しい方法あるいは、回答拒否するのは彼らの勝手ではある。

原理主義者の意固地な思考が、他の人に伝搬しなければ良い。なので、

　掛順の問題にどっちでもいいと言わない

かけ算の定義と分割累加の方向の関係を説明するのがよいと思われる

細かい問題シリーズ

なんか、gpgsm の --disable-crl-checks の flag が、また落ちていた。環境設定の hg のミスか

macOSの Text Replace の sqlite3 の ZTIMESTAMP は、日付文字列ではなくて、mac time (unix time - 978307200)の十進文字列なことを発見

なので、sqlite3のCURRENT_TIMESTAMPは使ってはいけないらしい

Red Black Tree のAgdaでの証明付きの記述は、なんか軌道に乗った感じ。もっと早くやれってことだが、まぁ、いつものことか

少し元気になってるってことかも

まだ咳と熱が残ってるな。月曜日の授業が最後なんだが微妙な感じ...


https://github.com/shinji-kono/macos-text-replacement

お熱が

昨日、「だいぶ良くなった」™ので、コンビニに買い物に出たら、激寒かったのもあってか

戻ってきて、お昼ご飯にしたら、一気に熱が... 39°はやめて。そのまま夜までだったので、

　　こんなこともあろうかと、コンビニで買いためたゼリー食品で

でも、割とぐっすり眠れた。起きたら37°台だった。なんだったんだろあれは

それまであんまり熱でなかったんだよな。なんか踏み抜いたのかも

まぁ、もうしばらくおとしなくしてるかってところです

Capture app がない macOS Sonoma

Dockに 入れて、そこから Screenshot 呼び出していたんですけどね。

⌘ + Shift + 5

とかのくそを覚えたくないんですが。これを押すだけの Applescript 書くか。

Image Capture.app できないというのが謎すぎる

つうか、お前はどうしてそこにいるんだよ。これから座ろうとしてるのに

Global Game Jam(GGJ)開催のお知らせ

毎年、学生がやってくれるので素晴らしい

2023年の1/26 ~ 28

対面とオンラインのハイブリット

卒論修論と重なってる毎度のスケジュールですみませんが、ま、どうしようもない

別な日付てやってることもあるみたい

https://igda-ryukyus.doorkeeper.jp/events/167792

週末の風邪

いつものパターンだが、授業とか卒論はZoomだから

木曜からおかくて、金土と咳がつらかったが、おさまったかな

明日も午前中はお休み。っていつものことか

UEFI解決篇

kernel load して

Status = uefi_call_wrapper(SystemTable->BootServices->ExitBootServices, 2, ImageHandle, MemoryMap.MapKey);

して、kernel entry にいけばいいだけなんだが、なんか Exception はく。最初は EL0 とか EL1 なのかと思ってたんですが、


- Status = uefi_call_wrapper(BS->AllocatePages, 4, AllocateAddress, EfiLoaderData, *FilePageSize, FileAddr);
+ Status = uefi_call_wrapper(BS->AllocatePages, 4, AllocateAddress, EfiBootServicesCode, *FilePageSize, FileAddr);

の問題だった。

なんか、ldd で COFF吐けば、ImageLoad でいけるとかあるんですけど、そうなんですか?

最強食堂のカツカレー

いや、なんつうか、この

　　福神漬けとソースが似合うカレー

がいいじゃないですか。量的には、無理で

　　最初に「半分パックに詰めて」持ち帰り

が良いかも

UEFI と格闘中

いや、学生にいろいろやってもらってるんですが、ぜんぜん進まず。

しかたないなで出動したんですが、まぁ、いろいろひどいよな。なんで大域変数多用するかな。

EDK2 と GNU-efi でCのAPIが異なるってのもなんとかならんの

結局、efi で loader を書くはめになってるんだけど、それおかしいよね...

MBA15 vs MBP16

まぁ、だいたい、15上で作業できるようになって、確かに腹の上に乗ってるときは軽い

カバンはあんまり差を感じない

なんですが、

　　またイヤホンとUSB Cが逆なの?

何でアドホックに変えるかなぁ。ただ、

　　ACアダプタに USB-C が二本ささる

のはよいです

重い計算するときはサーバ使えばいいしな

東工大でのミーティング

1/9の話なので、ちょっと古い

なんか縁あって、久しぶりに東工大の人文関係の先生と。技術史の河西先生ですね

自分がいた頃は道家先生だったりするわけですが、東工大は実は人文系充実しているのも伝統

戦前の計算機の開発の話とか、ドイツにもそういう話があるとか

　　今残ってる本の記述は基本的に嘘だと考えて対応する

まぁ、歴史はそうだよなぁ。かけ算や直観主義論理の話もしました

いや、話てくれる理系の先生がいないとか言ってましたが、東工大にいるのになに言ってるんですか...

まぁ、日本のアカデミックはたこつぼだからなぁ

今回は一緒に飲みにはいけなかったんですが、また、こんど

2号館、少し綺麗になりました

1号館と色はそろえたのか

15inch MBA

いや、ちょっと 16inch MBP 重いかなと思って...

でも、思ったより差がないかな。軽いことは軽いんですけどね

プロシンでもMBP16は割と見かけました。サブディスプレイ持ち込んでる人も。元気だな

あっと驚くことに、2017なIntel版のMBP15な人も。修理したらしく妙に新品でしたが。

でも、うちの学生で2017 Intel MBP15をお下がりで使ってるのもいるんだよな

なので、Setup 中なんですが、いまいち進まんな。スペックが若干下がるのでモチベがな...

本だけ?

いや、ノートPCは本だからセーフ

といっても、帰りはぜんぜんノートPCは開けなかったんですが

JavaPathFinder on Java 11

やっぱり、モデル検査のいいのがなくて。Go / Rustのが欲しいので書けよって気もするんですけどね

Java9 あたりで動かなくなってて見捨ててたんですが、githubのを見たら、Java 11 な build.gradle が。

Java8/Java21 では動かず。Open JDK Java11 で。Javaには、もう対ていく気ないし

Singularity なんですが、sif 作ると動かない。gradle が ~/.gradle に触ってしまうので、それを
移動する必要がある。あと、

　　gradle build -x test

とすると、なんと、RunJFP.jar を作らない。まぁ、test 待てば良いんだが

apt-get -y update
apt-get -y upgrade
apt-get -y install tzdata
apt-get -y install build-essential vim curl git
apt-get -y install rsync
apt-get -y install pkg-config libgl1-mesa-dev xorg-dev
apt-get -y install mercurial zsh
apt-get -y install locales file
locale-gen ja_JP.UTF-8
locale-gen en_US.UTF-8
DEBIAN_FRONTEND=noninteractive \
apt-get install -y \
wget \
openjdk-11-jre-headless unzip
java -version

mkdir /opt/gradle
cd /opt/gradle
wget -4 https://services.gradle.org/distributions/gradle-8.5-bin.zip
unzip gradle-8.5-bin.zip
export PATH=$PATH:/opt/gradle/gradle-8.5/bin

mkdir /opt/pathfinder
cd /opt
git clone https://github.com/javapathfinder/jpf-core.git
cd jpf-core
export GRADLE_USER_HOME=/opt/jpf-core
gradle build
# update-java-alternatives --set java-1.11.0-openjdk-amd64
# bin/jpf +classpath=build/examples DiningPhil

忘れ物大作戦

一昨日はOBたちとご機嫌に三軒飲んだんですが、なんと二軒目で上着をなくすという技が

コートと鞄はあって、まぁ、いいかで三軒目にいったりするのが酔っ払いの危ないところ

カードとかは止めたんだが、財布もなにもないのに iPhone はあるで、特に問題なく

ホテルを出て飛行機にも乗れました。で、沖縄で飲んでたところで

　　二軒目で見つかりました報告

が。やっぱり、もっと良く探すべきだったか。たぶん、トイレの扉の裏側とかだったんじゃないかな

ついでに、ノートPCの電源も忘れました。それもホテルで発見

悪いけど、沖縄まで送ってくれ。すまん

そんなわけで沖縄

最後の incident を除けば平和で、飲んだくれてた出張でした

修善寺駅RPG

行きは、池袋駅から、JR湘南新宿ラインで、横浜乗り換えでJR踊り子号っていう経路なんですが、
自販機で買うの難しいんだよな。昔はみどりの窓口で、超優秀な駅員さんが発券してくれたもんなんだが...

　　なぜか池袋のホームではミニスカのお嬢さんが踊ってて、向かいのホームから撮影している人が...

そのまま Pasmo で乗って(これが罠)
特急券は横浜のホームで買えたんですが、車掌さんが廻ってきてたので、別にそのまま乗っても良かったらしい

いや、でも、そっちの方が高いとか駅員さんが言ってたような。でも、罠は

　　修善寺駅では Pasmo は使えない

で、ばっちり「紙出しますから、あとでJRの駅でPasmoのリセットと清算」をくらいました。

帰りは、みんな修善寺駅の窓口にならなんでたので「券売機でいいや」と思ったら、

　　特急券は買えない

え、なんだそれ。まぁ、いいやで乗車券だけ買って、改札で「中でも特急券買えますよね」と言ったら
「じゃあ、200円出して」で、特急券(硬券)が手に入って、で、三島で新幹線乗り換えで東京まで。
指定でなくても、赤いランプのところなら座っていいからシステムなのね。

Pasmoのリセットも三島で

昔、熱海で駅弁買った時は少し残念だったんですが、三島のはなんかいろいろ選択肢があって豪華でした。

プロシン2日目

自分とあとシス管の発表二つは午前中に片付いて。システム管理は時代遅れ的なところもあるけど、

プロシンはインターネット老人会的なところがあるので「楽しそう」と思われていたようです。

infratusture as code みたいな話も出てたけど、まぁ、そんな感じ。

自分の発表は「Agdaで書けよ」みたいな話なんだけど、Automaton と NFA の同等性を数行で示せるってので
少し驚いてもらったみたい。あとでいくつか聞かれましたが

それって本当に Automaton なのとか NFA なのとか。いや、普通に関数型プログラミングで書いてあるだけですが

本当に一緒なのって「証明してあるじゃん」で

　　人は証明があっても信じないもんなんだ

ってのが面白かったです。まぁ、高階論理の意外さみたいなのがある。これに慣れた世代が楽しみかも

既にたくさんいるはずだ...

あとは、だいたい風呂入って寝てました。割と政府政治関係の話が多かったからかも

プロシン1日目

今回は学生2人と一緒に。一人はデモみたいなものなので、発表もすぐ終わり

場所は去年と同じラフォーレなんですが、少し微妙。今年はカミソリも歯ブラシも置いてないのか

いや、なぜが持ってきたので問題ないんですけどね

代数的Effect というMonad的な関数型言語での副作用/メタ計算の扱いが出てきたんですが、
そういうの嫌いじゃないんですけど、

なんか、普通に継続で切り出してシステムコール呼んでるだけに見えるんですが

まぁ、あとで調べるか

明日は朝一で発表だ。少し疲れたので宴会からは早めに退散してお休みしてます

というわけで`

しばらく東京です

いきつけのお店を廻るだけで初日には終わり

明日は修善寺なはずです

寒いのに、ミニスカートな女の子えらいな感じの池袋

ってわけで、普天間宮

に ingress にいってきたわけですが、

　　記念撮影している作業着な人たちが

そうか、1/4で仕事始めは、初詣て、あとは宴会なんだろうな

いや、それくらいがちょうど良くない?

もはや機械がいろいろやってくれるから、ひと一人が自分の食べる分を自給で生産するとか無理だから

お医者さんと一緒で、個人が払った分の三倍が営業している人に入るくらいでちょうどいいんだと思う

普天間宮

いや、初詣はしてないです。次に(ingressで)よった時にね。

門前の立ち退きは交番を除いて終わったんだが、工事はまだぜんぜんな感じ

もう少し集合論

Agda に safe というのがあるのを発見して。postulate で仮定したり、Heterogenious Eqaulity や
Functional Extensinality を使わないってやつらしい

関数外延性はかけ算の議論でも出てきて、関数の実装は一つで ≡ で扱えるってのなんですが、

　　確かに良くないかも

その代わり、関数は入力と出力の組が等しいというのを関係として使えばよいわけね

集合も要素が同じなら、集合として同じなんですが、それは、そういう関係なんだよな

順序数なアドレスは、集合としては一つ。それでつじつま合うと。10月ぐらいに思いついて放っておいたんですが

　　年末年始プログラミングにちょうど良いか

で、ZFの公理まではできました。

去年はトポロジーやってたみたいね。その辺も修正はいるけど、できるはず。ただ量多いのがな

いろいろすっきりしてよい。safe 自体が主導原理になる感じ

明けましておめでとうございます

やっぱり、行きつけのお店でカウントダウンしてました

まわりはオジーばかりだったがな。自分もそのひとりか

今年は、仕事探さないとな

まぁ、あせる気はないし、金儲けたいわけでもないけど