大学で教えるべきこと

OBに聞くようにしてるんですけどね。まぁ、いま自分が必要としていることを答える人が多い。

　　データベースとかコミュニケーション能力とか

それは残念なことかなと思うけど。取締役クラスだと

　　分析力とか論理的思考能力

とか。なるほどとは思うけど。具体的な授業とかカリキュラムにはつながりにくいかな。

いや、別に回答を批判しているわけではなくて、大学が提供するものの難しさとかがわかる感じ。

学生には、

　　大学で学んだものが役に立ったという実感がる

よりは、

　　大学で学んだものは何もないが、そこで学んで得るものがあった

方がうれしいかな。

　　新しいものを学ぶためのメタ知識

みたいなものを教えたいと思ってます。

書類の続き

欲しいのは戸籍謄本なんですが、自分のカードでは「このカードで使えるサービスはありません」で郵送してもらうってことだったですが、

妻のマイナンバーカードでは問題なくコンビニで印刷できた。いや、筆頭は僕なんだけど。

　　なんでやねん

コロナ世代

物理的に大学にきてないので、どうも学生間のつながりが浅いらしく。連携が取れてない感じ。

OSの課題だとむしろ、まわりや先輩に聞いてやって欲しいんだが、それができない。

いや、Discord でやってとはいってるんですけどね。難しいみたいね。

イギリスの鉄道の話

90年頃はBritish Railは、まだまともで、InterCityもきれいだったんですが、
保線と営業を別にしておかしくなって、00年代にはぼろぼろ。

This train has been cancelled を結構くらって超残念だった。

そのあといろいろ修正されたらしいんですが、この一連の tweet のがひどくて、

(1)4PMにロンドン-エンジンバラに乗ったら
(2)スマホに This train has been cancelled
(3)運転手にそれが乗客から伝えられて Preston で止まる
(4)乗り換えの電車は満杯
(5)次の電車は cancel でもう電車はない
(6)約百人の乗客は鉄道会社持ちのタクシーで3時間
(7)道知らないイギリスのタクシーの迷走
(8)着いたけど、タクシーの運ちゃんは無事帰れるのか?!

失われたインフラを取り戻すのは難しいってことね

あるいは公務員が誇りを持って働けることの重要性か...

Preston は西側だが、マンチェスターの近く。せめて、その駅ならねぇ。

https://x.com/JamesNokise/status/1706433356186161479?s=20

ldap-server

何か最近は、ldap server / slave と呼ばず、provider / consumer らしく。

懸案だった、ldap -server を container にするってのを小川が片付けたらしい。えらい。

なんだが、いろいろトラブルが。

1) gitlab に login できない。

なんと、gitlab の ldap 設定がIPv6 address直打ち。あぁ、IPv4つながらないとか、そんなトラブルあったっけ。その時のだな。

まぁ、IPv6も割り振れよって気もしますが。

2) ldaps で接続できない

あぁ、昔からそうなんだよ。なんだけど、

cert がないとかいってる

昔と違って、Wildcard Cert を持ってるから、いれれば良いんじゃない? でアクセスできたんだが、

3) sssd からはだめ

いや、sssd 要らないとも思うんですけどね。実際、入ってるのは 4台のうち1台だけなんだよな。

ところがなぜか sssd が切れない。

sssd が古いのかも。結局、sssd の設定は ldap: のままか。残念な話だ。

いろいろなぞなままだな。

いや、でも ldap server は podmain になったし、ldaps は動いたし。進捗はしてる。えらい。

アナログメーター

なんかいいよね〜

上島珈琲のだったかな

agda の version up はだいたい終わり

一部、激ムズくらいましたが。

　　ライブラリの引数を変更されるとムカつくよね?!

Data.Fin の suc だけじゃなくて、inspect が新しい構文になったんだが、どうも一部の機能が低いまたはバグがあるらしく。

