図書館から本を借りる

いや、卒論修論がぜんぜん進んでないっていうか...

でも、竹内外史先生の物理関係の本があったなと思って。中3階に置いてある。

昔は、この図書館のかびくさい感じは割と好きだったんだけど。なんか、

　　コンピュータ関係の本が絶望的に古くて...

80年代の竹内先生の本にも「リー代数の良い本が絶版で」とか書いてある... 結局、

　　無限小解析と物理学
　　リー代数と素粒子論

の二つを借りたんですが、どっちも割とダメぽい感じだなぁ。

無限小解析の方は、超実数の導入が証明/モデル抜きなんだな。それは無理でしょ。

伊藤積分とかあるらしく、論文紹介見たいな感じ。

リー代数の方も、両方中途半端な感じ。いや、証明あるので、まだましなんですが...

いや、あの練習問題があるようなのが欲しいんですか。

どっちも圏論のけの字も出てこない。むしろ避けてる感じでもあるな。

圏論ベースの量子力学は最近少しやられてるみたいですけどね。

ほぼ同じ時期に書かれたらしいので、大変だったのかも知れないな。少し入り混じってるし。

原神 世界レベル7 / 冒険者レベル55

そこそこ90がそろってきたので。先生はすでにもってたので甘雨を貯めてたので引いたら

　　行秋が完凸

なにそれ。甘雨育ってなかったんだが、練習と思って行秋つれて昇進試験にいったら、なんかクリア。

まぁ、そんなようなゲームらしくって。出やすい☆4が役に立つ。でも、おかげで

　　溜まっていたクエストはなくなった

なので、あんまりもうやることないかも。いや、

　　レベル上げた直後なので、雑魚に殺されそうになる

わけなんですけどね。いろいろイベントあるゲームなので、それをゆっくりやるくらいか。

甘雨/アモスの「適当に打つと当たる弓」って、なんかすごい。デイリークエストの弓に使えないという...

iOS update trouble

MBPから iOS をあげる習慣なのは、バックアップも取るからなんですが、(iCloud backupは最小)

　　最近、あんまりテストされてないんじゃないか?
　　そもそも、そんなことするやつ、もういないだろ

的な。昔は、そこから旧版アプリを復活させたりできたんだけど。

　　iPhoneを直接 mount していろいろやるとか

まぁ、つまらなくなった気もするが。

本題はそこではなくて、いきなり restore 画面に。appleのiphone restore pageを見ろと。

結局、

　　MBP側のMonteleyをupdateしてないと、restore 画面になる

ってことらしい。確かにMBPの方をupdateしたら先に進んだ。

いや、そういうのは update 始める前にいってくれよ。

Stream style programmming

Java 9 以降、Scala もそうなんだけど、

　　巨大なList / Queue を作って、それに lambda を map するプログラミング

が流行ってさ。並列処理向きとかいろいろあるわけですが。

　　for文を自動的に書き直す

にみたいな余計なお世話も。Rustとかもごたんぶんにもれずそんな感じ。

まぁ、その時代の流行なんだけどさ。一つは

　　fp 的な関数型プログラミング

だってのがあるとは思う。それはプログラムの正しさの証明につながっているわけなんだけど...

　　確かにListを構成する性質(property)が明解になる

というのはある。でも、

　　見かけの計算の計算量と、実際の計算量は自明には一致しない

ってのも。毎回巨大なリストを構築するわけはないわけで。そこを

　　コンパイラを信じる

ってやるかっていうと、まぁ、生成コードを見るか、実測するかどっちかなら、まぁ。

いつものことなんだけど、自分のやってる方向が真逆だったりするのが面白いかな。

ミステリーサークル

ってっわけでもないんだけど、水はけわるいからなぁ。

去年は、しばらく養生してたんですけどね。なんか偉そうな看板が立ってた。

さくら公園っていうんですが、桜がみれるようになるのはいつだろう?

昔は、この辺にイタ飯屋さんんがあった。新町含めて再開発みたいな話もあるらしいんですが...

うらそえようどれ

あの辺のポータルを取る人が... まぁ、へんぴなところはいいんだが、夜取るところじゃなくてな。

なのでお昼に。お散歩する人たちが結構。

桜もそこそこ咲いてました。今年は早めだな。

浦添前田駅から上に登る道ができる感じか。

咲樹の定食

我如古郵便局の少し先です。いや、だから〜

　　ミニ沖縄そばのどこがミニなんだと

ほとんど二人分だな。野菜炒めおいしい。

学生の怪しい食べ物

業務スーパーで買ったキムチと納豆二つらしいです。

ご飯入ってないのか?

時相論理

Agda の方も、その段階まで来たらしく。

　　data LTTL ( V : Set )　: Set where
　　　　s :　V → LTTL V
　　　　○ :　LTTL V → LTTL V
　　　　□ :　LTTL V → LTTL V
　　　　⋄ :　LTTL V → LTTL V
　　　　_U_　:　LTTL V → LTTL　V → LTTL　V
　　　　t-not :　LTTL V → LTTL　V
　　　　_t\/_ :　LTTL V → LTTL　V → LTTL　V
　　　　_t/\_ :　LTTL V → LTTL　V → LTTL　V

