Lean 4

Agda と同じ定理証明系なんですが、少し触ってみようかと

VSCode で入れるらしいが、入るけど

　　なに入力すればいいの?

まぁ、ChatGTPに聞けばいいか。#eval 1 + 2 とかするらしい

import First.Basic

#eval 1 + 2

def square (x : Nat) : Nat :=
x * x

#eval square 4

theorem hello1 : 1 + 1 = 2 := by
decide


コマンドラインからできるんだろと思ったが、なんか、動かない

+leo+kono ~/.elan/bin/lean First.lean
First.lean:3:0: error: unknown module prefix 'First'
No directory 'First' or file 'First.olean' in the search path entries:


build は動く

+leo+kono ~/.elan/bin/lake build -v First.lean
ℹ [2/3] Replayed First.Basic
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First/Basic.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.setup.json --json
ℹ [3/3] Replayed First
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First.setup.json --json
info: First.lean:5:0: 3
info: First.lean:10:0: 16
Build completed successfully (3 jobs).

なんか、結構、えげつない呼び出しだな

まぁ、動いたみたい。

一旦、C に変換するの? 微妙だな

agda みたいに「全部、Haskell でがんばる」ってのがいいかどうかは、また別だけどね

Restrant Lily

沢岻の少し奥にあるレストラン

経塚のサンエーから、あるいて330までいく途中で見かけました

行ってみたい気もする

崖崩れする前にいった方がよいか?

歯医者

なんか、詰め物がとれてしまって。といっても、11/20くらいでさ

「年末で混んでて」で、今頃に。来週には予約してたのに

まぁ、そこまで延ばすのも良くない。でも、いったら

　「2年前にも取れてる。少し強力な接着剤使うか」

う、うーん、ま、まぁ、そんなものかな?

まぁ、すぐに終わりました

時の庭2

なんか、前に閉めてた時の庭、普天間のカフェ、ラーメン金川のそばですが、店主が変わって復活してました

前と違って、食べ物がたくさんある。それは良い

でも、ボロネーゼに生卵のせるのはやめて

Wifi も電源もそのままなので、使いやすい。長続きすると良いんですけど

OSC Okinawa 2025

Sakuraのいつもの場所で。なんか、

　00年代と参加者が変わってない感じ

でも、そのまま人は歳くってる感じね

シス管の琉大生が一人。高校生がブース持ってたな

さむい〜

沖縄、20度きるとかなり寒くて

チョッキを出してもらいました

　「このソファをちょっとどけて出せるところにあります」

いや、それ無理だから…

図南の翼

なんとなく読み返してしまう本

十二国記の一冊だけど、珠晶が12歳で、王を目指して登極する話ね

NHKのアニメではやらなかった

話に無理がないわけではない。というか無理の塊

でも、なんか読み返したくなる

玉泉洞

本土からお客さんとしか来ないわけですが

なんか、年何ミリとか成長するらしく

床が既に鍾乳石化してる

入ったのは20年ぶり? 900m は結構長い

そして、その後のお土産公園が長い

鍾乳石の先が白くなってる。ここ20年分の成分の変化かな。二酸化炭素で白くなるのかな?

Okica はわかりました

Okica のポイントのサイトを見たら、

　月4万円で20%還元

になってる。あぁ、それだと1万円還元はあるな

いったい、いつ、1%から変更になったのか?

Prince concert on IMAX

なんか、ふっと調べたら、浦添パルコで11/20まで。一週間だけか。まあ、80年代だろ? おじいちゃんおばあちゃん用?

仕方ないなで観に行ったんですが

　Led Zeppelinの時の只券は使えない

え〜 しかも、特別上映で3千円。見てるのは、3人

いいけどさ。Prince って、まぁ、お祭りバンドなんだよな。なので楽しかったです。シーラE が良い

なんだが

　　一曲も知ってる曲がなかった

どういうことなんですかね。聞いてたのは90年くらいのはずなんだが、このコンサートは1987なんだよな

なんとなく、Electric Miles っぽい

Prince はヒゲが嫌いな人は多いかも?! 没後10年?!

https://towapictures.co.jp/prince_sign-o-the-times/

月と龍

大平のラミロワールの向かいにあると聞いたのでいってみました。 2022にオープンしたらく。

お昼にいったが作りが料亭。断られるかと思ったが入れて

　お昼は、2,600円からの魚の御前

あぁ、まぁ、やられた感じはあるが、そんなものか

個室に案内してくれたんですが、明かりが

　まるで事務室

な蛍光灯で、ちょっと料理が可哀想な感じ。魚はカンパチですが、まぁ、おいしかったです

値段相応

新しい nvim-agda

まぁ、動いてはいるんですけどね

なんか、知らんけど

　引数がずれる

goal 表示する時に、隣のを表示してしまうんだな。まぁ、害はない

前に使っていたのは「sub windowが出て表示する方式」だったんだが、こっちは「Windowを割って表示する」

まぁ、どっちでも。あと、term が表示が少し変。まあ、それも害はない

自分で作って使うと「そういうの気にならない」ところがあってさ、まぁ、そうなんでしょう

正気な人は VSCode を使っているんだろうとは思うんだけど

Lean は VSCode only らしい

自分の手元のを Lean に書き換えようって気もなくはないんですけどね

https://github.com/isovector/cornelis.git

首里城再建

なんか、もう儀保駅から見える -

公園の修理

330愛知のまつぼっくり公園の裏の通り、元浦添総合病院のところの330の上の通り

だいぶ前の台風でやられて閉鎖されてたんですが、最近、修理完了してるのを発見しました

地味に便利。Ingress にね

月を詠むのカレー

最近、通っているかも

昔は嘉数のソウエイシャっていう茶店をやってたらしい。短かったけどね

このカレーは南インド風? メニューが

　このカレープレートと、コーヒーとチャイ

くらいしかない。潔い。どうせ、いつも同じもの頼むので、それでよい

