P's Square Beer Rise

なんか、週末はここでやるらしく! そばのWest Field Cafe と串カツ田中からつまみは頼めるらしい。

330沿いので、排ガス臭いのが残念か。まぁ、ここはバイパスからはずれてるので、そんなに多くはないんだけど。

West Filed Cafe も愛用してます。割と普段通り営業。

真栄原のエージェント

いつも緑のエージェントが夕飯前と後とご丁寧に二回も。

がんばって埋めますが、ま、何事も予定通りというわけにはいかないよな。

このために、犬の散歩よろしく、いつものところからキーを集める。

そんな感じの運動ですが、

　　でも、なんか、ここ数週間体重が増加方向

まぁ、代謝が落ちてるってことだよな。筋トレでもするか。

Google App Script

まぁ、良いんですけどね。便利に使うなら、それでいいけど。

　　でも、それを業務的に使って、バックアップはどうするの?

いや、気持ちはわかる。Google に閉じて使う分にはメールの検索からなにから JavaScriopt 的なくそでなんでもできる。

でも、それってさ、

　　Google ban されたらどうなるの?

そもそも、いまどき、git / hg なりにリポジトリのないプロジェクトとかあり得ないと思う。こいつは、

　　Google にあるだけ

で、取り出すには Web 経由で取るしかないらしい。もっとも、

　　鍵が script に埋め込まれてるのが普通

なわけなので、public な github とかには馴染まない。もちろん、

　　commit する時には置き換えて、運用時に実際のキーを使う

みたいなことは可能なのだが、事故はあるからなぁ。

せめて共有プロジェクトにしてください。その自分一人で持ってるようなものは

　　トラックナンバーを増やすだけ

だから。

Teal 組織

Reinventing Organization ですが、まだ、20%くらい。ゆっくり読んでます。Paper White だからか、英語だからか...

一つはむかしより丁寧に読んでるからってのもあるかな。

Red 支配 / Orange 管理 / Green 家族、みたいなものから、Teal 自律、とかにいく話なわけですが、

　　ちょっと Spiritual な感じも...

オランダの介護組織の話が出てきてようやっと面白くなってきた感じ。十数人の均一な自律単位の話はうちの学科的でもあるし

OSSのグループの話みたいでもあるな。そして

　　ネット前提

IT音痴な人たちには関係ない話かも。組織分類の話は、組織はいろんな要素を持つものだ的なところもがあると強調されてました。

もう少し上の階層の話があると思うし、まだ、先長いから、まだ、良くわからないかな。

Reinventing Organizations
https://www.amazon.com/dp/B00ICS9VI4

南極

github のあれですが、結構な比率で取ってるらしく自分のも一つ引っかかりました。圏論の方が量は多いんだが、集合論の方ね。

うちの卒業生でも github 使ってるのは多いので、そこそこ引っかかってるみたいね。

fork は元のしか取らない方針なのかな。

集合論の方は Generic Filter の定義はできたので、いろいろやる部分があるのだが、取りあえず集合の自然数とAgdaのNatの変換の iso を書くので

いつもの依存性のある項の置換で引っかかってます。あれ、なんか統一的な解法ないのかな。

普天間の Agent

最近、基地の中の Ingress の Agent ががんばっていて。基地からのリンクはなぁ。

でも、普天間は民間地に囲まれているので

　　一周して取ればだいじょうぶ!

まぁ、大汗かきましたけどね。

いや、みんなストレス溜まってるよな。

経済は変われるのか?

コロナ騒ぎも2ヶ月自粛すれば収まることはわかってる。実際、5月に収まりかけたのにね。我慢できない子供みたい。

大都市はだめだが地方都市はそれほどでもないと思ってたんですが、米国はNYで増やしてから地方にばらまくという仕組みになったらしく...

毎月10万円半年配っても60兆円で赤字国債は6%しか増えないわけで、非常事態なんだから、それくらいやれと思います。

年間25兆円の観光業が消滅してるわけでしょ? お金配るしかないと思うけど。

