写真の管理

いろいろあって、音楽の方も写真の方も

　　できるだけ iPhone 上に置かない

方向に。iCloud に置くのは、あまりに人質ぽくって。結局、

　　Google Photos に圧縮ありで同期
　　Original は手動で MBP に取り込む
　　Photos.app から yyyy/mm/yyy-mm-dd/IMG* 形式に変換
　　それを手動で Desktop / NAS に backup
　　iPhone 上のはたまに削除

という方法に。Google Photos には昔の物も入れたので、それで困らない。

Original が欲しいとか、もうないけど、Google Ban の可能性はあるからなぁ。

iPhoto.app/Photos.app の振る舞いには、いろいろ困ってるわけですが、

　　Mojave から Terminal.app / xterm からの Photos.app への access が default で禁止

という嫌がらせも。設定すれば良いだけだが、これも人質政策の一貫か。まぁ。やっばい写真で Google Ban とかあったからな。

iTnues Match

人は三十代に聞いた音楽で一生を過ごすとか...

まぁ、いろいろ聞いている方だとは思うけど、音楽のSubscription系は高すぎると思ってて。音だけでNHKと同じくらい取るのは何様だ的な。

それにCD借りてきた方が安い問題がなぁ。もっとも、そこまで聞きたいと思うようなものも、もうない。特に、

　　車に乗らないので、聞く機会がない

ってのが大きいかな。別になくって問題ないわけで、

　　わざわざお金出さない

的な感じはあるかな。もっとも、

　　今まで買ったものはどうなの

ってのはあるので、自分のiTunes Library がいつでもブラウズ/再生できる iTunes Match は合ってるとは思う。

とか言うのに気がついたのは、iTunes Libaryの同期が切れてることに気がついたからで、それくらい聞かなくなってるってことか。

iTunes Match は最大25,000曲くらいなんですが、手持ちは8,000曲くらい。制限に引っかかってる人もいるだろうな。

制限があるのは、商売仇がランダムデータを何十万も登録するとかやるだろうからな。

オライリー本

まぁ、買わなくなって久しいわけですけどね。Anatofu が買うのは職業上の理由だろうな。

Perl も TeX も、油断するとかなり知識が古くなるので注意しないとダメだが、オライリーの日本語版は「最初から古い」

Perl6 は仕切り直し的になって、Raku はPerlからは独立な感じに。Perl5 の変わらなさは面白いともつまらないとも言えるな。

自分は Python は嫌いなので使わないのですけど、いつまでも Perl でいいのか問題も少しあるかな。

Anatofu も golang / Rust はいろいろやったみたいだが、まぁ、普段使いは Perl になってます。

学生には日本語じゃなくて英語の本を読んでもらいたい。

Bi-cartesian Closed Category

Topos は Pull back で書くとか割と順調なんですが、教科書通りだと

　　Internal Language つまり、直観主義論理/型付きλ計算

に突入。なんか重いな。なので、去年やり残したところをちょっとやってます。

Cartesian Closed Category は積(つまり∧)しか入ってないので、和(つまり∨)を入れようって話。問題は、

　　○ : Hom A a １

の双対の

　　□ a : Hom A ⊥ a

つまり「矛盾からは何でも出る」って奴が入るってことね。CCC には

　　Hom A (a ∧ ⊥) c ≈ Hom A ⊥ (c <= a )

があるので、

　　 Hom A a ⊥ -> a ≈ ⊥

が出てしまう。(いや、割と道のりは長いんですけど) T 側でも状況は同じで、Bi-cartesian Closed Category には

　　実質的に二つしか対象がない、つまり Bool 代数になる

ことになるわけ。命題論理になってしまうわけだな。なので、直観主義論理/型付きλ計算のモデルには使えないので

　　Topos

ってことになるらしい。あとは、

　　Functional Completeness (= coMonad)

をやると、復習のネタは尽きるみたい。去年はここでGraphに走ってしんだはずです。合流性とかC-Monoid とか載ってるけど、まぁ、いいかな。

金網に沿って

ちょっと面白いかなくらい。

卒業ハリーズ中継

時節柄、ハリーズに集まるわけにもいかないので。去年はぎりぎりやってたんですけどね。

ハリーズ組と、冷凍発送なOB、持ち帰りな現役組の三つにわかれて Zoom みたいな感じです。