https://www.instagram.com/tsukiwo_yomu/

原神の紙芝居

月の関連のストーリーをやってるんだが

　途中で寝落ちすると、かなり前まで戻される

　わけわからん双六みたいなモード

ちょっとひどすぎない?

わざとか? まぁ、そろそろゲーム的に寿命なような気はする

かけ算の話 5m/s x 2kg =2m/s x 5kg

もともとの掛順は

(一つの皿に飴5つ分)x(皿2つ分) 5x2
(一つの皿に飴2つ分)x(皿5つ分) 2x5

で、「どっちでもいいだろ」だったはずだ。「だから、一つ分の差だろ」ってわけね

運動量の自然な累加の交換則

　5m/s x 2kg =2m/s x 5kg

は、
　2kg = (基準の量 1kg ひとつ分) x (2つ分) で2倍 　5m/s x 2kg = 5kg m/s x 2
　5kg = (基準の量 1kg ひとつ分) x (5つ分) で5倍 　2m/s x 5kg = 2kg m/s x 5

で、皿と飴の掛順と、まったく同じ構造を持ってる

　5m/s x 2kg =2m/s x 5kg の左右は2kgと5kgの差がある。これが掛順

この動かぬ掛順の証拠を「見ないふりして」話をそらすだけなのが反順序ならしい

結局、これだけで掛順の説明としては十分ならしい

「順序じゃなくて単位を無視するな。 5m/s x 2kg =2kg x 5m/s だから掛順はない!」

という反順序もいるんだが「まったく関係ない式」だよね? これは

　交換しない交換則
　「a x b = b x a の両辺は、aをb回足す」
というトンデモらしい。かけ算は「a x b はaをb回足す」という意味なのだから、交換しない交換則は
一階述語論理に対する反則みたいなものだ。もともと、そういう曖昧さを避けるために記号論理が開発されてるわけね

正しくは
　「a x b = b x a は、aをb回足すのと、bをa回足すのと値は等しい」
というわけ。これが掛順の説明にもなっている

まぁ、掛順を理解してるなら「かけ算の順序はどっちでもいい」のだが

　「かけ算に定義はない」
　「教科書のかけ算は定義ではない」
　「かけ算は累加ではない」
　「(ひとつ分)x(いくつ分)と(いくつ分)x(ひとつ分)の両方がある」
　交換しない交換則「PV=VPだから掛順はない」

これらは単なるトンデモ。教科書を読んで勉強しなおそう。今からでも遅くはないよ

https://x.com/shinji_kono/status/1895764620629197140

色褪せたポスト

沖縄の日差しだからな

昔の丸いのも嫌いでないけど、さっさとこれになってた

年金関連の書類が郵便なんだよな

まぁ、物理的所在を見たいのかもしれないけど、もっとましな方法あるだろとも思う

Neovim package manager

Lazy での設定は、ほぼ終わって、agda も動くようになったんですが、

　vim.pack.add()

ってのが次期 package manager になるってな話が

せっかくだから、試してみるか? なんだが、

　pack is nil

ってなんだ? 0.11 ではまだ入ってないらしい

　 NVIM v0.12.0-dev-1569+g16c8152229-Homebrew　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
で、試すと動く。なのだが、

　　"neovimhaskell/nvim-hs.vim" ,
　　"isovector/cornelis",

は、対応してない。これらは Haskell base だから。あっそ

まぁ、Lazy でいいか

nvim update の続き

.vimrc を init.lua に書き換えるだけだが、

^M ではなく <CR> と書くのか

vim.cmd とか vim.opt とか書けば良いだけ

package management には lazy ってのを使う

~/.config/nvim/init.lua
~/.local/share/nvim/lazy/

置き場所がよくわかんないんだが、まぁ、動いているらしい

設定は config に書いて、package は local にいく感じ? lazy が面倒見てくれるらしい

githun copilot も lazy 経由で

と思ったら、node.js が古いだと? v21 で、今は v25 か

次は autoload を書かないと

問題は、新しい agda vim UI が、微妙なところ

今ままで使ってるのは、若干、バグがあるんだが、自分でなおすのは既にめんどくさい

長い物に巻かれるのは嫌いじゃないんだが

homebrew updgrade

AgdaのSheafの方もだいぶ進んで、って

　まだやってるのかよ

て感じなんですけどね。でも随伴函手のηとεの定義まではできた

ところが、εの定義を接続すると Agda が止まらない。なので、

　そろそろ version up するか

と brew upgrade するわけだな

で、まぁ、いろいろ trouble が

　Perl/Tk の build に失敗する。って、ソースは5年前?!

他のものを探すと、Prima ってのがあるらしい。それは Aqua もあるらしいが、install してみたら

　X11 base

まぁ、それなら、Perl/Tkか。JPEG/jpeg を見直すと、system のlibjpegを使う設定の認識にしくってたのでそれでなおりました

ChatGPTがこの辺には便利

でも、agdaの方は

/Users/kono/src/CategoryExercise/src/@@HOMEBREW_CELLAR@@/ghc/9.12.2/lib/ghc-9.12.2/bin/./ghc-9.12.2: No such file or directory /opt/homebrew/bin/ghc: line 10: exec:

なんだこれ? 要するに、テンプレートからの生成に失敗しているらしい

結局、brew uninstall ghc ; brew insatall ghc で解決

ところが、nvim のplugin がトラブる。まぁ、予想はしてたんだが。ついでに

　　新しい plug in 試してみるか

で、https://github.com/agda/cornelis これを見るんだが

　　neovim では、init.lua で初期化するのが普通

って、いつからだよ。まぁ、neovim 使うってのは、そういうことだから、仕方ない

というわけで、emacs で止まらないことは確認したが、nvim では、まだ、動いてません

落書き

しちゃいけないところに書くから面白いわけで「落書きするな」では効果がない

割と良く見るサインの意味はなんだろ?

トロピカルビーチの工事

白ポになってなので、埋めにいったら、なんか作ってました

