MBP16

じゃ〜ん〜 32GB/1TB な控えめのやつです。

2017からだったからな。でも、少し設定するのが気が重い。もっとも、Catalina よりは抵抗ないですけど。

たぶん、USB-C なLAN adaptor が動かないな。

太くて重い。学生もいってたけど、2017の方がかっこいいかな。でも、

　　キーボードが良さそう

なにせ、

　　ESC key あるし！

MacDonald の電動バイク

この赤はなかなか良い感じ。どうも、

　Uber eats ではなく、ちゃんと自前の従業員を保険対応で

ということらしく、そういう意味で好感度高い。

もっとも、だから

　Macの take out の配達を頼むか

というと、微妙かな。

Uber系は従業員の待遇悪くして儲けるという日本の悪い習慣を輸出しているようなところがあってなんだかね。

生活保護あるいは所得補助みたいなのと組み合わせて、配送インフラと所得再配分を一緒にやるみたいなのが好みかな。

長田のレンタル自転車

なんと、交差点の向こうと手前と二箇所にあるらしい。でも、縮小ぎみな気がするのは気のせいか?

　　もっと、屋根のある所に置いてほしい

感じ。野ざらしなのはな。

でも、ここは98との乗り換えが100m以上なところなので目の付け所は悪くない。

大学からキンタコに行くのに便利か? そばやさんも長田にできたしな。

ここから、市役所まで自転車置き場はない。微妙ね。

Audio

もはや死語な気もするわけですけどね..

Accuphaseのプリメインのイコライザーとかもろもろが死んでるらしくって...

修理するべきだろとは思うのだが、自分でなおす根性は微妙。コンデンサーちまちま交換でもいけるはずだが。

ユニゾンカフェの一階で見かけたのも良さそうだが、この大きさにしては良い値段だな。

　　イコライザーは bluetooth 接続

うーむ。

スマピでもよいと思うが、もはやあんまり聞かないことも確か。

酒が飲めるぞ〜

ってことらしいです

やきがまわってる

いや、自分でやってる継続ベースの言語は、結構、まったく違ってて、特に

　　再帰じゃなくてループ

ってのが。で、久しぶりに再帰な関数型で書くと勘が狂うんだこれが。

depth first search で listとか、差分リストですらで書けるわけはずですが...

　　なんか、はまる

そして、諦めてバス停で待ってると

　　code ごと頭に浮かぶ

昔は、その場で Libretto で書いたりしたんですけどね。

いきなり差分リストで書き出すはずなのに、なんでそうしなかったのかげせん...

プログラミングプロジェクト -- ゲーム班

PBL ですけどね。そんな言葉が出る前からやってて。実験でものづくりやろうみたいな感じで。

ゲーム作ろうみたいな感じだったけど、来年からは似たようなのも増えたのでサーバ班に戻そうかなと。

なのでゲーム班は今年が最後っぽい。

なのだが、既に良く覚えてないのだが「それだったら、node.js が良い」と言ったのだが、

　　よくわからんので、python + AWS で

え、それ python 嫌い僕にいうわけ? と言っても、node.js は JS でやるのか。最近は typescript が流行だが..

気持ちはわかるんだが

　　ほげほげ諦めて、ふがふがにする

というのをやるたびに、環境設定にそれなりに時間がかかる。でも、

　　最近の開発系の検索の悲惨さが残念

google/duckduckのだめさかげんか。もちろん、SESとかやってるバカたちがいけないわけだが... コピペ技術blogとか。

なので、マニュアルと有料技術書な時代に戻ってる感じもあるね。マニュアルだけでやれと思うくらい。

日本語で検索するので2019なライブラリとか使ってて、2年前だと絶望的に古いとかいう問題がある。最新を見ると

　　deprecated

というわけね。最新が良いとは限らないわけだが、学生は最新やるしかないだろ。

新城あたり

前は優雅な外人住居地だったんですけどね。

なんかダサイ造成やってるな。

上大謝名の美容院の絵

絵自体は可愛くてよいんですが...

　　ハイヒールでお仕事はどうかな

まぁ、美容院は女性にとっての社交場って話もあるから、ありなのかな。

どうせなら、かっこいい方が良いものね。

停電

この間から計画停電ごとに機材が壊れるってのが続いてて..