その部分を、case文の中で再証明すれば workaround できるのに気がつくのに少し時間がかかりました。

後は細かい問題だった。postulate / functional-extensinality があると、--safe は付けられない。

まぁ、少し分離したけど、虚しい気もする。module の入力にすれば形式的には逃げられる。

Agda の std-lib 2.0

一応、群論の方はなおせんたんだが、いろいろ判明。

　　--cubical-compatible では、case 文と Termination check に問題がある

なので、case文の方は

　--warning=noUnsupportedIndexedMatch

で警告を消す。Termination check は　cubical-compatible 諦めるしかないっぽい。

まぁ、cubical-compatible のありがたみは特にないわけなんですが。

--safe の方は、ほとんど問題無し。なんなんでしょうね。


問題は、

　　Data.Fin の 関数の zero / suc への展開が全滅

with f x とかやるだけで、

　 Function.Bundles.Inverse.from perm (suc x) != w of type Fin (suc n)

意味不明らしい。

いや、もともと Data.Fin (有限な自然数)怪しくてな。workaroundはできたんですが、大変だった...

finiteSet とかでもとらぶる予感。でも、無理になおさなくてもいいとも思うんですが。まぁ、ちまちまなおすか。

OSの補講と ChatGPT

いや、火曜日から4日間しかやらなかったんですけどね。課題出してもらえればよい。後期の授業は10月からなので、

　　後期の授業のチェック

みたいなところもある。なので、いろいろ修理しているわけですが...

課題の採点もやってるんだけど、

　　ChatGPTなだめなレポートが

いや、別に中身あってれば問題ないわけですよ。ところが、正解にならない。もともとコピペ対策で、

　　gitlabのciの失敗したやつのリンク
　　作成したVM imageの ls -l

とか提出されているので、チェックされてしまうので、そもそもChatGPTでは歯がたたないわけなんだが、

教科書の問題とかも、

　　dead lockの問題なのに snapshot という言葉に引きずられて snapshot について語ってしまう

ChatGPTおしゃべりだからな。問題解けよ! 語るな! いや、それでも、そういうのは少しは点数は出してたんだが、

　　もはや、問題を理解してないなら再提出しかありえない

なので、ChatGTP下だと採点が辛くなるのは仕方ないかなぁ。

教科書の対応する章を全部食わせて、問題解かせると良いんだが、API経由でそんなことすると10万円コースらしい...

gitlab-runner

OSの補講をやってるんですが、gitlab ci の課題が動いてない。まったく、こう次から次へと...

gitlab-runner で ci のテストが動くわけね。vmから、container / podman にしたのか。

　 podman exec -it gitlab-runner /bin/bash

で接続できて、go version も動く。何が不満なんだよ。と思って、.gitlab-ci.yml に full path で書いたら動く。

/usr/local/bin に symlink でいいか。ついでに Rust も設定。こっちは、.gitlab-ci.yml　を

　　variables:
　　　CARGO_HOME: "./cargo"

　　before_script:
　　　- export CARGO_HOME=$CI_PROJECT_DIR/cargo

とすると良いらしい。

singurarity　 も

　%environment
　　 export PATH="/opt/rust/bin:/opt/go/bin:$PATH"
　　 export CARGO_HOME=$HOME/.cargo
　　 export RUSTUP_HOME=/opt/rust

という感じで動きました。Rust 完璧に忘れてるな。

singularity / apptainer と Rust

pyenv / cabal とかもそうなんだけど、rustup が

　　$HOME/.rustup

にいろいろ作る。これが singularity / apptainer container と絶望的に相性が悪い。なぜかというと

　　$HOMEが default でbindされるから

これ、PC (一人一台) な文化なんだよね。それでいいならいいんですが、

　　個々のノートPCの能力が低すぎる (VMや Agdaに足りない)

なので、Server 側に singularity で整備してやろうってわけなんですが、