　劇場?!

まぁ、とめないけどさ

経塚サンエーから見える

なんか、大きなビル

Google map で調べると、東急ホテル跡にできた大浜病院らしい

いや、そんなところから見えるのかってのが面白いんだが、下り坂ね

28のバス

今日はラグナガーデンでMBP広げてたんですが、

　28番のバスで帰ろう

と思ったら「次は浦添パルコ」、途中のバス停はなし

浦添パルコで降りると次のバスは2時間後。結局、安謝橋まで迂回

いや、ラウンドワンでおろしてくれよ〜　バスのアプリで見て間違えてるのでしかたないんだが

まぁ、ingress できてよい説はあったけどさ

38でのライブ Brian Hooper

おじいちゃんのライブですけどね

年齢が近いからなぁ　自分のカラオケで歌う唄と重なってる、BeatlesとかEWFとか

まぁ、楽しかったかな

何曲かオリジナルも入ってて、「あの頃の」ポピュラーソング的な感じが良かったかな

ローランドで働いていた人なのね。でも日本の会社だが?! SC55MkII まだ使ってるんだよな

そういえば、最近、はまってるカラオケは、Prince の1999。Electric Light OrchestraのTwilight だが、そういうのはなかったです

Okica point

なんか、ゆいレールで見てみたら

　10,000 point

え? なんで、そんなに? 1%だろ? 100万円乗ったってこと?! ありえんのだが

ハリーズのカレー

先代のおばちゃんの味そのもの

でも、値段は750円から1750円に

学生と一緒にテイクアウトしてたのが既に懐かしい

iPhone 17PM

いや、iPhone 13PMと、驚くほど差がない

まぁ、逆に調子が良いという言い方もあるかな

横にボタンが増えているんですが、まったく使わず

丸いデザインも、すぐになれた

画面の保護フィルムも調子良いです

容量倍256GBで、写真は削りまくったので、余裕

slient mode のボタンがスライドではなくなったのか

USB-C も調子良い

まぁ、また、長く使いたいものだ

SLAM DUNK の映画は

沖縄出身の宮城リョウタの話だったのね

いや、まったく漫画の方は読んでなくて。最初の試合の部分のたるさでめげそうになりましたが

まぁ、面白かったかな?

2022から、毎年、再上映しているので、観にいこうかと思っただけです

浦添パルコの割と小さい部屋での上映だった

スポーツは自分が苦手たったのもあって、あんまりみない

バスでオバーが

なんか、「ここどこ?」とかいってる。110で沖国側がだからな

1万円チャージは太っ腹だが「オバー、どこへいくの?」っ聞いたら

　知花

え〜? それ、反対向きですが。周りがざわざわするんだが

　佐真下のサンエー

あぁ、それは、近くは通るけど。といっても、第二佐真下から歩くのか? ま、いいか

まぁ、がんばれ

浦添運動公園

なんか、作っているっぽい      

北前から北谷

バス停の話。 ちょうど、その真ん中にスタバがある。たまに使うんですが、

＊　58号線を北前から北谷まで歩くと、基地側がジャングル

という問題が。いや、ほとんど人は見かけないんですけどね。正気なら、基地側は歩かないだろ

ところが、北谷の上りのバス停は、もちろん基地側にある。そして、

＊　横断歩道がない。歩道橋もない

どういうこと?! そもそも、間にバス停あっても良くないか?

Apple Watch

新しいのに同期しなくて。「まぁ、リセットだろ?」とは思ったんだけど、どうも

　　古いのから同期を外さないとだめ

だったらしい。でも、かながリセットしてくれたので同期は終了

まぁ、古い Apple Watch で、脈拍だけでいいかとは思ってるんですけどね

MNRV2J/A watchOS 6.3

かぁ

iPhone コースター

いや、iPhone 17 、かなり、出っ張っててさ

そのまま置かないでコースターにのせるとよいらしい

まぁ、別に曲がりはなしないんだが

iPhone 7 でも少し出っ張ってるが、17は、半端ない

ワクチン

コロナとインフルエンザと打ってきました。補助がでるなら打つよな

なんか、コロナは新型ワクチンらしい 「ヌバキソビッド」なんだ、その名前は…

なんか、効果が少し長いらしいです

靴はだいぶなれてきたが、まだ、少し痛い

ほうせんか

北谷に寄ったら、セブンプレックスでやってたアニメ映画です

終身刑のやくざ者が、ほうせんかと話して大逆転の夢を見る的な話

まぁ、悪くはなかったんだが、他人に勧められるようなものかというと微妙な感じ

でも、暇なおじいちゃんが見るには良いかも

話の詰めがあまい感じで、それは話があわないだろ的なところが結構ある

一方で、「男はそんなものだろ」的な共感はあるかな

　いわなきゃ伝わらないだろ

的な話でもある

大逆転の比喩に使うのがオセロ。うーん、それも微妙すぎる

https://www.pics.tokyo/works/housenka/

新しい靴

といっても頼んできたのは、だいぶ前

いつものジビキ製靴なんですけどね。なんか、痛い。いつものことなので、しらばく履いてれば

と思ったが、足の甲が痛いな。まぁ、だいぶ収まったか?

8番出口

東京にいった時にみた映画

まぁ、Twitterで話題にはなってたし

ホラーやスプラッタは嫌いなんだが、まぁ、それほどでもなく

いやさ「ゲームでやられて、そんなにくやしがるか?」ってのはあるよね

実はゲームだろ? だが、クリアできない的なところが面白いわけだが…

映画として面白かったかといわれると、まぁ、佳作な感じ?

まぁ、ネタないから書いた的な話

iPhone 17PM 移行

やっときたので。まず

＊　画面保護シールから

なんか、カナが「間違えて買った16PM用の保護シール」があるらしく、貼ってもらえました

13PMの時はなくていいかと思ってたんだが、意外に傷がつく。保護コーティングも無力。なので、シールにすると決めてた

