カレー作り

風邪ひいたので延期だったんですが、例年よりは規模を縮小する感じで

なんだが、まぁ、めんどくさい。

　　そもそも、リハビリモード

だな。キーマカレーとエビのカレーは作りましたが、少し力尽きてる感じも。

ベースだけで6個(30人分)作ってた時もあったんですけどね。

恒例のあれ

今年も登場してます。一段だけだけど。ちゃんと入学に書き換わる。

誰も大学に来ない年もそろそろ終わりか。元に戻るのは残念なところもある。

でも、オンラインの授業は便利かな。来年度も授業もオンラインでできるなら、

それでいこうと思ってます。

Cohen Model

順序構造P(Power Set)から Generifc Filterを作るところまではできたので、モデル作ろうってわけですけどね。

valuation とか指標空間とかを使うんですが...

　 val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }

とか書いてある。これが定義だと。いや、だって val の定義に val 使ってるし... data で再帰的定義なのかとか
思ったんですが ( M は可算だから )、どうも、超限帰納法による定義らしい。

学部の時には、まったくわからなかったんですが、まぁ、いろいろやったからな。

val は集合なので、{} から始まって、{{}} 、さらに{{},{{}}} と進む。つまり、

　　x を V にそって分解して、val x G を再構成する

らしい。この時に、G ∋ p がくっついたものだけが、再構成されるわけね。そのまま Agda / HOD で書けたんですが、

そこからが進まない。だって、HOD だと、V=L じゃないから。なので、Vで再構成するためには、

　　順序数をVで作る必要がある

それはいやだな。できないことはないんですが。それをいうなら、ZFに沿って全部やることも可能だが

　　それでは、Agda に向いた集合論にならない

だよな。ここから、

　　M[G] : HOD
　　M ⊆ M[G]
　　M[G] ∋ G
　　M[G] ∋ ∪G

となる可算モデルM[G}を構成できれば勝ちなんですが、

　 M[G] = { val x G |　M ∋ ∃ x }

なので、そう簡単にはいかないらしい。

ところが、Mは可算モデルだから、その要素は数え上げて取ってこれる。つまり、M=Lとしてもよい。

　　¬ ( M ∋ G )

は示しているので、L に含まれない G がある、つまり、非構成的な実数があるまでは終わってるらしい。
(全体のLがMだと思えば)

M[G} の構成は、M[G]のLとMのLが同じなことを示すのに必要なだけなので、もしかして要らない?

M[G}をHODで作れないわけでもないらしいので、まだ、先は長そうです。
-

東芝の洗濯機のUI

まぁ、BAD UI は JTC の伝統だからなぁ。予約ボタンを押すと

　　07:40

とかでるんだが、これが午前なんだか午後なんだかかわからない。時刻は直接は入れられなくて、これを上下するんだが

あるところを過ぎると、07:40に戻る。規則性が不明。

でも、これは午後7:40分で洗濯開始時刻らしい。いや、どっちかていうと帰る頃に終わってる用に設定したいんですが。

このまま放置すると帰ってから洗濯機が周り始めるという残念なことに。

なので、帰ってから電源切ってもういちど。

　　08:40

う、これは。きっと朝の8時かな? それでいいか。

タッチパネルなんだから、もっと情報出せよと思うんですけどね。終了予想時刻とか。

シン仮面ライダー

まぁ、風邪も収まったので。少し体力削られてるけどね。

　別に普通に佳作。

期待ししすぎなんじゃないの?

　解像度高く初代が観れる。

まぁ、それでいいかな。シンウルトラマンだって、そんなもんだったし。

仮面ライダーは漫画とテレビとリアルタイムで見た世代なわけですが、それほど思い入れがあるわけでもなく。

いやでも、V3までの展開は良かったかな。アマゾンでは落ちましたが、アマゾンファンもいるんだよな。

石森の設定は少しだけハードより。テレビも最初はそれを踏襲してたんですが、途中から「変身!」に。

がっかりがなかったかというと、まぁ、あったかも知れん。でも、そこに突っ込むほど子供でもなかった。

　　むしろ、サーキット一周してくる間に改造されてる的なシュールさ

が良かったかな。死神博士と地獄大使の悪役な感じが、むしろ喝采で。

　　みんな世界征服したいでしょ?!

そういうのをぼーっと観てる的な感じでした。少し疲れている時期だったかもな。

超人の中で、普通の人間として戦うライダーマンとかに少し思い入れがあったかも。

タイピン