　　学生一人一人が、$HOME/.rustupに rustc とかを持つのかよ、馬鹿すぎるだろ

ってわけなんですが、一応、

　　export RUSTUP_HOME=/opt/rust
　　export CARGO_HOME=/opt/rust

で切り替えられる。それでも、そこが固定されてしまうので後から module 追加とか困るだろうけど。

まぁ、とりあえず、これでいいかな。メインフレーム/TSSっぽい話。ただ、

　　コンテナ用の package 管理もでるんじゃないかな

とも思います。

1円玉の処理

なんか350枚くらいたまってて... 学生のやるやる詐欺はもういいので、ingressのついでにコンビニに。

最近は銀行で引き取ってくれないのね。有料ってなんだよ。硬貨なんて廃止しろ！

ローソンで、何枚いいですかって聞いたら、200枚。十分十分。学生二人とちまちま格納。

で、次はファミマ。なんか計数器みたいのがある。ざざざざ。あ、拒否された。

　　もう一度やればよい。日本人は絶対やらないけどね。

最近はネパール人が多いかな。ありがとうございます。

蔵前工業会

なんかメール発掘してたら、会費無料とあったので10年ぶりくらいに。

そしたら、なんか学長さんが来てて... まぁ、数人しかいなかったし、首里の普通の居酒屋だったんですけどね。

久しぶりな面子にも会えたので良かったです。

学長は女子枠推進派らしく「理論武装は完璧」みたいなことをいってました。僕も女子枠賛成です。

医科歯科との統合もあって大変らしい。

たまには、行ってみるか〜

Agda の version up

なんか、一日たっても終わらないので、without-k やるかってことなんですが、そもそも、--safe にすると、Decの例題が通らない。

server側とのずれも気になるので「versionあげるか」なんですが、

　　name: standard-library-2.0

ちょっとお〜 なんかいろいろ変わってる。inspect が deprecated?! あれはひどかったからなぁ。

without-k も、< や Decの展開とかできないし、Heterogenous は文句いうしで、割と

　　　最初から勉強しなおし?!

な気分。まぁ、なんでもそんなものですけどね。

Agda の option

なんか、library が --without-k ってのを使ってるのは知ってたんですが、なんか最近、without-k 使ってないと文句言われたことがあって。

群論(S₅がS₃を含む)ってのも見直してたんですが、

　 [ dba , aec ] = (abd)(cea)(dba)(aec) = abc

が Altin に書いてあるやつなんだけど、作ってるのは abc だけど、元は dba とかで違うものじゃん。adb = dba⁻¹ だから、半分はわかる。

で、プロシンで発表した時は「全部の存在を示す」みたいな感じでやってたんですが、群でやれば良いんじゃないか? と思ったんですが、

　　交換子自体は積に閉じてない、なので、有限生成して群にする
　　なので、S₃から要素を取り出しても、交換子とは限らない

あだだ。でも、q が交換子なら、共役元 p ∙ q ∙ p⁻¹ は交換子になるってのを交換子群が正規部分群なことを示すのに使ってた。なので、
dba とか、abc の共役元で良いじゃん。で、次の一行で良いらしい。

　　 abc ≡ [ (dc)(abc ⁻¹　)(dc ⁻¹　)　, (eb)(abc) (eb ⁻¹　) ]

これで、abc の逆元と共役元から abc が作れるので、これが可解群 (いつか交換子群列は{ε}になる)の反例になる。簡単!

なんですが、

　　　チェックが全然終わらない。しかも、全部つながってるのだが、つなげると時間がかかる

　　% time agda　sym5h.agda
　　Checking sym5h (/home/teacher/kono/src/galois/src/sym5h.agda).
　　agda: Heap exhausted;
　　agda: Current maximum heap size is 3758096384 bytes (3584 MB).
　　agda sym5h.agda　1429.15s user 19.74s system 99% cpu 24:09.22 total

なので、もしかして、--without-k 使うと良いかと思って。なんだが、最近は、