インフレになるという人も(こりずに)いるかも知れないけど、結局、十分な供給があればインフレにはなりようがないらしい。

今の産業は実はもうあんまり三密じゃないんだよな。むしろ営業とかホワイトカラーが三密なわけで...

もちろん、どこでも感染することはあるわけだけど、

　　ほとんどの人は感染させない
　　大量に感染させることがたまにある

みたいな状況は変わってない。いや、米国は変わったかも。でも欧州はほとんど収束してしまった。

ひどかったイギリスとか、いろいろ批判のあったスウェーデンでさえも。

日本も収束していると思われてますけど、

　　昔みたいな観光者がたくさんな状況に戻る

ってのはしばらくないかもなぁ。香港でも5年くらいかかったらしい。

緩めれば増える状況なので、社会を変えていくしくないと思う。大量感染の機会を減らしていく方向でしょうね。

小型の重機

なんかスパイダーマンの敵役的な。どうやって運ぶのかという疑問があるが、それほど重くないのかも。

330の赤道ポケットパークあたりで見かけました。

コロナと糖尿病

コロナの死者は馬鹿にできないっていうグラフを見たら、トップは

　　糖尿病

なんと栄養失調の倍以上。今や人類は飽食で死んでるんだなと思いました。

https://public.flourish.studio/visualisation/2944635/

クラウドは便利使う、でも頼らない

そういうスローガンですが、学生の今学期のプロジェクトベースな授業のリポジトリですが、

　　既にない

いや、授業で要求しているものなんだけど。学科のMercurial でも gitlab でも github でもなんでもいいけど。

消すのはひどいな。まぁ、

　　黒歴史にしかならない

のはその通りなんだけど。でも学生が最初に作ったものとか誰も期待してないし。採点まではおいといて。

ルートビア フロート

ちょっとできごころで。まぁ、半分で脱落しましたが。

普天間をいつもの ingress で廻ったついでです。

いつも思うんだが、砂糖抜きでないかな〜

フィルターの続き

元ネタは田中先生の公理論的集合論で、例題は

　　set of finite partial function from ω to 2

ですが、いろいろ苦労して書けたんだが、集合論でやるの面倒くさすぎる。Filterの定義もわかったので、

　　Agda でやる方が良いんじゃないか?

そもそも、強制法で使う filter は別にZFの中でやる必要はないわけで... で書いていったんですが、

　　なんか教科書と合わない

そもそもフィルターの定義がタイポしてるし。「x < y なんだが集合だと x ⊇ y 」とか書いてあって、

　　小さい方が拡大な

とか書いてるあるんですが、自分でばっちり間違えてるし。しかも、例題の方も! どうりでできないはずだ。ぷんぷん。

いや、たぶん。後の方の版ならなおってるんじゃないかな。

でも、がんばって集合論書いたけど、はっきり Agda で直接やる方が楽。L の集合は L → Set で良いらしい。

Power Set は (L → Set ) → Set だな。

この本、20年以上読んでるんだけど、今頃、気がつくのは問題ありだな。

Ingress の Key 整理

今のスキャナーになってからの一番の苦行。まぁ、前も対して便利だったわけじゃないですが。

　　重要なところ以外は最大4くらいにして
　　2個を残してキーカプセルにしまう

ってだけだが、これを手動でやらんとあかん。スクリプト一発じゃんと思うけど。しかも、スキャナーのUIがいじわるで

　　キー整理している時に、上下のキー列を勝手に動かし
　　移動上限数を間違える

ってな状況。数年なおってないので治すきないんでしょう。

せめて、目の前、あるいは目標のポータルのキーがキーカプセルにあるかどうかくらい表示してくれても良いと思うのだが。

もっとも、CF構築までやるエージェントは少数派らしい。ちまちま作ってます。最近は、西原サンエーくらいまで足を延ばしてます。

石頑當

プロレスラーの名前だとか、単にかっこいいだけとか言われてますけどね。なんとなく、

　　安直なものほど強うそうな気がする