今回は前もって落としてナイフスイッチ切ってもらうことに。

4月からすったもんだしたかいがあったかどうかは知らないですが、

今回は自分の出番なし。素晴らしいです。

そうでなくてはね。

一通りあがったぽい。まだ、いろいろトラブルはあるが...

交通量測定

ようやっと、カメラになったのね

あのバイトはつらいよな〜

僕は割と

　　「別に常時見られてていいじゃん」

系なんで、ずーっと測定してればと思うかな。

車はカーナビで勝手に測定されてるので、人も携帯勝手に測定してよいよ。

その情報を使って悪事を働く人はきつく罰するよりも、利用された人が1億円もらるみたいな方がいいな。

歯医者さん

先週、ちょっとブリッジのところがあやしくて... 予約したら来週の木曜日、ってのが今日。

なんですが、土日結構痛んでな〜　でも、月曜日には、まぁ、収まった。

で、診断は「歯周病だけど、まぁ、神経は生きてるっぽいから、掃除と化膿止め」

まぁ、そんなことだろうと。まぁ、いきつけの医者は

　　積極的に治療するより、ちょっと薮の方がいいかな〜

黒猫

奥様が拾ってきた猫ですけどね。フーという名前なんだけど。

微妙に美人じゃないんだよな。猫なんてどれも同じ、特に黒猫はと思うわけだが...

でも、育ってきて少しデブになったので割とまともになってきたかも。

噛みくせがな。まぁ、噛まれないように注意すれば問題ないです。

おじいちゃん猫と喧嘩するのは相変わらず...

debugger の使い方

授業でやってたりするわけですが、

　　golang は dlv を使う

なんだけど、1.13は古すぎるとか生意気をおっしゃる。brew upgrade go

go は、なんか手元に全部ライブラリ持ってくるんだよな。

Rust はライブラリが深すぎる感じなんだが、go は

　　あっという間にアセンブラ出てくる

感じ。

ただ、最近は debugger 使わない疑惑もあってな〜 log で全部すませる?

Zoom でペアプロ

どっちかっていうと独り言いいながらのプログラミングを見物ってのが近いかも

授業でも、がんがんプログラミングしてみせるってのもやるわけですが...

今年は

　　golang だが、Rust / Java でも良い

的な感じで。ただ、

　　inteliJ も VSCode も golang / Rust のプロジェクトの初期化は苦手

ならしい。GOPATHがどうとか無理だよね。なので、自分もついうっかり

　　xterm から vim で編集して dlv debug

とかやってしまう。

まぁ、学習系は jupyter note でいいだろとは思いますけどね。

歩道橋

なんかながなが工事しててな〜　使えるのは明日からか。開通式でもやるのか?

バカは高い所に登りたがるので歩道橋は割と好きです。

その手前のマクドどスタバの所にも歩道橋作ってほしい。いや、反対側からポータルが届かないので。

この手の工事って歩く人やバス使う人のこと考えて工事してないのがな...

石嶺駅の橋は割と面白いかな。あと、経塚駅の墓地の橋はやっと通れるようになっていた。

Dune

あんまり期待してなかったんですけどね。予告編が us and them だったからな。でも、当然ですがピンクフロイドの音楽は出てきませんでした。

音楽割と良かったな。重々しくて。クラッシクでなくて。

忠臣蔵みたいなものなので、この映画を見るような人は話を全部知っているはずなわけですが...

再現度が高くて

　　中学生の時に最初に石森の表紙と挿絵で読んだときの感情が蘇る感じ

でした。話の詳細を思い出していく感じだな。そして、

　　オーニソプターが超格好良い

若王子と美人のお母さんの逃避行だからな〜　「おかあさんといっしょ」な話でもある。

説明しすぎでもなく、足りなくもなくと感じましたが、初見の人はどうかな。まぁ、そういう人は見ないんだろうなとは思いますけど。

フレーメンと合流するまでなのは予想通りだったんですが、後編は無事に撮影開始できるんだろうか。10年後とかだと困るんですけど。

男どもがかっこいい話でもある。

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

ぐるぐる

なんか、30mのループを音速で回して、ロケット飛ばすとかいう話が。時速8000km/hですか?

実験は1/5くらいだったらしいけど...

　　それって遠心力どうするの?

って計算してみたら、1000G くらいらしい。今回のでも200Gあるのか。