次は

＊　esim への移行

Webからで問題なく、申し込めて、1時間もかからずにメールがきて、QRコードで設定

＊ Wifi がつながらない

どういうこと? Guest用にはつながる

旧iPhoneからの同期がすんで、アプリのダウンロードの段階でスタック

＊ Wifi がつながらないが再発

結局

＊ 再起動で Wifi につながる

アプリのダウンロードは終了

なんだが、IIJ mio / au の回線がつながらない

＊ iijmioのアプリから SIM Profileをdown load。そして、iPhoneのGenral / VPN から install

がいるのか。 そこまで通ったら

＊ LINEのアカウントもQR Code 経由で移行できました

あと使ってるのは、原神と Ingress くらいで、それは、得に問題なく移行できました

そういえば、iCouid が、また写真バックアップが入ってて一杯。これは写真バックアップを削除で終わり

iPhone 7 から13への移行では、結構、やらかしてたからな

肝心の 17PMの使い勝手? これからね

鬼滅 無限城編

いや、観たのは、ずいぶん前なんだけど、blog に書くのを忘れてたみたいで

　どうせ、アニメの予告編みたいな感じでしょ

だと思ってたんですが、 割とがっつり入ってて

「考えるんだ」とかいってるわりには、たいした考えもなく話は進むってな感じでした

まぁ、まだまだ、続くわけだけど

レゼ編みたいなあとをひく感じではないのはよい。まぁ、それも悪くはないんだが

https://kimetsu.com/anime/mugenjyohen_movie/

iPad 更新

家にあるのは、2018の32GBと、2013の16GB

さすがに、iOSが16GB近くとるようになっているらしく、256GBの最新のを買うことに

ネットの情報だけだから容量は最小で良いと思ってたんだが、256GBは必要な感じね

昔のは、もたなかったが、今のは長く使える。それは素晴らしい

Kindleだけなら、2103の16GBでもいけるんだけど「消しながら使う」感じになってしまう

チェインソーマン レゼ編

なんか、ちょっと話題になっていたので。いや、あんまり観たいと思わなかった

そもそも、スプラッタとかホラーとか、そんな好きじゃないし

で、まぁ、総集編から始めたんですが

　　テンポが遅い
　　悪魔のやられる条件が不明
　　なんのために戦ってるの?

そして、致命的なのが

　　主人公はバカ設定

まともそうなのが出てくると「全員殺される」。困ったもんだな

でも、まぁ、なんんとか見終わって(3時間なので短い)、レゼ編へ

いや、まぁ、面白かったかな? なんか、

　　映画館は若い女の子でいっぱい

だったし

7年目のビスケット

なんか、会社のが賞味期限にひっかかって放出

って、7年持つって書いてあるんだが

7年前のもの?!

Led Zeppelin

Becoming ですが、観てきました。が、

　　3,000円、シニア割引なし

え、60年代のバンドの話を IMAX とはいえ、その値段? おじいちゃんおばあちゃんしか観にこないんだろ?

実際、がらがら。20人いなかった?

と思ったら、9/26からなのに10/2終了。いや、セブンプレックス側では、もう少し長くやるはずだが

なんだが、映画の前の予告の映像が出ない。「IMAXだからじゃない」? え、そうなの

と思ったら「上映しなおします」のアナウンスが。おいおい。と思ったら、いきなり本編の始まり

子供の頃からの話と、影響を受けたミュージシャン、そして、ヤードバーズから、Led Zeppelin

で、II までの話なわけね。ジミーページとロバートプラントが

　「あの頃は良かったよな〜」

と、笑顔見せる。というようなお話。もっとも、Led Zeppelin は、その後、いろいろ不幸があったし

まぁ、でも IV、Phisical Graffiti、Presence までは素晴らしかった。IIまでの、Led Zeppelinの成功話ね

ジミーページの若くて、自信に満ちた笑顔が良かった

僕は IV が出て天国への階段が出てから知ったわけだけど、あの頃のAtlantic のアルバムが面白かった時代を
再発見できる感じね

なんだが、途中で

　　字幕のピントや映像が乱れるっていう上映事故が...

お詫びのチケット2枚。だがIMAXには追加料金? Led Zeppelin もう一度はないかな

https://zep-movie.com

Sheaf

まだ、やってるんですが、

Γ : Functor ( top / X ) (HOD-OSCA (topology X) )

は、できたので反対側

L : Functor (HOD-OSCA (topology X) ) ( top / X )

をやってるんだが、位相空間を作らないといけない

それは関数の定義域の制限のFunctorの同値類でみたいな話

有限な ∩ と和集合ができればよいんだが、難航してたんだが

　　Functorだけでなく、その元になる関数に well defined な仮定がある

らしく、

　 FO-wld : (F : Functor OX HODSets) → Set (suc (suc n))
　 FO-wld F =　{a b c d : Obj OX}
　　　 → (b⊆a : SObj.s b ⊆ SObj.s a)　→ (d⊆c : SObj.s d ⊆ SObj.s c)
　　　 → {x y : Ordinal} → (ax : odef (FObj F a) x)　→ (cx : odef (FObj F c) y) → x ≡ y
　　　 → Func.func (FMap F {a} {b} b⊆a ) ax ≡ Func.func (FMap F {c} {d} d⊆c ) cx

の仮定を入れるとできるっぽい。でも、有限な ∩ の4つの方向の一つができただけなので、まだ、先が長い

でも、「なにやってるのか」を人に説明するのは無理っぽいので、プロシンには出さないつもりです

TEAVANA

スタバのお茶バージョン。ライカムのスタバがもう一軒ってわけで、寄ってみました

いつも頼んでる「English Breakfast, Non syrup」は、なさそう。メニューにはない。TEAVANAなのに

コヒーは一通りあるらしいんだが

アールグレイがあるので、それにしたんだけど「シロップ抜きにはできない」ん〜?