お金かけたものよりも。Ingress のポータルになりにくいのが残念。もっと、通そうぜ。

といいながら、あんまり、審査してないな。

ID : Invaded

ID は井戸と無意識のイドに掛けてるらしい。殺人者の無意識にダイブできる的な設定。古くはディックの宇宙の眼にさかのぼるな。

自分自身のイドに入るとイド嵐が起きるとかいろいろ面白い仕掛けがある。ドサディ実験星的なところもある。

ダイブした人を外から観測してるのはタイムトンネルっぽいな。

いくつか釈然としないところもありますが、まぁ、面白かったかな。思念粒子が「落ちてる」っていう設定とか。

探偵物が苦手なのは江戸川乱歩たくさん読んだりしたからだと思う。コロンボみたいな倒錯形式だとまぁ。

https://id-invaded-anime.com

新しいサーバ

普通にDell/EMC x 6 です。2ヶ月かけてゆっくり設定する予定。「いっぺんに電源入れないでください」指令が。

　楽しい作業なんですが

最近、インフラ系は学生に人気がないらしく、うちのシステム管理チームも新人があまりいないという問題が。

アニメの

　○○部存亡の危機

ですね。せっかく、情報系の学科を出るのだから、インフラの技術に慣れておくと、つぶしが効いて良いと思うけど、まぁ、

　余計なお世話

かな。まぁ、今まで毎年そうだった気もするんだが、毎年、

　異常に優秀な学生がいた

ような気もする。もちろん、その異常に優秀な学生を育てるためのカリキュラムなんですけどね。

玉城先生

珍しくメール読んだら、いきなり。玉城史朗先生は自分より1年早い赴任だったんじゃないかな。最初のシステム更新を一緒にやったのを思い出します。

数年前に身体を壊してたのは知ってたんですが、大学で会う時には元気そうだったのに。聞くところによると最近は入退院を繰り返していたらしく。

最近は農業のIT化みたいなのをやってて苺の二酸化炭素の制御とか、山羊にセンサ付けたりとか。最初の頃は太陽電池とか風力発電とか。

割と地元の企業と一緒にみたいなのが好きだったみたい。農家は毎日来い的にこきつかうの学生には不評だったみたいです。

酒飲みですが、割と居酒屋で飲む感じ。Mou でも何回か見かけました。身体壊してても飲む的な。僕も酒のみだから気持ちはわかる。

今年退官だったはずですが、学生の面倒見は良い先生だったので残念です。

割と板書な先生。情報数学の授業はもう少しレベルをあげて欲しかったが、うちの学生にはちょうど良いくらいか。

告別式は北那覇でしたが、地元に密着した先生で三線弾いたりしてたのでたくさんの参列者が。全員マスクで。さらに

　　Twitter の #forever_t_shiro

　　Zoom online 告別式

も。好きだった We are the champion も流れたらしい。

Kindle の辞書

授業の最初では英語の教科書の読み方とか教えたりするんですが、

　　Mac も Kindle も辞書が使えるのが素晴らしい

初代 Kindle はタッチパネルでなかったんだが、新しいのは「そこを押せば辞書を引いてくれる」。超素晴らしいです。

英英の引き方も教えるんだが、それが役に立つ段階に学生がいるのかは謎だ。日本語で引くと、

　　Strive も Effort もみんな「努力」

別にいいけどさ。Kindle の英和があほだから説はあるな。シソーラス見るべきだ説もあるけど、微妙。

熟語の選択が微妙。一応、選択を広げられるんだが。

Podcast もあるし、オンライン英会話教室も。Netflix の字幕は便利だし(Amazon は死んで欲しい)。素晴らしい英語勉強環境だ。

Dirac とか Qwine とかを辞書片手に格闘してたのが懐かしい感じ。

Dictation とか Shadowing とかしなければ伸びはしなかったりするから、結局は、環境だけではだめで、いかに語学に commit するかってことだけど。

サンロードビル