え、それどうするの? これでも軌道脱出速度には足りなくて、さらに加速する必要があるんですが、

　　構造物は無理でしょ、砲弾とかなら

でも、それでも、まぁ、物資運搬くらいには使えるか?

SFだといろんなスケールで作られてるんですけどね。60kmくらいのループにすれば10Gくらいになるかk

デジタルデバイド

WIDEのかなり初期の頃から議論されてて。ってことは、35年くらいか。

いろいろ、もう差がでてて

　　駅で定期券を買うのに並ぶ
　　バス停の時刻表を見る
　　マクドでカウンターに並ぶ

とか、もうデバイドされてる方なわけね。

授業でも「対面じゃなきゃ嫌だ」っていってる教師も学生もいるんだけど、それもデバイドされてる感じ。

動画の文化は、また別で

　　動画じゃなきゃいや

的なのもあるらしくて、動画強制な学校もあるらしい。僕は動画はいいかな、面倒だし。

でも、去年、VScode を読んだ時は、debug build を録画したのだった。

たまたま、間違えて録画してただけですけどね。

これから、どんな風になっていくのかな〜

建物工事中

なんの工事しているのか、実は知らなかったりするんですが。

おそらくは単なるメンテ。

　　1号館から総情センタへの道がブロックされてて

地味に困ってます。ingress 的に。まぁ、建物迂回すれば良いんだが。

古典的な「通り抜け禁止」だな。北口ローソンも微妙に迂回させられるんだよな。

　　いや、歩いてるのは琉大では自分だけな気もする

マイナンバーの怪しい機械

行きつけのお医者さんです。

　　置くといいことあるんですか?

と置いてみたが、何も起きず。保険証として使うのは

　　テスト中です

ってことらしい。マイナンバーカードのだめなところは

　　物理的なカード

だってのが一つある。アクセス手段の一つではあるけどね。さらに、

　　専用の機材を作る

ってのがださい。既存の医療用PCにカードリーダーでいいでしょ。

まぁ、最初の登録の時の謎な巨大装置とか、昔のSF映画に出てくる感じで嫌いではないです。

無意味に点滅するのとかつけて欲しい。

gitlab が...

update さぼってたら、やられてしまいました...

gitlab-ctl upgrade だと最新までは上がらないのだな。

新しい iPhone

かなり重いです。7+ からでも重いな。大したことないです。

顔認証がほとんど通らなくて、Quick Pay が全滅。

　　double click で Apple Pay の起動で顔認証通らないの確認してパスコード

ゴミすぎる...

VISA touch の方が楽。サンエーとかローソン/ファミマでは使えるが、吉野家と和風亭がだめ。

吉野家は VISA 自体拒否るので、Apple Pay 使ってたんですけどね。

あと、アプリの切り替えが良くわからん

　　原神は、お祈りしながら下をスワイプすると、たまに通る
　　Ingress は Glyph で必ず切り替えに入るので中断

なんか規則あるのかな。

あと、なぜか Battery の%表示がでない。7+では出るのに。右上からのスワイプで出るんですが、

　　%表示が指の下で、移動しても下のまま

そこまでして%見せたくないのか? なんで?

原神が快適なのと、アプリのupdateが速いのは良いね。Wifi更新したせいもあるか。

あと、何回か上げたが、写真が妙に明るい。

128Bのままにしましたが、

　　iCloud は最低限のbackupのみ1GB以下
　　iPhoneは写真はなるべく消してて 77GB (ほぼアプリ)
　　写真は Google Photos のみ

という構成です。

Google Photos が年内に引っかかる説があるんだよな。でも、削除でのりきるつもりです。

別に cloud けちるわけでもないが...

大学にある橋梁

これは模型じゃないよな。なんていうんだろうね。実物模型か。なんか矛盾した名前だな。

環境建築(学科じゃなくてコース)だからな。Ingress Portal ではありません。

登りませんでしたが、大学なので、こういう謎なものはたくさんあります。

ポータルもたくさんあるので、ぜひ寄ろう。ポケgoでもいいよ。

二分木の Hoare Logic

いつもの Agda で格闘中。なんか、実は

　割と簡単で、2018の方法でできていた

という落ちが。仕様の受け方が間違ってて、継続の入力で受ければ良いだけだった。

