昨日は爆睡

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

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

まぁ、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 自体が主導原理になる感じ

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

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

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

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

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