前にも書いたような気もするんだが、佐真下のビルです。まだ、あるので。ごらんのように廃墟。しかし、まだ、何軒かお店が残っている。

元はホテルだったらしく、それを飲み屋さんのビルにした。真栄原のライトビルとか、昔はパチンコ屋だったのだが、飲み屋さんのビルに。良くある。

割と謎なんだけど、ビルのローテーションみたいなものがあるらしく、幽霊ビルだったのがよみがえったり。警察の恣意的な指導のたまものらしい。

なんですが、この状態なので、もはや消防署の許可が出ないらしく、オーナーも建て替えする気もないらしい。ま、良くある。

　　幽霊ビルを放置しても大丈夫なようになってるのが日本の法律

なので。

昔、何軒か入ってた頃には2,3回いったこともあります。一階の「わざび」は割と美味しかったらしい。ウニホタテだったかな。

それも10年以上前の話ですね。少し上には

　　MTBビル

が。宮城テナントビルらしい。そこの待夢は今でもたまにいきます。既に老舗だな。玉城先生と一緒に行きたかったかも。

いや、玉城先生とは会っても居酒屋が多かったかな。

適当にぼろくなった安物

みたいなのが割と好きです。油断すると捨てられてしまうのだが。

機内販売で気まぐれに買った物。下を隠せば普段使いできますとか言われたが...

　ドラえもんのファンではありません

Ingress 用です。最近は枕元に置いてるな。

大汗

だいたい大学に入るのだが、誰にも会わない感じ。学生はぼつぼつ来てるらしい。

Ingress で寄り道すると、大汗かくので大学で着替えてます。

毎日、着替えを持ってくのは残念な感じだな。大学に洗濯機欲しい感じ。

すると、大学に住み始めてしまう...

R.Pes

去年、真栄原の交差点にできたカフェです。ここと、P's square の West Field Cafe ができたので、お昼ご飯に便利。

どっちも Wifi あるし。コロナ対策は... 入口にアルコール置くぐらいか。沖縄はどこもそんなものかも。次が来るまでは。

パスタもカレーもランチも、まぁ、普通かな。普通が大切。

https://twitter.com/rpes6

Kindle Paper White

初代 Kindle がまだ動いていたりするんですが、「読めない本がある」のと、

　　風呂場で読みたい

ってのがあって。安いし買ってもいいかなと。なんだか複数のアカウントの使い分けがあったりするし。

なんですが、

　　初代 Kindle と読める本は変わらなかった

がっかり。まぁでも、風呂場では使えるし、初代は touch panel でさえないので辞書引くにもカーソルだったから。

バックライトあるから明かりなくても読めるし。そこそこ便利かな。

Anthy vi拡張

結局、VSCode は気に入らなくて、vim/emacs/evil on xterm のままなんですが、Onew がなんとかみて、

　　そういえば、escape でかな漢字変換を切る方法が...

でぐぐったら、Mac UIM だと Anthy の vi 拡張があるとか書いてる。そういえば、そんなのあって入れてたような。

いや、最近は prime にしてたんですが、Anthy にしたら、ちゃんと escape で変換モードが切れる。

う、もしかして、コマンドモードで「ち、変換モードだぜ」とか思ってたのは、もしかして、scape で切れてるのに再度変換トグル入れてた?

でも、それって10年前以上の話だったような。まぁ、それほど日本語の途中でコマンドモードに移行するわけでもないからな。 割と間抜けな話。

てだこ浦西駅の工事

西原入口の交差点に通じる道を掘り返してるのが理解不能なんですが...

おかげで、西原入口から幸地の高速バスまでの乗り換えがさらに遠い回り道を強制されることに。

まぁ、ゆいレール側からは、それほどでもないのだが。

せめて97が駅前を通るくらいやっても良いと思うんですけどね。125は不可能ではあるが。

もっとも、高速バスの方が琉大にいくにも便利ではあるんだが。97は東口から入るとかしないし。

結局どうなるかはわからないんだけど、もしかして、

　　てだこ浦西駅のバスターミナルは、どのバス会社も使わない