ハリーズレベルのスープカレーってなかなかなくて。東京組も懐かしく思うらしい。

Spacial Chat の方が良いかな。

現役組はOBとの連携が重要だと思うんだけど、なかなか難しいみたいですね。

OB組は LINE なのと、そうでないのとあるみたい。

Dual Boot

まぁ、Apple の macOS もいろいろダメになってきていて... さんざん、ubuntu 使って、singularity の環境設定とか podman とかが macOS ではいまいち...

なので、anatofu (今年修了な) が選んだのは ThinkPad。なのだが、

　　事務が Windows なExcelを要求するらしく、Windows と Linux を行き来するはめに

別にVMとかLibreOfficeで良いじゃんと思うのですが、こだわりがあるらしく。再インストールですか。で、

　　「だったら、Dual boot にすれば」

と言ったんですが、実は最近はよろしくないらしい。

　　Windows が年二回の大型updateで、UEFIを上書き、さらに partition も変更

なるほど。そういう嫌がらせか。partitionも変更されてしまうので、その辺をrecoveryできないと詰むらしい。さらに、

　　あまりに何回も再インストールしたので、SSDが故障

さすがです。まぁ、初期不良踏んだんだろうとは思いんですが。で、1万円で1TBのを買ってきて換装という羽目に。

どうも、違うdriveなら上書きに耐えるらしい。なので、SD cardからWindowsを上げるのが良いんじゃないかな。

ThinkPadは、Wifi slotにSSDを刺すなんて言う技もあるらしい。

いや、僕は Windows はVMで困ったことないので、それでいいです。

https://qiita.com/gpioblink/items/708b2a5add6c854965cf

カートリッジ交換 Ortofon Ω

この前、いろいろ修理した時に電気屋さんが「聴いてみたい」とか言うのでレコードかけてみたんですが...

　　なんか、だめだめ

なので、AT15Egも寿命だよなと思って検索したら、Ortofon Omega が結構安い。これでいいかなみたいな感じで。

なのだが、

　　配線が老眼で厳しい

やっぱり、巨大拡大鏡欲しいかなぁ。まぁ、配線終了。でも配線中に発見したのだが

　　AT15Egの針が緩んで下にずれてた

それが原因か。もっとも、それ直しても、さすがに新しい方がまともに鳴っているので良しとします。

Denon と比べるな説もあるが、もうあんまり気にしない。

アームもだいぶ怪しくなっててな。あ、なんか TEAC のがアームは SAEC なのか。買っちゃおうかな。

Ortofon は針圧高めが良いので、まぁ、しばらくは。

学科システムの使い方 hands on Hugo

自分の趣味のシステムだったりするからな。特に静的Webは売りだったりするんだが、

　　gitlab から push で CI 起動

う、うーん。実は自分は、もっと簡単で「手元で Perl で生成→ rsync でuoload」だったり。なので、

　　手元で Hugo で生成→ rsync でuoload

が簡単なんじゃねと思わなくもないです。

最初の repository の設定を script にしたらと言ったら、なんか gitlab API を叩いたり、json 生成したりな

　　golang binary

ですか。正直に言えば

　　怪しいバイナリ動かす気になるか?

ってところがあるけどね。shell とか ruby とかあるだろとは思いましたが。

hands 自体は順調だったんですが...

　　OSが High Sierra な人が

それは想定外だな。と言っても、僕もまだ、Mojave 使ってるんですけどね。なんか、どんどんダメになる感じがな。まぁ、まだ、

　　SIPはずせばなんとか使える

感じではあるんだが。

このまま動画にしておいてもらうつもりです。動画の方が良い人の気持ちは理解できないが、必要なんでしょ?

Topos

卒論修論片付いたので。いや、やるべきことはあるんだけど、Topos を Agda でやってないなと言うことで。

Lambek 先生のには

　　Sub ≅ Hom(-,Ω)

とか簡単に書いてあるんだけど意味不明。Sub は Suobject Functor らしいんですが、型くらい書いてくれてもバチは当たらないんですが。

でも、もちろん、ちゃんとした定義もある。Subobject Classifier を pull back で定義するですか。実際には Equalizer 使うわけね。

書いててわかったんだけど「お前、一回もToposの定義をちゃんと読んでなかっただろ」すみません。その通りです。