　test = next ( λ x → x ≡ c10 )

みたいに書くのではなくて、

　spec : (x : Nat) → x ≡ c10 → t
test = next spec

みたいに書けばよいだけだったらしい。

二分木の方は「これでできた」「だめだ」ループを20回くらい回ったんですが、

　どうも、結局、condition ではなくて、二分木に値が入っているという意味を表すデータ構造

つまり、表示的意味なデータ構造を書いてしまうのが良いらしい。そんなもんらしいです。

Ultra Garlic

なんか、twitter で見かけたので。ファミマですね。意外に大きいが...

　　奥様には不評でした

が、一袋は開けたらしい。もう一つあったので大学で学生と一緒に。

　　開けた瞬間がすごい

味は、まあ、そんなもんかな。

いろいろ、もと通り

それが良いかどうかはわからないけど、しばらくは。

12月になれば、いろいろ感染は増えてくるんでしょうけど、それまではな。

ワクチンが間に合わなかった人がいるのが残念だが、今からでも年末には間に合うな。

その後も、もう自粛には入らないんじゃないかな。感染したら「ワクチン打ちましたか」って聞かれるんだろうな。

もっとも、答えによって扱いが違うわけでもないんでしょうけど。

* * 1 */2

なんか、gitlabの証明書更新がどうのこうので、あぁ、それは

　　crontab中の起動は、PATHとか環境変数とかうるさいんだよ

で、なおしたんですが、1分後に設定するというデバッグ方法も。

11/1から動かなくなるという技が。

　　なんか gitlab-runner が再起動繰り返してるんですが...

で、気がついたんだが、

　　* * 1 */2

確かに、1日から毎分起動するよな。確かに、Zoom で、アスタリスクって言ったような気がする〜

なにやってんだかな〜

　　17 35 1 */2

とかで、お願いします。

gitlabも podman にしてしまうという技も可能らしい。

花火

iPhone 13 Pro Max ですが、妙に明るく写るんだよな。手持ちでも、もう少しちゃんと撮れるだろとも思うけど...

　　Ingress 優先で

大きな画面で twitter できるし、やっとできた原神もさくさくだし。

でも、7+ に比べると、かなり重い。face id がバカすぎる。アプリ切り替えも「お祈りしながらスワイプする感じ」 電池の%表示がだめ。

ま、7+の電池がもう3時間もたない感じだったので、それで比べれば天国です。

Hoare Logic

割と昔からの技術でさ、2018年にもやったんだけど、なんかいまいちで。

木下先生がAgdaで書いたのも動かしたんですが、割と煩雑な割に停止性とか怪しくて...

Agda は loop の停止性が自明でないと文句言うのだが、それをループの回数でなんとかするという方式らしい。

なのだが、夢で「型じゃなくて、値つまり、証明その物を渡せばいいんじゃないか?」ってのが降ってきて。

ところが実際に書いてみると「あれ、ちゃんと値が回ってきてるじゃん」

　　proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
　　proof1 = refl

今までは、こんな風にしてたんだな。それだと、自分で値を作らないとだめ。だから refl なわけ。

　　whileTestSpec1 : (c10 : ℕ) →　(e1 : Env ) → vari e1 ≡ c10 → ⊤
　　whileTestSpec1 _ _ x = tt

そうじゃなくて、こういう風に入力で仕様を受けてやればよい。実際、PostCondtion は証明が渡されてるからこれでよい。

ということなので、2018年の時点で十分だったということで終わり。え、何もしないの。

なんだが、停止性も「自然数の減少列に写像する」という当たり前の方法が使える。当然のように、Agdaで高階論理で記述できる。

TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set )
　 → (ExitCond : Index → Set) → ( reduce : Index → ℕ)
　 → (loop : (r : Index)　→ Invraiant r → (next : (r1 : Index)　→ Invraiant r1 → reduce r1 < reduce r　→ t ) → (exit : (re : Index) → ExitCond re → t) → t)
　 → (r : Index) → (p : Invraiant r)　→ (exit : (re : Index) → ExitCond re → t)　→ t

まぁ、なんのこっちゃかんもあるが。

Hoare Logic だと、プログラムをコマンドに分解したりとかの手間もあるのだが、こっちの方がプログラムに埋め込める分、簡単ならしい。

続きは、プロシンかな。　

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestGears.agda