　　{-# TERMINATING #-}
　　M : { V : Set } → (ℕ → V → Bool) → ℕ →　LTTL V　→ Set
　　M σ i (s x) = σ i x ≡ true
　　M σ i (○ x) = M σ (suc i) x
　　M σ i (□ p) = (j : ℕ) → i ≤ j → M　σ j p
　　M σ i (⋄ p) = ¬ ( M σ i (□ (t-not p) ))
　　M σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M σ j p )) )
　　M σ i (t-not p) = ¬ ( M σ i p )
　　M σ i (p t\/ p₁) = M σ i p ∧ M σ i p₁
　　M σ i (p t/\ p₁) = M σ i p ∨ M σ i p₁

こんなものかな? 変な記号使わないといけないのがなぁ。いや、わかんない。もっと違う定義を使うかも知れないです。

Polymorphism ないから記号を使いまわせない。

Buchi / Muller automaton とか、自分のD論見直した方が良いかも。

あんまり差がない

なんか、工事終わったんですが、差がないように見えるんですが...

後付けの二重サッシは台風対策です。一号館でも台風の時には雑巾はさむ必要がある。

そんなに作ってどうする

なんか琉大周辺にレンタル自転車が... 確かに僕とか学生はたまに使ってるんだが...

　　お前ら、作りやすいところに作ってるだろ〜

そうじゃなくて、与那原側とか普天間とか作るべきところあるだろ〜

原神の現状

相変わらず世界レベル5なんですが、次にいくにはLv90にあげる必要があるらしく。タタラ物語も歯が立たないしな。

なんだけど、5人80突破したら、いろいろ使いきったらしく

　　何をするにも、しばらく待つ感じに(樹脂回復を)

まぁ、あせってやるようなゲームでもないしな。将軍、絢香、先生、ディルック、主人公をしばらく90まで上げてるはずです。

逆に言えば、それくらいしかもうやることがないともいう。厳選? 資源的に無理だな。

子供の頃の絵

画家のしんおじさんが書いてくれたものです

小さい頃の記憶は割とある方だが、これはかなり小さい頃だからなぁ

横断歩道

P's Square の前、バス停のそばですが

　　去年からずーっと消えてた

ないのかと思ったよ。塗りなおされていた。まぁ、あんまり尊重してないんですけどね。

押しボタン式じゃないんだよな。

もっとも、P's Squareにいく人でバス使うのは僕以外みたことはないです。

マクドのポテト

まあ、人々、あるいはマクドにとっては象徴的なものらしく。

コンテナの関係で海運が滞っているってのが理由らしいんですけどね。

自分的には原田社長の時に導入されたサラダを選択するので関係ないのだが。

サラダなんか消費者は求めてないってな話もあったけど、

　　自分はポテトをサラダに変えられなければ、マクドにはいかない

前にクーポンの関係でポテトにした時もあったんだけど、やっぱり、もはや無理な感じ。

でも、クーポン系だとポテトなのは、やっぱりポテトを売りたいのだろうな。

空中都市008

NHKの超昔の人形劇ですね。子供部屋を増やすのにねじみたいいな建物を回転させると部屋が増える! みたいな、そんなギミック。

空中都市の下にはラミネートパイプが張り巡らされていて、そこに落っこちると二度と戻れない。とか

　　小松左京のセンスはいまいち意味不明

だけどさ。今だからこそ、そういう未来のイメージをドラマとかにするべきだろうな。

でも、ひょうたん島もそうだったけど、

　　話が冗長

だろうなと今は思うかな。サンダーバードに原子力旅客機が出てた時代だからな。アトムももちろん原子力だし。

宇宙船木星号であの世にいくみたいなドラマもあったような気がする。妹が〜みたいな話で、ほとんど夢落ちな。

ラジオのSFドラマもあって、冷たい方程式とか良かったかな。

今の子供たちはネットで見る感じなんでしょうけど...

花ぐるま最後の日

近所のいきつけのお店でしたけど、さすがに

　　建物がお取り壊し

らしく。月末までとかいってたんですか、今回の再流行でお休みに。

なんか引っ越すとかいう話は去年から出てたんですが、

　　ママは何にもしてなかった

らしく。いや、もう47年やってて、ママのお年もな〜

去年は転んで入院で休みとかやってたし。そろそろめんどくさくなってるのがわかるよ。