record Mono　{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set　(c₁ ⊔ c₂ ⊔ ℓ)　where
　　 field
　　　　 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ]　≈ A [ mono o g ] ] → A [ f ≈ g ]

record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)　( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :　Set ( suc c₁　⊔　suc c₂ ⊔ suc ℓ ) where
　　 field
　　　　 Ω : Obj A
　　　　 ⊤ : Hom A １ Ω
　　　　 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])
　　　　 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω

　　　　 char-ker　: {a b : Obj A } {h : Hom A a Ω}
　　　　　　 → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ]
　　　　 ker-char : {a b : Obj A} →　(m :　Hom A b a) → (mono : Mono A m)　→ Iso A b (　equalizer-c (Ker ( char m mono )))

と割と簡単に書けた。

なんだけど、Equalizer とかがごねてるな。Agda 入れ替えたからな。と思ったら、存在量化を知らなかった頃の旧悪が露見。

Equalizer の復習からか。どこまでやるかは謎です。竹内先生の「矢印を追うだけでできるやつ。積とか」からかな。

みそ汁

まぁ、お腹はなんとかなった。ってよりは、いつもの程度の不調に戻ったわけですが、

　　ここ三日間のお昼は、みそ汁(ご飯半分)

二日酔いと胃痛の友みたいな感じです。

パチンコ屋さんの二階(ひまわり)で、600円。ポークでないところがよろしい。

近所の碁会所のおじいちゃん

最近の飲み友達だったんですが、なんか1月になくなってるのが発覚したらしく。一人暮らしだったのだな。子供はいたはずですけどね。

あんまり良い飲み方の人ではなかったので、ほとんどの店から「出入り禁止」。まぁ、僕には矛先は向かなかったので...

いや先月与那原のオリオン通りで一緒に飲んだばっかりだったんだけどな。沖縄、こんなの多い

　　先週まで一緒に飲んでたのに、帰り家の前で転んでそれっきり

とか。心筋梗塞説が出てたが、医者はわからないと心筋梗塞と書くからな。でも、

　　割と依存性の少ない人

ではあったかも。親友の一人は落ち込んでました。まぁ、

　　割とうらやましい

気もします。

卒研発表

修士ともに無事に終わりました。あんまり、無事でなかった気もするが... いや、

　　今年はコロナだったという言い訳が...

いや、あんまり関係ないか。うちの研究室は、おっそろしく関係なかった。研究室でやってるかZoomでやってるかぐらい。

8,9,10 のシステム更新も楽しかったし。むしろ、旧システムの自分の知らなかった部分が面白かったかも。こんな風になってたのかとか。

いや、何年か前のWordpressのトラブルから全部見てたつもりだったんだが、それでも若干逃げてたかも。

今回も次の停電辺りで思い知るかも知れません。

いずれにせよ、卒研生、修論生、お疲れ様でした。

卒業ハリーズは、オンサイト、オンライン混成で、冷凍ハリーズ発送サービス付きです。詳細は tiwtter/facebook/LINE で捕まえてください。

UEFI

2014くらいにもtryしたことがあるんだが、まぁ、良くわからず。ラズパイにfirmを入れることはできるんだけど。

　　EDK2 のconfigが難しいらしい

らしいってのは卒論生にやってもらっているからなんですが。どうも自分的に優先順位が上がらず放置気味。今年はいろいろあったからな。

ですが、GNU-EFI が良いらしい。で、こいつを

　　qemu-system-arm で動かして...

で、gdb を接続して debug と。で、それが

　　singularity の中でできるので

「とくに環境設定しなくても動く」あとは、

　　それが、macOS の singurality 上で動く

ってのができると良いんですが、どうかな〜

マルチプログラミング

いや、ここ30年くらい聞かない言葉なんですが。元はダイスクトラ先生が使った由緒ある言葉らしいんですが...

　　学生のレポートに良く出てくる

おかしいなぁと思って指定した教科書を検索するんですが出てこない。でも、問題にはあるな。と思ったら、

　　Kindle の検索は exact match しかでない

なんだそれ。なのだが三ヶ所くらい。まぁ、そうだよな。ところが「ググる」と引っかかる。なぜだ。

そもそも教科書の問題からみで出しているので、本文読んで答えればそんなことにはならないはずなんですけどね。

