ばってん

なんか手足にばってんが付けられてる

なんですかって聞いたんですが、血管がどうこうとか

ZF on agda rewriting

Agda を {-# OPTIONS --cubical-compatible --safe #-} に書き換える作業なわけですが、

Red Black Tree 片付いたので、ZFの方をなおしているところ

引っかかるのは、functional-extentionality とか、非構成的な仮定を module の引数にするとかそんなの

あと、微妙に unification 関係に差がでるらしい。どれくらいの意味があるのかは実はよくわからない

割と順調だが、残りの4つが割と大物でな。Zorn と Topology と Tychonoff か

まぁ、復習になってよい説はある

これが終わったら、たぶん、Category 側もやります

　＊　＊　＊

病院から戻ってきたら、夜、なんか熱出したので、少しお休み

風邪かと思ったら、今日には熱は引いてたんだが、まぁ、休んだ方がいいだろう

いつもの「休日ダウン」パターンだな

除細動

浦添総合病院で、やっと除細動してもらって少し復活

別に先週やってくれても良かったんじゃないか説。なんだが心エコー取らないとダメとかで

そんなわけで、この一週間は割と調子はよくなかった。先生にはそういったんだけどな

除細動、体験してみたいから麻酔なしでいいですって言ったんだが「痛いですよ」と許してもらえず

その瞬間は覚えてないです。つうか麻酔が聞いてる時になんか説明されたらしいんだが覚えてるわけないだろ...

「その辺のAEDでも良いんじゃないですか?」と聞いたら、「心停止じゃないから起動しないんじゃないかな」

ってな話でした

まだ、検査は続くらしい

git submodule commit number

前にもくらったんだが

　　% git submodule update --init --recursive　

　　Submodule 'themes/ie-hugo-theme' (https://gitlab.... egistered for path 'themes/ie-hugo-theme'
　　Cloning into 'themes/ie-hugo-theme'...
　　fatal: remote error: upload-pack: not our ref 76bbd95e5f23e6dfc17578c06fd45c697246069d
　　fatal: Fetched in submodule path 'themes/ie-hugo-theme', but it did not contain 76bbd95e5f23e6dfc17578c06fd45c697246069d. Direct fetching of that commit failed.
　　fatal:

実際、submoduleの repository には 76bbのcommitはないわけ

cache とかがあるらしいけど、 main と sub をゼロから clone してもなおらない。この 76bb がどこに書いてあるのかも不明

こんなこともあろうかと、

　git submodule sync
　git submodule update --init --recursive
　git commit -a
　git push

と手順が README.md に書いてあるんだが、役立たず

76bb がどこから出てくるのかが謎すぎる

しらばく、格闘してたんですが、めんどくさくなって giti submoulde deinit して、消して、そのまま add して解決

Wordle 300

いや、すでに306なんですけどね

ま、時間の問題だとは思うが順調です

最初の4つは決め打ち。4つ目は少し工夫するくらい

二つ目三つ目で当てにいって後悔することは多い

ってなわけなので、5つ目に当てにいくわけですが

　そこで、変な単語が通ると危ない

Well Founded

定礎性とかいうんですけどね。超限帰納法は、不等号関係列に必ず起点があれば使えるってやつ

　　<-TransFinite : {ψ : HOD → Set n}
　　　　 → WellFounded _<_
　　　　 → ({x : HOD} → ({y : HOD} → y < x → ψ y) → ψ x ) → (x : HOD) → ψ x
　　<-TransFinite {ψ} wfa ind x = induction x (wfa x) where
　　　　 induction : (x : HOD) → Acc _<_ x → ψ x
　　　　 induction x (acc rs) = ind {x} (λ {y} y<x → induction y (rs y y<x) )

という風に使うんだが、肝心の WellFounded _<_ の作り方がわからない

　　ordWF : WellFounded _o<_
　　ordWF = ?

とか作っていくんだが。調査中

元は 1984 の論文か...


Constructing Recursion Operators in Intuitionistic Type Theory" by Lawrence C Paulson.

プラザハウスで絵画観賞

知り合いの人の絵の個展をのぞいてきました

とくにそういう趣味があるわけではないけど

イメージが膨らむ感じの絵だな

この手のものは、伝わるというよりは自分の心の中にあるものを

見つけきっかけみたいなものかも

(まちがえてコリンザの方にいったのはなんでだ)

ZIQUCO絵画展 〜6/27

https://plazahouse.net/news/post/16882

深いポケット

iPhone 13PM なので、でかい

それにあわせて上着のポケットとかワイシャツのポケットを深くしてもらってます

まぁ、調子いいかな

全部ってわけにはいかんが

不整脈

ここ数か月調子悪くて、行きつけのところで心電図とってもらったら心房細動だそうで、浦添総合病院にいってきました

中略。治すつもりなら一年禁酒しろとか言われましたが、まぁ、そうかも

　　飲み過ぎ　→　無呼吸　→　不整脈

みたいな流れらしい。スナックのママさんたちとかもやられてるらしい

1,2月、風邪であんまり飲めなかったので、調子に乗って飲んでたからな

確かに酒抜くと少し調子良かった気もする

クニンダのランチ

国際通り、県庁前よりのクニンダなんですが、今日、スーツを取りにきたついでによったら

　　なんと、500円ランチ (第三木曜のみ)

おいおい。

　　そもそも、お店が目立たない
　　開いてるかどうかもよくわからん
　　入ろうとすると、沖縄料理3,500円
　　カウンター中心で、個室は一つだけ

なんか、根本的に間違っている気がする。旅行社と提携とかもうないのかな

料理は、3,500円の価値はあるとは思うんだが...

汗かき

大学にいくだけで汗だく

で、教官室で着替える

帰ってきて、シャワーを浴びて着替える

というわけで、洗い物がたくさん

たいして歩いてるわけでもないんだが

RedBlackTree はできました

たぶん、詳細はプロシンで話すんじゃないかな

やっぱり、学生には無理だったか的な。3月から6月までかかった

他にもいろいろやりたい気もするが、これはここまでかな

4つのケース(grand parent/parent)のパターンがそここに出てくるのだが、
微妙に統一的に扱えない

かといって、github copilot の精度も低くて

でも、時間かかったのは実はそこじゃないってのが面白いところかも

Ingress Anormaly Goods

いや、さぼったんですけどね。登録はしてたので、もらえました
>ありがとうございます

緑と青で人数差があったらしく、なかなか

まぁ、いつものことか

でも、けっこう、凝ってる。いいな

Niantic 的には、Ingress はすでにおまけかな

再開するかどうかは、気分次第かな。やっぱり、歩く量は減ってるので

少し考えないと

足 Apple Watch

やっぱり、腕は邪魔でな。単に心拍見たいだけなので

割と調子良い

振動で壊れそうだが

琉大のバス利用者

例年今ごろはバス使う人は、ほとんどいなくなるんですが、

なぜか、今年は、まだ使う人が結構いる

不思議な感じ

「うちはご飯屋さんじゃありません」

「酒の飲まない人は帰れ!」

ママさんが、にっこにこで、そんなこというお店です

ノンアルでも良いらしい

相変わらず、いろんな食べもの出してくれるな

なんか、学園通りの庵は30周年とか。来年?!

算数の教科書のかけ算

まぁ、議論するならよんどけよ、くらいです

(ひとつ分)x(いくつ分)
同じ数ずつのものを足し合わせて、全体の数をえる

ですね。最初が構文の定義、その意味を日本語で説明するという一階述語論理の
標準的な定義の方法にそってます

まさ累加なんですが、包含除というものらしい。同じかずずつのもので割り切れるみたいなもの

同じ数ずつに分割して、総合するという分析総合的な考え方ですね

絵が具体的なものなのは、小2は、そういう理解の段階だかららしい。人によって違うとは思いますけど
'
掛順問題は、この絵の中からかけ算を探し出して、式を書くというもの。直後にあります

なので、掛順問題は主に定義の確認だとわかる

この「同じ数ずつの集まり」を無視しする人が多いんですが、絵の中には同じ数でないものも混じってる

異なるものが混じっているとかけ算ではないということらしい

この定義を書き写す問題もあります

このあと、この定義にしたがって計算して、教科書の九九表を埋めていきます

最後に、交換則を観察して小2は終わり。二桁のかけ算は、その先。ゆっくり学びます

教科書自体は公共図書館で見れますが、最新ではないらしい。学校図書の平成31年版です

先生によっては、この順序を6年まで使うらしい。まぁ、途中でやめるのは変だものな

　

最近のコタ

どうも過剰グルーミングらしく。こんなことに

でも、少しは収まっている感じ

月を詠むとソウエイシャ

月を詠むは、普天間のカレー屋さん。営業日が週の前半なのでなかなか

でも、どうも嘉数でソウエイシャという茶店をやってたらしい。あぁ、コロナの直前の2020/10にいった写真がある

あれから、紆余曲折あったな〜

魔女の一撃は、まぁ、少し痛いけど

　　歩きながら治す

方針です

魔女の一撃

なんか、朝、シャワー浴びててたら、いきなり

なんだよ〜　靴下たってはけないんですが

まぁ、歩くのには問題ない。危ない感じはあるが

トイレの手洗いが辛いんですが

ま、
　「そろそろ、ほどほどにしておけ」
って感じですかね

少し良くなってる感じがする

Red Black Tree

普通のバランス木ですね。これを

GaersAgda という CbC に対応したAgda の一種の手続き型言語で書く

で、それを Hoare Logic 的な方法で証明していく

なんですが、割と難航してて。去年は学生と一緒にやったんだけど、

　Invariant とFind

ぐらいまででな。その後のバランスさせながら上にあがるってのが面白いんだが

バランスさせるのは case1 から case6 まであるんだが、なんか case5まで到達

思ったより複雑なんですが、たぶん、今年のプロシンのネタにすると思います

削除の方も同じ Invariant 使えれば、まぁ

それで、こいつを CbC にコンパイルできるはずなんだが

消滅都市ライブ中継

10年も前のソシャゲですけどね。ソシャゲバブルの頃か

今年の2月にサービス終了だったんですが、このゲームは音ゲーではなく、アクション系なんだが

　音楽が良い

サ終したゲームのライブとかやるか? って気もするが、まぁ、根強いファンはいるってことか

90分楽しかったです

Sound track だとちょっと足りないかなぁ

でも、一応、オフライン版のアプリは公開されたので、音はきけます

曲目リストどこだ?!

https://x.com/noisycroak/status/1796832645701414976