確かに安くて居心地のよいお店でしたけどね。(最初の頃の客層はひどかった...

いや、ママ、10年間ありがとうございました。(いや、まだ、移転する可能性がほのかに...

WebEx

なんか某所の会議で使うはめに。いやさ、某銀行なんですが、

　　会議の番号とパスワードを口頭でいうのはやめてくれ

アプリにすれば良いのかと思ってアプリ入れようとしたら、M1用はないらしい

あっそ。Chromeとか popup block 切ったりとかしたが関係なかったらしい。結局、パスワード入力の問題だったらしい。

結局、Safari でつながった。20分くらいかかったかも。もっとも、つながらなかった面子もいたので

　　別に自分だけがたこだったから

ではないらしい。

SMSでもなんでもいいからっていったんだが、口頭以外禁止らしい。

s/mime とか言ってはみたが、MBP移行した時に鍵を持ってきそこねてるな。Time Machineから復活できるのか?

.NET / Rider / Unity

まぁ、学生の環境に付き合って。どれも Bug Sur M1 の環境で動くわけですが..

　　ダウンロードに少しコツがいる

Unity hub 使ってはだめとか、少しはしっこのリンクからとか。

ちょっとはまったのは、JetBrainsの one time password 。ばっちり機種変でなくしてた。なのだが、

　　JetBrains は二段回認証の時に予備の one time password がある

え、それっていいの感があるんだけど、まぁ、助かった。

ところが、Riderで project を hg から checkout すると....

Failed to load A, error: dlopen(/usr/local/share/dotnet/host/fxr/6.0.1/libhostfxr.dylib, 0x0001): tried: '/usr/local/share/dotnet/host/fxr/6.0.1/libhostfxr.dylib' (mach-o file, but is an incompatible architecture (have 'arm64', need 'x86_64')), '/usr/local/lib/libhostfxr.dylib' (no such file), '/usr/lib/libhostfxr.dylib' (no such file)

え、なんだよ。ぐぐるとかなりの人がひかかってて...

でも、新規プロジェクトだと動いてて、要するに

　　.NET framework の version 設定

の問題だったらしい。いや一応探したんですけど、その

　　メニュークエストが IDE の欠点

だからな〜 解決してめでたい。

Godiva

普通に普段使いで便利。どこにでもお店あるし。

でも、明治のブラックの小分けのやつも侮れない。いや、それ以外の日本のダークチョコレートは残念なんだけど。

(さいそくではありません...

真志喜置の歩道橋の続き

いや、もうできてるんですけどね。まだ、封鎖中。

別に歩行者のために工事したわけじゃないからさ。

　沖縄で歩いたりバス乗ったりするのバカだけでしょ
　まして歩道橋登る人とか...

おっしゃる通りです。いや、だから

　高いところ好きなので

我如古の横断歩道も良く使ってるな。

桜

一本だけだけど。今年は妙に暖かいというか暑いからなぁ。

日差しが、全然冬じゃなくて...

プロシン最終日

温泉でやらないプロシンの意味とは...

うちの発表は二件、AgdaによるHoare Logicと、RakuのServer baseでの実行でした。

そこそこ質問も出ててよかったかな。確かに fork して実行する方がいいか。

懇親会には gather を使ったんですが、あんまり参加しませんでした。

https://prosym.org

プロシン参加中

なんかいきなり

　　今の大学の研究室って企業の環境よりしょぼいよね

とかいう話が。それはPFNとかFixstarsとかと比べれば。選択と集中なのでTsubameとかOISTはまだ。

2年続けてオンラインなので少し迷走しているかも。もっとも、もともとそうだった気もする。

Viscuit をクラウド化したら、小学生のSNS化して荒れたって話が面白かったです。

うちの学生の発表は明日〜

らーじゃんめん

佐真下公園のはちれんに「つけめんでない」ラーメンが登場してたので。

いや、1月なのに沖縄暑くて。辛いものとか食うと汗ばんでしまう...

文字の大きさ

自分もMBPのぞきこまれて、

　　全然見えない

とかいわれているわけですが、学生のこれ。

　　この大きさは無理だろ

いや、僕も k14 を Retina 最高解像度で使って

　　やっぱり無理

となったわけですが。それでも、

　　Zoomで画面共有なら、まあ、なんとか

な感じではあります。

　　Windowsはフォントがいまいち

自業自得だろそれは。

プロシン

今年は金曜日かららしい。水曜日までは参加申し込み可能。オンラインです。

うちは二件だします。え〜、まだ、発表資料できてないの?

https://prosym.org

pumping lemma

Automaton の最初の方で出てくる定理ですね。正規(最近は正則って言うらしい)言語でない言語があるのを証明するのに使います。

かっこの対応をとるのは正規言語じゃないっていう定理なだけだが、補題の方が応用が効くので便利なことが多い。Agda では

trace-xyz : Trace fa (x ++ y ++ z) q
trace-xyyz : Trace fa (x ++ y ++ y ++ z) q

とか書くらしい。途中の状態が重なればそうなる。Trace は automaton fa が受理するのを表すデータ構造、あるいは、そういう性質。

証明自体は簡単なんですが、その簡単な証明を Agda で書くのは別問題。

なんで、年末年始にそんなことしたのはかは割と謎なんですが、授業で使うには複雑すぎる。まぁ、いろんな証明の例題の一つか。

複雑なのは証明の方なので、命題だけをみせて、証明は概略だけとかかな。いや、

　　神は detail に宿る

でしょ。いろいろ Agda の技術がみれて面白かったです。自分で書いていくというよりは降ってくる、あるいは、Agda を使って発掘してく感じ。

count 使う方が簡単ならしい。

5555

いや、それだけ。近所の使いやすいお店です。