なんか、割とお気に入りのをなくしてしまって。しょんぼりだったんですが、久しぶりに大学にいったら、

　　事務の机の上に置いてあった

らっき〜　誰だか知りませんがありがとうございました。

いや、もうさびさびなんだけどね。銀色のシンプルな四角いやつだが、割と長いのが特徴。

そうそう幅広のネクタイが流行っていた頃ね。確か羽田で買った。

黒いのを落としてしまった時も、北ローのところで拾ったんだよな。自動車に踏まれて残念になってた。

風邪は水曜日の夜がピーク

だったみたい。少し熱がでたくらい。明け方咳で夜熱とかが定番ですが...

　　風邪薬は飲まない派

ですが、ビタミンCは取った方が経験的には良い感じ。多少食欲なくても、お腹いたくても、

　　飯は食う

が母の教えですが、汁っぽいものでお願いします...

風邪でお休み中

まぁ、休みになるとそんなもんです

Twitter で数学

基本、Agda でやるわけですが、

　　Agda だと、周りの term にひきづられて、うまくできないことがある

問題を局所的に見ると解けないわけね。なので、

　　Twitter に問題を書くとわかることがある

まぁ、いろいろあるけど、

　　そもそも、Twitter に書けるくらいに問題を理解しているか

が大きい。文字で書くのが重要らしい。特に

　　問題の大きさを限定できる

からなんじゃないかな。でも、割と書ける。

これは、チコノフの定理でFilterの射影で極限は得られるけど、

それが極限であることを示すにはFilterを極大化しないとだめな理由の説明だな。

もちろん、全体の証明はかなりでかいので、その背景は多い。他の人にわかるわけじゃない。

でも、知ってる人なわかるかも。

学部の時の読み方と差があるのは、Agda をやったからか。

https://twitter.com/shinji_kono/status/1633657200546844672?s=20

Generic Filter

順序構造P上の Generic Filter 作って、集合論のモデルを作り、連続体仮説とか選択公理の否定をやるあれですね。

ブール代数を使う方が良いらしいんですが、公理的集合論とKunenとかの古い本はそうではなくて。

Generic Filterの方向が割と謎で、いろいろ間違ってる。結局、反対方向のIdealでやることに。さらに、

　　位相空間論で使う ideal と、少し定義が違う

いや、違ってても同じだろと思ってたんですが、ideal ⊆ L ⊆　Power P でやるんですが、

　　　 ideal1 : { p q : HOD } →　L ∋ q　→ ideal ∋ p →　q ⊆ p　→ ideal ∋ q
　　　 ideal2 : { p q : HOD } → ideal ∋ p →　ideal ∋ q　→ L ∋ (p ∪ q) → ideal ∋ (p ∪ q)

なんですが、二つ目に差があって

　　　 ある ideal e　があって、 p ⊆ e ∧　q ⊆ e

になってる。位相空間論だと L = Power P でやるので、p ∪ q がL に必ず入るので、(p ∪ q) ⊆ e から ideal ∋ (p ∪ q)がでる。
なので両者は同じなんですが、L ⊆　Power P だと、L ∋ (p ∪ q) とは限らないので、そうならない。ひどい。

それがわかれば、割と簡単に書けた。所詮、可算モデルな集合Mから作る可算集合G ⊆ L なので、自然数Nの入力する関数だからな。

Generic Filter は稠密な集合と必ず交わるという性質があるけど、そっちは影響を受けない。けど、部分関数なPを使って、

　　　¬ ( M ∋　G)

を示そうと思うと二つ目の条件の差が効いてくるという感じなので少しはまりました。

Ideal なのは要素毎の補集合をとれば filter になるので、まぁ、いいかってところです。

チョコレート

これは割と良い。割って食べる感じだな。

ライカムのGodivaでは、カレのばら売りが実はある。

でも、隠しメニュー的なものなのかな。売りたいものとは違うのかも。

普段使いは明治のブラックです。

どっかで見かけたラバーダッキー

某氏を思い出しますけどね。

00年代から一緒に飲んでるママさんのところ。

Fortigate and Certificate

いや、自動updateするでしょ? で、

　　Rest API

かなと思ったんですが、アクセスできないので log みようと思ったら、

　　GUIからは設定できない

で、

　　CUI からだとないと言われる

と思ったら、Forti OS 7.0 からか。なので、version up から。7.2 にあげられないのはなんでだ。

それでも、結局アクセスできない。Chat GPT が Rest API 叩くのを書いてくれるので楽ではあるんだが...