で、アイスが出てきて「沖縄はだまってればアイス」なのを思い出しました。ホットもあるらしい

もしかすると、English Breakfastもあるかも?! いや、まあ、もう少し探してみるか

いや、元の店にいけば良いだけではあるんだけど

蜘蛛

普天間基地の入り口あたり

気がついて、ちゃんと避けました

タンブラー

ずーっと昔に使っているのを引っ張り出してみました

最近のスタバは、洗ってくれないのか

カバンに入れるには大きいんだが、カバンの肩掛けベルトにつけるのも微妙

箸

東京にいった時に、かじってしまった箸の代わりをさがしてきました

「これよりも、長い箸が欲しいんだけど」
「あぁ、シンプルなのがいいのね。これは1600円」

まぁ、黒檀のとかも見たんだけど

　　1600円

には、負けました。それでいいや

スタバのチケット

なんか、1300くらい貯まってて、放っておいたら

　　期限が切れるから使え

という指令が。まぁ、一回分くらいだろと思ってたら、

　　500円分が130 stars

え、そんなに貯まってるわけ? 使うのが面倒くさい

Excelsior のコンセント

なんか書いてあるので、使うなって書いてあるのかと思ったら

　2時間まで

だった

スタバもコンセントは限られてる。長居する人もいるからなぁ

また、腰が

東京から戻ってくる途中は、地下鉄の階段が結構あって。CPAP持ち歩いているので

　ギクっと

まぁ、ちょっと痛いくらい

歩きながらなおす方針で

親戚付き合い

子供の頃から親しくしている従姉妹と叔母さん。東京にきた時には会いにいくようにしてます

まぁ、大事にされてた印象があるからかな

二人とも、結構な歳にはなったが、それは僕の未来でもある。でも、元気そうでなにより

なにごともなくすごせる、仕事している、それが偉いな

墓参り

天気はよい。暑くもない。少し迷ったが、見つけられました

小金井のお墓は父が亡くなった時に自分の名義になった

「お墓どうするの?」いとこにでも押し付ければいいかってところですけどね

別になにもしなくてもいいのだが、年間の維持費がある。だいぶ値上げされたが。たいした金額ではない

石材店におけがあずけてあって、そこによるとお花と一緒に2千円。それに何の意味があるのかは謎だが

　　子供の頃から、そうなので、そんなもの

妹は処分しようとしたが数百万円かかるのでやめたみたいなことを言ってたな。僕の名義なので忘れていいです

いとこは「八王子にあるお墓を、処分し忘れてた文京区のに移した」みたいな話もあった

祖母も「小金井は遠いから近くにわけた」みたいな話があったような気がするが、そっちは関係ない

妹が入れた卒塔婆もあった

羽田

台風だなと思ってたんだけど、18m/s なら大丈夫でしょ


で、実際、大丈夫だったんですが

　　　羽田のターミナル500m手前で停止

まぁ、よくあることと思ってたら

　　Thunder storm 2 の警告で空港業務は停止

で、50分止められました

まぁ、別にそれだけ。雨男にはよくある話

昭和演歌大全

すなつくなおみの常連さんがもってきてた

この辺は「スナックっぽい」んだよな

たまに、唄うのは良いよね

あっちの方では降ってる

なんか、土砂降りなんだが、超局地的

かけ算の話

まだ、続いてるんですけどね。twitter / X の話はだいぶ変わってきてる

＊　反教科書がいなくなった

教科書のコピペを貼ってるので、「かけ算の定義はない」みたいなトンデモいうのがいなくなった

反教科書を前面に主張すると、twitterの議論として成立しない。まぁ、そうだよね

反順序のかけ算は「教科書に載ってない」「参考文献もない」。つまり科学ではないわけ

教科書のかけ算と掛順を認めて「バツはないだろ」くらいがせいぜいな主張なんだよな

それを越えて

「かけ算の定義はない」
「元から対称なかけ算がある」
「かけ算はどっちでもいい」
「かけ算は累加ではない」
「アレイ図を数える」
「有限集合の直積だから、どっちでもいい」
「文字列のかけ算はかけ算ではない」

とかを主張し始めると、反科学、トンデモ化してしまう

ペアノの構成、高階直観論理の構成は累加なので掛順がある。それは文献はやまほどある

首里城工事中

なんか、結構、すぐにできてしまうらしい

鍵盤の足

Road PC-180と Micro Korg を並べて使ってるんだが、上下にずらした方が良いので本をはさんでたんだが

奥様のお気に召さなかったらしく、足が登場してました

100円ショップ?

ぴーかん

暑いだけですけどね

でも、本土よりはましなんだよな

古島のバス停

なんか、屋根がなおってました

まぁ、また台風で飛ばされるんだろうけど

なんか寝てる

むかーしの写真ね

鼻水

なんか、朝ご飯(カップ麺のフォー)を食べたら、鼻水が

そのまま、昼飯から、スタバと移動したんですが、なんか、ずるずるに

そのまま、スタバにいても社会の迷惑なので撤退

でも、家に歩いて戻る頃には収まってました

なんだったんだ? 熱はないし

まぁ、子供の頃からの慢性鼻炎だからな

県立博物館のブラックジャック展

なんか、量が多いとかなが感動してたので行ってきました。なんだが話を良く聞いてなかった

　生原稿リーダーズダイジェスト

だったのか。パネル毎に原稿とお話が並んでるわけね

いや、自分には少し微妙かも。ゆっくり見るには一部しかなくて、飛ばしてみるのはあれで

漫喫で読む方が良いかも。生原稿には萌えない

hg recover

そんなのあるのか...

　% hg push
　pushing to ssh://christina/hg/ ...
　searching for changes
　remote: abort: abandoned transaction found
　remote: (run 'hg recover' to clean up transaction)
　abort: stream ended unexpectedly (got 0 bytes, expected 4)

なんと、remove からはできないらしく。server 側は singularity container なので、singularity shell で