もしかして「Web 上から写したものを見付けた場合は失格としてます」これのせいで、図書館の古い本を見てるとか?

まさかな。

Mutics とか MP/M 、そして、マルチメディアに続く言葉ですね。今だと multi process は使わないが multi thread はまだ使うか。

マイノリティ枠

女性は人類の中でマイノリティじゃないかまた別な話ではあるんですが、理系の中では女性はマイノリティなので。

それでマイノリティ枠は劣るみたいな、あるいは俺たちの枠をとりやがって的な話があるらしく。実際、ERとかでも見かけたことが。

でも、これには正当性があるってな話です。そもそも、

　　マイノリティだろうが男女だろうが、だいたい才能は同じように分布してる

わけ。だいたい、どんぐりの背比べだし。

問題は、そのどんぐりの背比べレベルの中での話ね。で成績順に取っていけば比率も正しくなるかいうとそういうことはなくて、

　　採用枠の条件に合う確率は多数派の方が高い

まぁ、当然。そこで黙って取ってしまうと、図のBみたいなのがたまたまない限りマイノリティは取られないことが多い。

で、まぁ、文句言うのは4,5辺りの人なわけだな。なので、ちゃんとマイノリティ枠を用意しないとだめってこと。

　　本当にずば抜けている人は枠とか関係なく自由にどこにでもいけるので文句は言わない

つまりマイノリティの方が「優秀だが機会がなかった」人がいるので、うちみたいな地方大だと、

　　むしろマイノリティ枠の方が優秀な人が来る

ことが多いです。なので、

　　マイノリティ枠は「わきまえる」必要などないので、自由に好き勝手に使ってください

雨の330

事故らなくても混んでることが多くて... バスの時間に合わせて出たのに、バス停に付いてもバスの位置が同じ。

5分たっても同じなので、さすがにおかしいと思って twitter で検索したらこれ。

大型トラックが中央分離帯を越えて反対車線のオービスの支柱をなぎ倒して、軽自動車を直撃ということらしいです。

登りは、その前は長い橋で、それからトンネル、それを抜けた直後だな。浦添そばあたり。

中部商業高校経由は動いているので、そちらで。

　　クソ雨の中を

ま、雨男なので気にしないんですけどね。この写真を見ると浦添はあんまり降ってなかったみたいだな。

https://twitter.com/gesu_yarooo/status/1359726359325462528?s=20

胃酸過多

盲腸以来、そんなに腹痛はなかったんだが... ゼミでいつものカレーを食べられる状態になく...

　　事務室に行って「胃腸薬ください」

大正漢方胃腸薬でしたが、胃酸は収まった。が、胃痛は収まるはずもなく... お粥で防戦だ。

いつものお医者さんでも「薬お願いします」で出してもらいました。が、

　　二日分って言ってたのに二十? おいおい。

まぁ、保つからと言ってましたがね。ファモチジンですか。てっきりガスター出してくれると思ったんだが。

つうわけで、今日はあんまり使い者にならないです。いつもか。

映画の英語

そもそもTENETはやっかいな話だし、会話と言うよりは思わせぶりな単語の単発だったりするからなぁ。

英語字幕と日本語字幕なしで二回見たわけですが...

英語字幕だと見逃しが多くて。うっとうしいし。字幕なしで通しで見てわからなったところだけ見直す的な方が良いかも。

先に日本語だと多分二度目は見ないだろうから... 2時間半二回は、つらいお年頃だし。

でも、字幕なし英語である程度聞き取れるようになるのは、そこそこ大変。そういうのを目標にする学生はもういないかも。

昔、私の履歴書で見かけたのは、24歳で遅いとか言われるのだが、ねばってやった勉強法が

　　映画を見て、内容を電話で先生に英語で伝える

ってな奴だった。電話は面白いよ〜。

映画は映像もあるので、最初の英語だけで聞き取れないと感じていても、もう一度見ると「確かにそう言ってたな」的な感覚がある。

人は言語を学ぶようにできてるし、聞いた言葉は頭の中にはなんらかの形で残ってる。それを意識的な形で思い出すことはできなくても。

でも、それをぼーっと見過ごしていてはだめで、内容を人に伝えるみたいなモチベがないと

　　頭の中に外国語の回路はできない