でも、policy は見れたらしいので、Rest API tokenの権限の問題かも知れない。

fortigage が自分で ACME することも可能らしいんですが、それも失敗する。なんか port 開ける設定がいるのかなぁ。

でも、wildcard 使いたいなら、Rest API かなぁ。

ひさしぶりにDesktop

GDP3を出歩くときだけ使うのはどうかなと思って

MacMini すでにかなり古いので、OSい上げからだったわけですが

それほど問題はなく。ただ、nvimのlua5.1のluautf8は、ちょっとはまりました

wget が古くて luarocks が動いてないだけだった

nvim の中でluarocksを動かす方法ないのかな

でも、寝っ転がって使えないとか輝度変更が微妙とかいろいろ。

まぁ、なれるかもしれん

ZoomがＰＣが違うとアカウント切り替えてくるのがめんどい。

それぞれ 別アカウントという手もあるが。

MBP16で全部ってのもいいんですけどね。

バスナビ

新しい方が、アプリも含めて絶望的に使えないのだが、

古いのが残っているので、まぁ、なんとか

あんまり知られてないかも

こっちの方だと、バス停ごとに Bookmark して簡単にアクセスできる

残念なのは、最初にくるバスを路線ごとに調べないとわからないこと

宜野湾だと平然と20分遅れたり、10分かかるはずなのが5分で来たりするからな

たまに載ってないバスもある。沖縄バスで多い

この企業や役所ののWebサービスのUIのダメさは、日本の伝統らしいけど、

　　社会の生産性をかなり下げてる

沖縄のバスが使えない原因でもあるな

そもそも、バス会社の人がバス使ってないから

自社のサービスを使ってみたこともない人が作って放置、そんな感じか

https://www.busnavi-okinawa.com/mobile

猫に注意

まぁ、どういう風に注意するのかはわからないんですけどね

白いジグソーパズル

学生時代ありがちな

いや、自分の時も1200ピースってのがあって。

　　パネル三枚分

ところが、ちんたらやってたら「FGCSで見学が来るから、片付けろ」というお達しが。

で、超高速で片付けた。前世紀のかなりあとまで残っていたんですが、デジカメ前だからな。

写真が残ってないのは残念だ。あの頃は、Retina もってたので、白黒のフィルムだけ現像なし
でもいいから、もっと撮っておけばよかったなと今では思う。

でも、その頃は、その頃に集中できたので、それはそれでよかったかな。

MacMini のOS update

うっかりすると2018のだったりしてなぁ

macOSがCatalinaかぁ。ありがちではあるんだけど。

Ventulaに上げるんですが、いきなり、ssh port がdefaultに

/etc/services変えるだったような ...

この前、手元のをあげたばっかりなので、楽勝なはずですが、少し難航中です

brew が劇遅いのなんで

チコノフの定理はできました

Agda で書くトポロジーで始めたのは一段落。

まず、FのPとQへの射影が超フィルターであることを示す

すると、それぞれに極限x,yがあるので、その直積<x,y>が極限になる

あとは、その極限<x,y>の近傍がFに含まれることを言えばよい

ってわけですが、フィルタの射影が割と面倒だった

Agda の直積は data で書けば良いんですが、集合なので、

　　二つの要素は集合にエンコードされる

具体的には、<x,y>は、{x,{y}} という集合になる。これは pair で書けて (x , x ) , (x , y ) 。

このエンコードで、それぞれを取り出すのを示す必要がある

　　prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )

ってのはずいぶん前にやったんだが、学部1年の頃の

「なんでこんな当たり前のことを証明しないとだめなのか」ってのを、いまさら理解した感じ。

いや、瞬時に理解した人が多いんだろうけど。

さらに、

　　data ZFProduct　(A B : HOD) : (p : Ordinal) → Set n where
　　　　ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )

　　ZFP　: (A B : HOD) → HOD
　　ZFP　A B = record { od = record { def = λ x → ZFProduct A B x　} ... }

　　zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
　　zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a

みたいに、Agda のdataと対応させる必要がある。　これがわけわからない振る舞いで楽しかったです。

射影自体は

　　　　 FPSet : HOD
　　　　 FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))

二段の置換公理でできるんですけど、これがフィルタであることを示すのがそこそこ難しかった。

irr とか HeterogeneousEquality とか...

https://shinji-kono.github.io/zf-in-agda/html/Tychonoff.html

ここしばらく良い天気

うりずんの頃だからな〜

ちょっと前までの雨雨がうそのようです