　Singularity> hg recover
　rolling back interrupted transaction
　(verify step skipped, run `hg verify` to check your repository content)
　Singularity> hg verify
　checking changesets
　checking manifests
　crosschecking files in changesets and manifests
　checking files
　checked 1182 changesets with 1806 changes to 150 files
　Singularity> exit

まぁ、簡単だが、何年もつかっているけど、はじめてみた

水曜日はフロートの日

牧港のエンダーですね。A&W、ハイシーズンなので

　記念写真撮ってる人たちが

それとは関係なく一人で。最近は割とカロリー取るようにしてます

知能情報の新しいサーバ

これらから設定するらしいです。ARM serverもつけたんだが、おまけっぽい

Proxmox で設定したいらしい。まぁ、いいんじゃないかな

さくらサーバ側は手で設定?! ま、まぁ、がんばれ

最近、Ceph の調子が悪いらしい。長く使いすぎだな

遠近両用メガネ

にしてみたんですが。検眼している時はいけると思ったんだが、なんか結構違う感じが

まず、にじみがある

あと、プリズムなしにしたのが意外にくる。何十年もプリズムありだったからなぁ

で、致命的なのが

　iPhoneが見えない

え、どういうこと? 検眼してた時はいけると思ったんだが。近視よりに作ってもらったはずなんだが

まぁ、Ingress するくらいなら

もしかすると、逆に作ってしまったのかも

でも、ノートPC使う時には、まったくだめってわかっていたので、そんなものかも

遠近両用でプリズム入れることも可能らしいんだが

病院

CPAPの貸出に合わせて病院通いなわけですが、通知がなくて、忘れました

別に予約しなくてもよいらしい。いつもの先生は忙しいらしく「この先生なら早いよ」ってことで、そっちの先生に

いや、どうせ、なんもみないし

カレンダーの通知がおかしいのは昔からなんだが、困ったものだな

WARNING: private/main.ics failed verification -- update discarded (will try again).

こいつか...

-

屋富祖の壁

ちょっと安めの飲み屋さん街ですけどね。最近は少し静か

でも、この壁には気がつかなかったな

懐かしいっていうには古い感じでもあるか

めぇーみちの梅干し

子供の頃はよく見たけどね

いまは珍しいか

 猫避けの猫                                                                                                                                               

紅茶用の牛乳にくびをつこっむ奴がいるので                                                                                                                          

もしかすると、前にも書いたかも  

琉大病院行きのバス

ingress の関係でたまたま使ってみました。125番と294番の二つがある

意外に便利なんだが、普天間過ぎると

　新しい道に入って、橋を渡る

おいおい、どこへいくんだよと思っていると、左に曲がって、医学部。琉大病院は、さらにその先

　普天間でいご通りは、5F上にある

一応、

　5Fまで駐車場のエレベーターを使える

ってことらしい。いや、ちょっとした冒険なんですけど

儀保の下地パスタ研究所

3年目らしい。なくなってしまったヨナラボを思い出しますが

こういう名前付けは割と好きかも

割とカジュアルなパスタ屋さんでした

沖縄のテラス席

まぁ、土砂降りではねぇ

そもそも暑すぎるんだが、沖縄の人はわりと平気らしい

真志喜のバス停にて

ラグナガーデンホテルで、55番のバスに目の前でいかれたので、58号線までゆっくり

真志喜のバス停に近づいたら、なんか、ネーネーが走って追い抜いていく

　もしかして、バスが?!

と思ったら、後ろから来てる。なので、一緒に走って乗れたんですが、

　ネーネーは、それを追い込して、いってしまいました

いったいなんだったんだ。沖縄の人って、あんまり走らないので珍しいとは思ったんだよな

でも、実は、その後ろのバスの方が便利だったんだんだが

今日は別なネーネーにも車から挨拶されたんですが、誰だかはわからず。すみません

Sheaf の記述

「It is easily verifed that Γ p is a sheaf」は終わって、Lを書いている最中。たくさん出てくるのが集合であることを示しているところ

まぁ、最初の Functor のFObjが集合なのは仮定するわけだけど

でも、その 「It is easily verifed that Γ p is a sheaf」なんだが、それまでの準備に 600行。そして、sheaf であることを示すのに200行

そもそも sheaf を示すのに関数三つ作らないとだめで、そのひとつは連続写像であることも示すことになる

まぁでも、Zornの補題の時よりはましな気がする。量的には既におなんじくらいだけど、Zorn の時は、かなり書き直したので

これ、Agda 抜きだと、無理だっただろうなとは思う。覚えてられない感じ

眼鏡

どうもレンズがぼろぼろなので。いつもの眼鏡屋さんにいったら

　前回作ったのは 2015

つまり、10年前らしい。ぱかぱか眼鏡は、少なくなってるらしい

　遠近両用がのびてるから

なるほど。で、遠近両用の方も作ることにしました。できるのは少し先だが

下の近くが見えるところを少し指定できるらしい

まぁ、ノートPCでも、遠近両用では無理な感じね。でも、歩きながら Ingress なら使えるか?!

Functor の有界性

Sheaf の ΓのFunctorとΓ p が Sheaf なのは示せたので、L に取りかかってるんだが、いきなり、これ

Sets への関手が有界なわけはない。なに集合演算を平然としてるんだよ…

いや、圏論の人ってそうなんだよな。「一つ上の階層からみれば集合」。どうせ、そんな感じなんでしょう

ChatGPTと相談しても、有界性を仮定するのがよいらしい。あとで、どうトラブルのかは知らないが

agda の abstract

圏論の Sheaf のところまでできたんですが、一箇所、つなげると agda が止まらなくなるところがある

Chat GPT と相談しながらやってたら、abstract が使えると。いつのまに、そんなものが登場したんだ?

確かに通る。しかも、

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

と両立する。すごい

値の接続は見ずに、型が一致してれば良いというものらしい