　　{-# OPTIONS --cubical-compatible --safe #-}

と書くらしい。なんか、1 < x とかを展開するところで文句言われるので、かなりなおさないとだめらしい。で、

　　Dec p の展開で yes / no でも文句をいう

なので、何回いろいろ問題があるっぽい。たぶん、version 不整合とかかなぁ。

特にねたのない日

ま、無理して書く必要はないんだけどね。

BD-RE を買いにいったんだけど、ケースの方がない。48枚入りを使ってるんですが。そういえば前は通販した気がする。

でもさ、メディアとケースは組で売るものな気がするんだけど? 注文すれば買えるみたいではあるが。

Well-defined

数学だといろんなところで聞く用語なわけですけどね。Agda だと、

　　f-cong : {A B : Set} → {f : A → B} → → A < x ≈ y > → B < f x ≈ f y >

こんな感じ。数学だと型書かなかったりするから、x = y → f x = f y とか書いてある。

自明なのになんでと思うわけですが、≈ が関係だと自明にならない。ところが ≡ だと自明になる。後者は

　　data _≡_ {A : Set} (a b : A) → Set where
　　　 refl : x ≡ x

なので、Agdaの項として等しいという意味ね。

　 _≈_ : {A : Set} (a b : A) → Set
　 a ≈ b = ?

で自分で勝手に定義する。剰余群だと、mod 2 で等しいとかそんなの。なので自明じゃないので証明する必要がある。

なんで、Well-defined っていうかっていうと、関数の定義が集合論だと二つの集合の関係で well-defined なものだから。

　 F : {A : Set} (a b : A) → Set
　 well-defined-F : {A B : Set} {a b : B} {c d : A} → A < c ≈ d > → F c a → F d b → B < a ≈ b >

まぁ、にてるっちゃにてるけど、別なものだよな。

Agda / 直観主義論理だと関数が先だから、それは必要ない。

凖同型写像 f : A → B は群の構造を保存するわけで、それは A < a ≈ b > が保存する、つまり、B < f a ≈ f b > だってこと。
同値関係を保存するっていう方が明確な用語だよね。

面白いのは、圏論でもこの問題はあるのだが、大体省略されてる。圏の性質を保存する関手の定義には実は cong が必要。

剰余群 G / K は、Gの要素を a ∙ b ⁻¹ ∈ K という同値関係を持つ群に読み替えただけなので、f : G → H はそのまま f : G / K → H
になる。違いは

　　G < a ≈ b > → H < f a ≈ f b >

と

　　G/K < a ≈ b > → H < f a ≈ f b >

だけってことね。 GK < a ≈ b > は a ∙ b ⁻¹ ∈ K なので、x ∈ K → f x ≈ ε が凖同型定理の仮定なので、

　　f x ≈ f x ∙ f y ⁻¹ ∙ f y　≈ f (x ∙ y ⁻¹ ) ∙ f y ≈ ε ∙ f y ≈ f y

ってだけ。 これが凖同型定理だった。G / Ker f ≈ Im f も問題はそれだけでした。

剰余群の GK < a ≈ b > → GK < c ≈ d > → GK < a ∙ c ≈ b ∙ d > も、

　　a ∙ c ∙ (b ∙ d) ⁻¹ ≈ a ∙ c ∙ d ⁻¹ ∙ b ⁻¹ ≈ (a ∙ b ⁻¹) ∙ (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹)

で、(a ∙ b ⁻¹) ∈ K , (c ∙ d ⁻¹) ∈ K そして、共役元 (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹) ∈ から出る。

こうすると、共役元が K に属するのが剰余群の条件だってのが良く見える。

残りは自明だってのを納得するのに時間がかかった感じ。

BDレコーダー故障の続き

いや、まあ、もう録画止めてよいんですけどね。Amazon Primeの画質とか字幕の扱いは最低だが、それは地デジ/BSもにたようなもん。

でも、最後なような気もするし。惰性な趣味でもある。

BDZ-FBT1000 の光学ドライブがいかれただけなので、ソニーの一台買ってきて dubbing でいいかってわけですが、

　　接続がめんどい。AV AMPがどうこうで、学習リモコンがほげほげで。

元のをハンカチで目隠して、リモコンモードを変更。接続ポートを学習リモコンに登録。

なんか製品登録がソニーのアカウントと統一とか言われてる。まぁ、それはいいけど。

あぁ、前回のBDZ-FBT1000は登録されてないのか。ヤマダ電機で見つけたのは

　　BDZ-FBT3000

う、同じ時期の製品か。ま、いいか。ところが、

　　肝心の引越しダビングが開始できない

Firmware update (USB経由)とかもやったんだがだめ。でも、TVサイドビューはつながるのか。もしかして...

　　Wifi station ではなく、LAN Switchに二台ともつないだら認識した

最近のWifi stationって、broadcast 通さないのか?

ところが、

　　99個ずつ?!

まぁ、せこせこやれば終わるかな。メディアはBDZ-FBT3000の方では認識しました。

Ruby on Rails / Akatsuki

Free Radious は DHCP6 に対応しないようなので、Kea DHCP なんですが、それに合わせて Akatsuki をなおす必要がある。

まぁ、atton の置き土産だが、この前、PowerDNS対応したので楽勝なはずですが...

Ruby on Rails の package system って Gemfile に頼っているところがあるらしく、

　　Gemfileを用意しないとどうしようもない

いや、そこにソースあるんだから、そこから Gemfile を生成しろよと思うんだけど。まぁ、それは今あるのを使うんだが...

pddmanの Dockerfile が、まず、

　　COPY . /app

する。で、config だけ -v で map する。わけわんないんですけど。ファイル変更する度に podman build するのか?!

まぁ、debug する時だけ、そこを -v するっていう手もあるが... まさか、中から git する方式?!

この辺は、sigularity の方が開発向きではあるよな。

Readable Code

Twitter (自称 𝕏 )で、 話題になってたので学生部屋に置いておきました。

短いのは良いね。コードコンプリートはでかすぎる。

変数や関数名の付け方とかは英単語の話が多くてさ。get じゃわからんとか。同義語辞典使えとか。

コメントには、そのコードでないと起きる良くないことを書けとか。インデント深くするなとか。

まぁ、書いてあることは浅いんですけどね。後書きで須藤さんが

　　とにかくコード読め、読む文化を作れ

って書いてて良い感じ。

最近は証明にはまってるから

　　プログラムは正しさがわかるように書け
　　型は正しさを部分的にしか保証しない

ってな感じですね。

https://amzn.asia/d/351ioUJ

家系ラーメン

なんか大平の昇家の後が武蔵家になってたのでいってきました。ガテン系兄ちゃん二人。なんだが、

　　激アンモニア臭い

おまえらなぁ... でもめげずに注文したんだが、激しょっぱい。家系割とありありなんだが。東五反田のもそうだった。

でも、それを除けば。まあ家系でした。だた、なんか麺少なめだな。もしかしてご飯込み? 半ライスくらいつけるといいかも。

味薄めにできるらしい。いや、もう一回いく気にになるかどうかは。

はるやもやってるみたい。

コンビニで戸籍謄本

いや、とれるって話は聞いてたんですが、そもそもなん戸籍謄本が要求されるのか理解不能。しかも、郵送。

そんな手続き全廃するべきだろ。ネットでいいじゃん。そのためのマイナンバーなんじゃないの?

なんだが、なんか拒否される。

　　なんか、申請ボタンがあるぞ? なんだこれ? 馬鹿の仕業か?!

しかも、

　　5日待て

とかいってる。まさか

　　仕事なくされるのが嫌だから手作業残したのか? 馬鹿すぎるだろ...

例外処理なら、まだ理解できるが...

凖同型定理

学部の時の阿部先生の代数学の本を見直してたら唐突にできました。

　 Given two groups G and H and a group homomorphism f : G → H,
　 let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
　 (where G/K is the quotient group of G by K).
　 If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
　　　 https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
　
　　　　 f
　　　G --→ H
　　　|　 /
　　φ |　/ h
　　　↓ /
　　　G/K

ってだけだが、剰余群 G / K は要するにG要素の分類なので、Gと等号だけが違う群に過ぎない。

なので、 h は結局 f そのものでよい。φ も id でよい。なので、凖同型定理のほとんどは自明。

問題は、hの凖同型写像の条件の一つの

　　aN ≈ bN → f a ≈ f b

だけで、それ以外は f が凖同型写像なことからでる。これは、

　　GK < a ≈ b > → a ∙ b ⁻¹ ∈ N

なので、f (a ∙ b ⁻¹)　≈ ε から、f a ≈ f b だけだった。

代表元がどうこうとか、φ の逆射があるとか、いろいろ寄り道したが、それらはまったく関係なかった。

G / Ker f ≈ H まではやるかも。

カフェの灯り

まあ、いいんだけど。燃えるんじゃないかと少し心配。

紙っぽかったけど。

猫の結界

何か、新しい猫グッズが登場してるんですが、

　　そこにおじいちゃん猫が寝ると、お嬢ちゃん猫が手を出せない結界

になるらしく。原理は不明。単になれてないだけかも。

Alexa と Switch Bot

ホームオートメーションの基本みたいな感じですが、ラジオとしてでもいいかなと。

なんだが、

　　共有して使おうとするとめんどい

なので、自分は設定する気にならず。奥様の方は主にクーラー制御に使ってるみたいです。

HAL研のリモコンとか、USB赤外線とかもいろいろやったが、

　　いろいろ不都合がでるのに対処するのがめんどい

それに、

　　無線や赤外線の信頼性の低さとか

まぁ、一時期がんばったから、もういいかな。

lldb と Rust

Rust は LLVM base なので、普通に lldb / gdb が使えるわけですが、

　　使い方がわからないから printf debug

とか言ってるのがいたので..

　　cargo build
rust-lldb target/debug/rust-dbms

で普通に動く。

　　b main

だと、C側にかかるらしく、いきなり ARMのassemlerがでるけど、普通に Rust の関数に break point を掛けられる。

ChatGPT は質問している方がわかってるところまでしか聞けないところがあるので、ソースコードデバッグを
知らなければ、まぁ、質問しようがない。

もっとも、最近は、debugger 使わずに log base で debug するのが普通ならしい。Haskell とか break point の意味ないし。

水星の魔女

こっちも終わりまでみました。まーた、超能力エンドかよ。Vガンも逆シャアもそうだったし、進歩ないな。

お母さんが何したかったのかも良くはわかんないんです。でも、まぁ、

　　普通にしてれば、普通にハッピーエンドになる

そういう力はみんな持ってるはずなんだよな。そういう話だったかも。

まぁ、SFというよりは感性で進むみたいなものだからな。

BDレコーダーとか、Wifi経由のDLNAとかが割と不調。ご機嫌とるのも飽きたので、もう録画はやめてしまうかも。

宇宙兄弟

ちょっと絵があんまり好きな感じじゃなくて。敬遠してたんですが、ジャイアントキリングのあと読むものがなくて。

読み始めたら、六太が良い感じでした。時代背景はばかプーチンのおかげでだいなしですが...

この手の宇宙物って大故障大会なのが多くて。まぁ、宇宙兄弟もそうなんですが、実際のシステムだと細かいトラブルはあるからなぁ。

ISSも廃棄は確定だし。一方で月は、まだ有人は再開せず。

もっと自分は、ISS廃止賛成だし、月は無人でやった方が良いみたいな考えですけどね。