メス猫のうるささ

いや、まだ3才だったかな。若いからなぁ。

　　けつ叩けとうるさい

家猫だから、そういうのと分離されてるのでしかたないんですけどね。

オス猫の諦めさ加減あるいは、怠惰を見習ってほしい。

がん保険

結局、この年まで何もなかったので、まぁ、賭けには負けた感じ

でも、それは残念ではないよね。

ハリーズのおばちゃんとか、庵のママとか、がんで亡くなった人も生還した人も。

保険は社会のためにかけるものなので、ワクチンとも共通してる。

それだけに、国がサポートするべきものだと思うけど、合理性に欠けるものがあるのは残念。

個人から見た確率で、5%か0.05%かを体感するのは不可能だと思う。

それに配慮した政策が欲しいところかな。精神論とか陰謀論いらんから。

赤いポータル

ingress ですね。破壊すると、XMがゼロに。でも、

　　いろいろ落とす

が、基本ごみ。西原運動公園あたりにでるが、

まぁ、あっちは、あんまりいかないです。

お邪魔虫みたいなもんだな。

位相空間論の続き

チコノフ(Compact 空間の直積は積位相に関してCompact)の続き

　Compact ⇔ 有限交叉 ⇔　任意の超フィルターが収束 (A)

で、積空間の任意の超フィルターの射影を取ると収束先が分かるので、収束を示せば良いらしい。

定義が多くてね。このフィルターFの収束ってのが「P∋limitがあって、limitの近傍をFが含む」っていう意味。

record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
　 field
　　　 proper　: ¬ (filter F ∋ od∅)
　　　 ultra　 : {p : HOD } → L ∋ p → L ∋　( P ＼ p) → ( filter F ∋ p ) ∨ (　filter F ∋ ( P ＼ p) )

record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) )
　　(ultra : ultra-filter F ) : Set (suc (suc n)) where
　field
　　limit : Ordinal
　　P∋limit : odef P limit
　　is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)

いや、今年初めて知りました。学部時代の自分に「読めよ!」って思った。xの近傍の定義が、

　xを含む開集合oがあって、それを含むPの部分集合uの集合

record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where
　field
　　u : Ordinal
　　ou : odef (OS TP) u
　　ux : odef (* u) x
　　v⊆P : * v ⊆ P
　　u⊆v : * u ⊆ * v

いや長いし。位相空間の基底、フィルター基、近傍と似たようなものがたくさん。

収束の定義が間違っていたのが片付いたので、A まで Agda で書き終わりました。Zorn の補題を使うのは

　有限交叉 →　任意の超フィルターが収束

ここだけ。なぜか、呼び出すと agda でのチェックに1分かかる。外すと数秒。Zorn 自体はすぐ終わるようになった。

謎すぎる。普段は外してるんだが、入れる入れないでcheckに差がある。こまったもんだ。

残りはチコノフの定理本体だな。いきなり、フィルターの射影の定義を間違えていたが、割とすぐに片付くんじゃないか?!

Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ　→ Compact (ProductTopology TP TQ)
Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
　 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F)
　　　 → UFLP (ProductTopology TP TQ) F UF
　...

いや、Zorn の補題もそんなこと言ってて9ヶ月もかかったんですけどね。

一番餃子の自販機

なんか、大謝名の坂は餃子通りと呼ばれているらしく。

カラオケありな中華な店の小籠包がおいしい説も聞いたんだが、覗く気はせず。

冷凍餃子専門店とかも。

まぁ、いろいろあるけど、一番餃子の水餃子かな〜

Terminal は白い画面派

いや、Sun3 時代からそうなんですよ。Smalltalk とか、Mac とかそうでしょ。

　Black on white

もちろん、VT102とかCIT101とかは、White on black だったんですが。

一つの理由は、

　　プロジェクタで文字が潰れない

という理由だったんだが、今は、もうあんまり関係ないかも。プロジェクタ自体あまり使わない。

プロシンでは使ったが。

で、vim の color scheme で Black on white に合うものがないという問題がな。結局、zellner なおして使ってます。

github と HTML

元の github は、HTML が結構排除されてて。でも、agda は HTML生成機能があって、わりときれい。

で、どこに置くのかと探したんですが、github.io を使うらしい。特定の名前でおけばいいわけね。

元のと連携する ci ぐらい書きたいが、まぁ、いいかな。

Topology の方は、compact と finite intersection の同値までできました。チコノフの定理まで、あと少しだな。

https://shinji-kono.github.io