Γm : (p : Obj (top / X)) → {A B : Obj OX} → Hom OX A B → Hom HODSets (Γo p A) (Γo p B)
Γm p {a} {b} b⊆a = record {
　　　　 func = λ qs → & (F→FuncHOD (dfunc p {a} {b} b⊆a qs) )
　　　 ; is-func = Γo-⊆ p {a} {b} b⊆a
　　　 ; func-wld = lem02
　　 } where
　 lem02 : {x y : Ordinal} (ax : odef (Γo p a) x) (ay : odef (Γo p a) y) → x ≡ y
　　　 →　& (F→FuncHOD (dfunc p {a} {b} b⊆a ax)) ≡ & (F→FuncHOD (dfunc p {a} {b} b⊆a ay))
　 lem02　{x} {y} ax ay eq = ==→o≡ ( FuncEQ→HODEQ (dfunc p {a} {b} b⊆a　ax) (dfunc p {a} {b} b⊆a ay) lem10 )　where
　　　　-- lem10 it will take long time to check, so we need abstract
　　　 abstract
　　　　　 lem10 : (z : Ordinal) (az : odef (SObj.s b) z) → FuncEQ (dfunc p {a} {b} b⊆a ax) (dfunc p {a} {b} b⊆a ay) z az
　　　　　 lem10 z az = begin
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ax) az　≡⟨ ΓCont-eq ax ay eq z (b⊆a az) ⟩
　　　　　　　Func.func (dfunc p {a} {b} b⊆a ay) az　∎　where open ≡-Reasoning

牧港の変なカプセル

なんなんだろね

なんで、ここに置いてあるのか

Hail Mary

まぁ、日本ではアベマリアの方がメジャーだよな〜

と大浦天主堂の説明をみて思いました

映画はまだなのか

そういえば、Led Zeppelin の映画は9月かららしい

9月は東京

9/5-10 は東京に行く予定です

親戚まわりとかお墓参りとか

Sheaf は、順調だが、まだ終わってない。先も長いらしい

教科書では it is easily verified で終わってるところです

カップメンのビルの取り壊し

いや、まぁ、いいんだけど

結構、適当な壊し方だな

居酒屋リセット

反順序は、自分の議論で掛順を理解しそうになると「やっぱり、かけ算はどっちでもいいんだ」とリセットしたりするんだよな

やっぱり

　"abc" x "de" = "abcabc"

で、掛順の議論は終わりだろと思う今日この頃。なんか、この単なる文字列関数に文句をつけている人たちがいるみたいね

Sheaf の続き

なんか、ぜんぜんできなくて。で、どうも、Sheaf の定義が違うらしい

Pull back って a b の二つの対象にたいして定義するんだが「任意の a b 全部」って書いてある

a b に対して、pull back が決まるのではなくて「全部の a b 　の組に対して」決まるのか

ところが、それを書こうとすると、任意個の直積を書かないとだめ。Equalizer で書けるとか書いてあるが…

まぁ、pull back をコピペして (a b : I )を引数で入れればいいんだろ?

Lean 4 で書いてあるのもあるっぽい

国保の振込

なんか、また、降ってきて。前のは市税だったが、今度は国保

なんだが、用紙持っていって「自動振込でお願いします」っていったら「できない」

ってどういうこと? どうも、自分の沖銀の支店は浦添にあって宜野湾市の「自動振込用紙がないのでできない」

で「我如古支店ならできる」え〜? そうなの。どうせハンコ忘れたので家に戻ってから、もう一回

でも、次の振込は来年度らしい。今回のは振り込んでしまうので。来年、まだ国保かどうかはわかんないな

自動振込設定がネットからできるようになるとか書いてあったが「最初の一回目には間に合いません」とも書いてあってた

まぁ、作業は終了

郵便でいろいろ送ってくるのやめろ〜とも思う。まあ、最近はメールも読まないが

長崎の階段

まぁ、階段の多い街でさ。この風頭山から降りてくる階段ね

10分くらいで降りれました。まあ、汗はかくけどね

そして、どうでもいい喫茶店

なくなるお店

割と通った花ぐるまは、4月いっぱいで終了。40年間御苦労様でした

恵は今月いっぱいらしい。25年御苦労様でした

牧港ボウルのボウリングキャットは、淳子さんのお店でしたが骨折で再開は未定

安波茶のSon of Sun も閉店

大山の松倉は週末営業のみに

普天間のフランクリンアベニューは、居抜きで別なお店に

飲食店は、なかなか厳しい。もっと補助でてよいと思うんだが

文字列のかけ算による掛順の可視化

「かけ算には元から対称な定義があるに違いない」つまり累加でない定義ってことね。それはない、何故なら

　"abc" x "de" = "abcabc"

という文字列のかけ算を考える。これは「いくつ分」の文字列の文字の数だけ「ひとつ分」の結合を繰り返す文字列演算ね

Pthon で書くと

　def string_multiply(a: str, b: str) -> str:
　 return a * len(b)

こんな感じ。これは、もちろん非可換

　"de" x "abc" = "dedede"

これは長さを見ると自然数のかけ算になっている。この非対称なかけ算が書けるのは、かけ算の定義が、この演算にそった累加だからなわけ

つまり、この非対称な演算を実現する定義だけが許される。つまり対称なかけ算の定義は存在しない。そして、

　この文字列のかけ算で掛順が可視化されている

というわけ。

反論1 「単位ごとの交換なら掛順はない」

5m/s x 2kg =2kg x 5m/s だから掛順はないってやつね。

　5m/s x 2kg =2m/s x 5kg

はどうする? これには単位ごとの交換は使えない

反論2 「文字列の割り算が決まらない」

長さで考えれば割り算も定義できる。別になくてもよいんだどね

　"abc" x ? = "abcabc" の ? の文字列を見つける

これは簡単。2文字の文字列だ

　? x "de" = "abcabc" の ? の文字列を見つける

これは "abc" だ。でも、「 ? x "de" = "......" の ? の文字列を見つける。. はwild card」にしても良い