ってな落ちとか?

自分的にはゆいレールの終電に合わせた北向けのバスを出して欲しいと思うが...

逆に125/25/97の本数を減らすと言う技にになっているらしい。

結局、ゆいレールとかバスとかに移行しようという社会的モチベーションがないからだめってことなのかなあ。

undo-tree

ZF on Agda の方の気まずいバグの方はなんとかなって、クラスと集合の違いに付いて理解が深まった。クラスは順序数方程式の解に上界がないんだな。

ingress の方は不義理してすみません。

なんですが、今日のお題は Emacs の undo-tree 。VSCode のAgdaはあんまり良くなかったので、いまだにEmacsなんですが、viper から evil に乗り換えました。

今は、emacs lisp の packager があって、emacs lisp 経由で install するらしい。

　　;; Set up package.el to work with MELPA
　　(if nil (progn
　　(require 'package)
　　(add-to-list 'package-archives
　　　　　　　　 '("melpa" . "https://melpa.org/packages/"))
　　(package-initialize)
　　(package-refresh-contents)

　　;; Download Evil
　　(unless (package-installed-p 'evil)
　　　(package-install 'evil))
　　))

一度、入れたら nil で切っておかないと、毎回、アクセスが...

evil は vim なので undo が複数回できる。別に Emacs 側のを使ってたので良いんですが、ところが、

　　undo-tree っての入れられて、undo が編集履歴の一つの枝に限定

げ。つまり、戻って再編集すると、その先に戻れない。そのためには C-X u で graphical (characterの) mode に入って枝を選択する必要がある。

こんなの。

|　　　　　　　　　　　　　　　　　　　　s
|　　　　　　　　　　　　　　　　　　　 __|
|　　　　　　　　　　　　　　　　　　　/　 \
|　　　　　　　　　　　　　　　　　　 o　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　 o
|　　　　　　　　　　　　　　　　　　 |
|　　　　　　　　　　　　　　　　　　/ \
|　　　　　　　　　　　　　　　　　 x　 o
|


この選択が良くわからなかったんですが、

　　C-f で切り替えた後に space を打つと、その枝が選択される

という方式らしい。なにそれ。ちゃんと help に書いといて。

Agda はかなり試行錯誤するので、普通に木をたどる方が便利な気がする。はずしてしまおうかどうか考え中です。

HOD

順序数方程式である Ordinal Definable てっのを使う ZF Set Theory の Model を Agda 内で作るってのをやってたわけですが、
OD には「全部の順序数」という自明な最大があり、最大のない順序数に対応させるのは変だなと思ってたのだが、

<-osuc (c<→o< { record {　def = λ x → One } } )

とすると⊥が出てしまう。これは大変よろしくない。つまり最大のODの次の順序数に対応するODが撮れて矛盾してしまう。

sup でも osuc を返す関数という自明にsupのない関数があって、定義域を狭める必要があるらしい。

つまり、ODの解がある順序数で抑えられないと、よろくないらしい。古典集合論では

　HOD { x | TC x ⊆ OD } Hereditarily Ordinal Definable

ってのを使う。TC は推移閉包で、つまりxの要素は全部ODっていう性質を持つものらしい。ここで x は V つまり宇宙を動く。

でわかったんですが、OD ってのは解が順序数の中で抑えられてない場合があって、それは集合でなくてクラスなわけだ。

ということは逆に解が上限を持つことが HOD の条件になる。つまり、

　　record OD : Set (suc n ) where
　　　field
　　　　def : (x : Ordinal　) → Set n

　　record HOD : Set (suc n) where
　　　field
　　　　od : OD
　　　　odmax : Ordinal
　　　　<odmax : {y : Ordinal} → def od y → y o< odmax

としてやれば良い。これで矛盾は避けられる。順序数との対応はHODだけにするってのでいけるみたい。

この方がクラスと集合の区別もはっきりする。順序数の縮小写像を使うと集合の中でOD/HODを使ったモデルを作ることも可能。なるほど。
中から見るとクラスだが外から見ると集合ってのもわかりやすい感じ。

　　record ODAxiom : Set (suc n) where　　　
　　 field
　　　od→ord : HOD　→ Ordinal
　　　ord→od : Ordinal　→ HOD　
　　　c<→o<　:　{x y : HOD　}　 → def (od y) ( od→ord x ) → od→ord x o< od→ord y
　　　⊆→o≤　:　 {y z : HOD　}　 → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
　　　oiso　 :　{x : HOD }　　　→ ord→od ( od→ord x ) ≡ x
　　　diso　 :　{x : Ordinal }　→ od→ord ( ord→od x ) ≡ x
　　　==→o≡ : { x y : HOD　}　　→ (od x == od y) → x ≡ y
　　　sup-o　:　(A : HOD) → (( x : Ordinal ) → def (od A) x →　Ordinal ) →　Ordinal
　　　sup-o< :　(A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →　Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<　sup-o A ψ

Power Set の odmax が良くわからなかったんですが、⊆ が集合の順序を制約するとすると良い。この方が自然。ただし、⊆→o≤ から c<→o<　はでないらしい。

Union / Replace の上限も「そういえば教科書にそういうの載ってたな」的に証明できる。

最後に無限公理で行き詰まったのですが、

　　Union (x , (x , x))

は順序数との対応で特に上限が指定されてない。なので、どんどん大きくなる可能性がある。濃度とかで抑える方法も考えたんだけど、

　　面倒くさいので、ωはあるってことで仮定

で、治ったようです。ちょっとださいがまあ良い。

sup の定義域にも制限が付いたので、気になっていた(気にしてたならなおせよ)ところはなくなったみたい。

他の部分の証明(ブール代数や filiter、順序対)も大した修正でなく終わりました。

選択公理から排中律が出るところ、その逆、ε induction から正則公理も HOD で問題ないらしい。

超限帰納法のレベルが合わなくて n と suc n と二つあるが、まぁ、いいか。

https://github.com/shinji-kono/zf-in-agda

サージャー

なんか缶に付けて使うタイプ。プレモルの販促品らしい。

油断すると、泡泡になってしまします。

もう少し細かい泡になって欲しいが。

自分は Yebis 派なのでプレモルはあんまり。

父が脳梗塞やった年になったので、気をつけようとは思うんだけど、

　　思うだけでは効果ない

だろうなぁ。Ingress も最近は控え目なので体重がな。

やっぱり、対面な人たち

自分は、そもそもネット野郎なので、今の状況は快適。ずーっと、これでやって欲しい感じ。

なんですが、なんかいろいろ解除されたらしく、

　　来てしまう人たちが

まぁ、追い返しはしないんですが、できればリモートがいいなぁ。でも、 IT系の人たちでも

　　ネット環境がよろしくなくて

的なお話が。やっぱり最初の頃は面白くて顔出ししたりするわけですけどね。帯域がね。

そうか実際に会うと、チャットに記録が残らないのかとか思ったり。

Pure Storage は Zoom で営業してくれて、そういうのはありがたいなと思いました。

Disk

なんか、貼れって言われた気がしたので。

FDD自体はリースバック1万円のを使ってた。ヘッドが「スコーン、スコーン」という感じで動くので気持ちよかったです。

IBMは、ちゃんとドクター中松に特許料払ってたんだよな。

Prometeous

また、なんかかっこいい名前だけど... なんか学生が

　　Zabbix のメンテに疲れた(失敗した)

らしく、こんなものの話が... 妙に燃える学生がいる時もあるけど、log監視システムは埋もれてしまうものだよな。

Zabbix の代わりになるものなのかな。どうせ ping しか見ないなんて話も。まぁ、ねぇ。

なんか今日は珍しくシス管ミーティングをのぞきに来てくれた学生が何人か。最近人気なくて、存亡の危機状態。

なんですが、現メンバーの士気は高いみたい。

9月のシステム更新は楽しそうだ。

https://prometheus.io