みたいな感じかな。機械学習は進歩しているのだから、それを人の学習、特に語学の学習に feed back して欲しいかな。

人に話してバグを見つける

モデル検査のコードを書いてて、なかなか動かなくて。なんとなくて眠れなくて朝4時から debug して「動いた」

と思っていたんですが、log を見るとやっぱり探索し切れてない。わかんね〜　なんですが、

　　学生にコードを説明してたら、ここで変数がずれてると降ってきました

代入しなおしでばっちりなおりました。独り言でなおすのも良くやるのだが、

　　声の大きさに比例する気も

ちょっとするかな。ただ思ったより遅くて、いろいろやることがあるらしい。

X11

いや、まだ使ってたりするんですが。Terminal.appの代わりなだけなんだけど。なんと M1 Mac でも動くようになったらしい!

まだ、M1 mac 使ってないんですけどね。16inchがでたら買おうかと。なので

　　Xquartz の新しいのがでた

ので入れたら

　　cut & paste が効かない

で、ぐぐったんですが、

　　emulate three button を入れろ

な、なるほど。確かにそういうのあった。それが reset されてしまったわけね。あとは、問題なく動いているようです。

まぁ、そろそろやめろ説あるんだが、VSCode とか vim のGUIとかに比べて、まだ、response が微妙に速くて...

と思ったが、Terminal.app だと、差はわからんな。

まぁ、将来、macOS を見限る時に役に立つかも知れん。そん時は、Wayland か。

https://eud.gsfc.nasa.gov/David.Friedlander/macintosh/mac_copy_paste.html

TENET

壊れたテレビを家に持ってきたので、なんか4Kと思ったが「どうやって何をみる」で少し困ったんですが、

　　PS4のApple TVでTENET

にしてみました。PioneerのSC LX87なAV ampが4K対応なので大丈夫らしい。いや、予想外に綺麗。最近、

　　MBP側が Retina なのでHDだとちょっと残念感があったので

なのだが、ケーブルネットの方が調子悪くてネット設定と格闘しながら。もっとも、

　　英語+英語字幕
　　日本語吹き替え

の二周はしました。この映画、冒頭7分でさっぱりわかりませんになるので二周は必要だな。

これは元ネタは時間衝突だな。これを理論付けるのは難しいけど「考えるな感じろ」とか言ってるので、まぁ、そんなものかも。

物理法則的には逆回しはエネルギー保存則に反しないので問題ない。問題は作中でも言ってたエントロピーですが、

　　等価原理はない

ので、割と自由にいろいろできる。決定論的に話が進むのは結構良くて、どうせなら「パウリの排他律」ネタも入れて欲しかったかな。

時間逆説を避けるのは排他律に寄る力として見えるってのが僕の主張なので。ただ、

　　動作の起点はどうなの?

って問題がな。もっとも自由意志は錯覚説もあるし。

　　出てくるのを見ると入ることができる

とかは面白かったです。ノーランだからコンピュータとかAIとかでてこないのがちょっと残念だったか。

ベイリー　時間衝突
https://www.amazon.co.jp/dp/4488697062

ドヤ顔

下から撮ると良いらしい

てだこ浦西の道

歩道は通れるようになってました。高速バス下りは削って降りられるようにしたみたいだな。それは良いんだが

　　駅からだと道を渡ることになる

結局、那覇向けの車はこちらを通るようになると思うんだけど、交通量が多いのを渡るのは微妙だな。

高速バスをインター経由で駅に持ってくるみたいなのは、あまり良くないと思うが... もっとも現状だと

　　よほどの好き者でないと乗り換えは不可能

と言いつつ何人かは見かけました。

ここにはヨナラボもあるんですが、最近寄ってない。

男の浪漫っぽいもの

大きめのスイッチとか、むき出しのなにかとか。

そういうのは普通に大学に転がっている感じ。

そういえば、うちには使ってない「巨大なパラボラ」があるはず...

壊れまくり

借家なんですが、

　ウォシュレット水漏れ
　BSだけでなく地上波もだめ
　12年目のクーラー
　火災報知器が断線でなりっ放し

といろいろ修理中。もともと大家さんが住んでいたところなので火災報知器の元締めがある。

明日はアンテナを見に来てくれるらしいが...

危険物

グラッパにチョコレートアイスクリーム

これは危ない。危なすぎます。