反論3 「文字コードで変わる」

len の仕様にしたがうだけ。文字列のbyte長でも良い。それでもいやなの?

それは「反順序の強迫観念」に過ぎない。「かけ算はどっちでもいい」と思いたいための禁則ね

反論4 「勝手に作ったものに過ぎない」

　"vvvvv" x "mm"

5m/s x 2kg のことだ。結果は v が10個。10 kg m/s のことね。任意のかけ算をこれで考えてよい

　おはじきで学ぶ算数

をおもいだそう

JR九州の QRコード

この手のものはトラブルの好きなんだが

　　予約のQRコードをかざすんだが、エラー

あとで気がついたんだが

　　QRコードを読み解らせたあと、アプリになんか変化があり、ボタンを押す必要がある

らしい。それをしないで、もう一度かざすと「エラー」

ってことらしい。ふーん。なんかリーダーがなんかいってたような言わなかったような。よくわからん

というわけで、沖縄に戻ってきました

長崎

なんか、奥様の馬イベントの付き合いで長崎に

馬のイベントにはいかないんですが、長崎で遊んでます

今日は風頭の山にバスで登って、歩いて降りてきました

夜は稲佐山にスロープカーで登って、ロープウェイで降りてくる感じ

街は階段ばかり

でも、沖縄と違って街がきれい。お金があるところは良いね

歯医者

5ヶ月ごとのクリーニング。特に異常無し

なんだが「フッ素抜りましょうね」「え、いいけど、お昼ご飯は?」「30分、だめです」

と、お昼を30分待つことに。歓海門前の真にしました

予約は、さらに5ヶ月後。そんなんでいいのか

同級生になおしてもらった前歯は35年もってるんだよな

その時以来、目だったトラブルは奥歯一本抜いたくらいだ

マイナーカード更新

なんか、Webで申請していたらしく「できました」的な葉書がきてた。年金もそうだが、こういうのに郵便使うのは政府の陰謀的

で、シールで隠されている市役所の窓口(つまり、隠す意味はまったくない)にいくんだが

　「パスワード(番号)を紙に書け」

え〜とは思ったが、大人なので抵抗せずに書く。のだが

　なんかタッチパネルで、そのパスワードを入力しろ
　と、窓口でタッチパネルが登場

え、じゃぁ、さっきの書いたのはいったいなんなんだ? と思ってフリーズしてたら

　「代わりに入力します?」

はい?! なんだが、大人なので

　「お願いします」

で、更新終了〜

いや、パスワード変更してないんだよ。この行事はいったなんなんだ? 単に市役所にパスワードを教える手続き?

時の庭

普天間のラーメンかながわの近くにある喫茶店。台湾系らしく、台湾茶と

　　仙草ゼリー

があります。広くて、無線LANとコンセントがある。水曜休みだが…

午後いくとガラ空きなんだよな。食事ものが最近登場したらしいんだが

なので、行ってみるとよいと思います

近所のフラップコーヒーとか、スタバ、モスとかは割と人が入ってるんだが

Shaef と Agda

Adjunction (HOD-OSCA (topology X) ) ( top / X )

ですが、なんと、一通り書けて、なんでΓの対象が Sheaf になるのかもわかった。

　連続写像の値域の制限ってだけ

なのを、圏とか トポロジーとかSlice圏とか、関手とか、Contravariant とかで難しく書いてあるだけね

なんだが、

　残ってる穴を埋めにいくと、agdaが止まらなくなる

関数が同値なのはすべての値について一致を調べれば良いだけなんだが、そこで止まってしまう

じゃぁ、サーバ側で動かすかと思ったら、既に Agdaのversionが古い。おおい〜

なんか、チェックに時間かかる部分をさぼる方法があったような気がするんだが…

まぁ、もう少し埋めて、それから別なものかな。C-Monoid が面白そう

Google Photos の振る舞い

なぜか、Academic Account ではない方を使ってたりして、たまに「そろそろ一杯です、ストレージ買え」ってのがくる

くるんだが、昔の jpg / heic の重複のを消すと復活する。それを繰り返してるんですが

　重複が甦ってる気がする
　それを消すと容量が増える気がする

まぁ、たぶん、気がするだけだとは思うんだけどさ

そんなこんなで、最近は「そろそろ一杯です、ストレージ買え」ってのはこなくなりました

もしかすると、Academic Accountの扱いになってるのかも。統合したつもりはないんだが

結局、使っている日焼け止めはこれ

なんだが、つけ忘れてしまうので、カバンにいれておくのがよいらしい

沖縄なんで、真っ黒にやいている人もよくみるが、まぁ、ほどほどにね

日焼け止め

まぁ、いろいろあるらしい

Sheaf

まだ、 Adjunction ((topology X)ᵒᵖ → Sets ) ( top / X ) と戦ってるわけですが、

　ΓとLは、だいぶできた

なんだが、「Finally, it is easily verified that ...」が、まったくわからん

この Finally が笑えるのは、Lを作ってるところの Finally なので、さらに、自然変換二つと、その等式二つが残ってるわけ

でも、Agda で書けるので「忘れることはない」。「今まで書けたところは、そのまま残っていて使える」わけね

でも、これプロシンで発表する話でもないしなぁ。役に立つなら話は別なんですが

まぁ、まったくわからんといっても、nat : F → G から、L(F) → L(G) は構成できて、top / X の射の条件である射を作ってるところ

そのうちできるはずです

孔雀楼の冷やし棒棒鶏麺

大山の老舗。結構広い。いつでも開いてる便利なお店(定休あり)

まぁ、普通?

ふんしんせせらぎ通り

伊佐になんかあるんだよな

割と緑が取ってることが多いかも

ポンプで吸い上げて流してるらしく、水が綺麗で魚がいる

ただし「飲めません」。まぁ、そうかな

ゆっくり人がいるほど広くもなく

台風の時には魚は飛んじゃうんじゃなかろうか?