Photos.app

なんか、340GB くらい食ってるらしく。もっとも、写真だけだと165GBくらい。

普段そんなにみたいわけでもないしなぁ。なので昔やってた

　　iPhoto は最近のPhoto Streamを受けるだけ

ってのに戻そうかと。昔は、iPhoto Library を分割してた。それはそれでめんどくさかったんですが。

340GB空くのは大きい。Photos.app/iCloud Photo libary の残念さは半端じゃないし。

SSDだと1TBでもまだ高いからな。

一時期は面白かったんだけどな。どっかの会社を買い取れば良いだけだと思うんですけどね。そういうの下手なんだよな。

Social Distancing

いろいろ工夫が。でも、食堂のテレビはとばっちりっぽい。パチンコ屋の二階だからかな。

どっちかって言うと、キャッシュレスの方が良いかな。

OS研究会 on Zoom

木曜日したが。 結局、8件。ほんと、

　　いつもの研究会の感じ

いや、

　　拍手しないでいいですから

Zoom の reaction とか、自分も気がついたのは最近だったりしますけどね。

うちの学生の一人の音声が途切れ途切れだった。ネットに自信ないなら大学に来ればよいのに。

大学に来るのは MatterMost での申告制になったみたいです。

　　このまま対面授業は消滅で僕は構いませんです

質問も chat にどんどん書き込んで良いんですけどね。そして、

　　寝っ転がって参加できるとか最高です

でも、Zoom Meeting 疲れるから 8件ぐらいでいいかもね。二日とか無理ぽい。

学生たちは大変だよな。まぁ、さぼりながらでいいからさ。

http://www.ipsj.or.jp/sig/os/index.php?2020%C7%AF5%B7%EE%B8%A6%B5%E6%B2%F1

Haskell

ソフトウェア工学では Haskell やってるんですが、だいぶ慣れたとはいえ、まぁ、いろいろなぁ。

　　学生たちも苦労しているみたい

でも、そういうことができるのは学生のうちだとも思う。

メインが Agda だったりするのもあって、Haskell 力は、なかなか上がらんな。

特に、わからんエラーメッセージなんとかならんの? 努力しているようではあるのだが。

　　*Main> tama = Cat "Tama" "白"
　　*Main> pochi = Dog "Pochi" "茶"
　　*Main> pochi
　　Dog {name = "Pochi", color = "\33590"}
　　*Main> color tama
　　"\30333"

おお、微妙に残念。そろそろ UTF8 default でお願いします。

図書館から借りた Kunen

理学部図書室から連絡が来たので取りに行ってきました。いや、

　　やっぱり物理本は良い

なんだが、ページめくるの面倒くさい。もう暑いから手を良く拭いてからでないと読めないな。

何十年かぶりに

　　図書カード書いてしまいました

いや、いー感じだよね。

集合論の定番の教科書なので、買って手元に置くべきな気もするんですが、

　　この本の半分くらいは Agda で書いた

たので要らんっていう説も。残りの半分、強制法/Filterは、まだできてないんだよな。

知りたかった OD / HOD の話もちゃんと書いてある。構成可能集合よりも先に出てくるのだな。

brew bottle, Xcode, Mojave

昨日の全然動かなかった brew bottle 。

　　(1) github に登録した formula から ruby script で soft を build / install
　　(2) できあがった install image を tgz にまとめる bottle

という風になっていて、(2)でエラーだったんですが、調べていくと

　　popen で git version を取っていく

ところで落ちている。popen と `` の干渉かと思ったんですが、git の version が悪い?

と思って、別ファイルにして version 履歴一つにしたら夜中の二時に通りました。なんだよ、それ〜

作ってるのは GCC/LLVM (の改造版)なんですが、さらに

　　Catalina で build できない

と言う問題が。まぁ、自分たちの改造にもいろいろ問題があるんだがな。でも、

　　Mojave の XCode.app が残ってると悪さをする説

確かに自分も引っかかった。チェックしてエラーを返すべきかもな。

まだ、いろいろ動いてないんですが、方法論は確定した感じ。いや、まだ、先長いかも。

brew bottle と格闘

割と懸案だったんですが、ほっておいたんですが、

　　CbC compiler を brew install できるようにする

ってのがあって。昔、atton にやってもらった気がする。

brew は ruby で書かれていて、packageの作り方とかは ruby script で書く方式。formula とかいうらしい。

formula は github に置いておくと、brew で git_user/repsitoyy みたいな形式で取ってこれます。既に、うちの学科のがある偉い。

Ruby あんまり書かないので、ちょっと苦労したんですが、gcc を build して bottle を作るまでは割と楽勝。

なのだが

　　Catalina の方が動かないらしい (と学生は言っている)

付属の LLVM clang ではだめらしく、clang をbrewで入れてやるらしい。

さらに、

　　GCCのCbC compiler の arm cross compiler

を作ろうとすると、brew install まではいくのだが、brew bottle が落ちる...

　　 arm = `/usr/local/bin/brew --prefix arm-none-eabi-gcc`.chomp
　　 path = `/usr/bin/find #{arm}/ -name stddef.h -print`

この辺が、brew の git の popen と干渉しているらしく... 謎だ〜

https://growi.cr.ie.u-ryukyu.ac.jp/CbC/GCC/homebrew

American Graffiti

これも見てないなと思って。自分の若い頃とは国も時代もずれてる話。

そもそも、ここでかかるロックってのは自分の世代では、時代遅れ、または敵だったような。

男子校から東工大の暗黒時代を突っ走った自分とは違う世界だな。車乗ってるとかいなかったし。

それに関して後悔があるわけではないですが、いろんなのが出てくるけど、

　　男共はもてもてで
　　女性は尻軽で

と言う感じだな。

高校卒業時の選択でいろいろ決まる。自分もそれなりの決意があって... なんか気分はわかるかな。もっとも、時代と場所的には

　　米国の黄金時代が過ぎて、不景気になり始めた頃

みたいな感じ。つまり、日本のバブルが弾けたあたりか。氷河期世代は、また別だろうけど。

ハリソンフォードが二枚目役で出てますが、そんな扱いなのか。

でも「あのドライブイン」がみれるだけで十分な映画なのかも。

https://www.amazon.co.jp/gp/video/detail/B00JEZ8OW8/ref=atv_dp_share_cu_r

ウォータフォールの滝登り

ってのをTwitterで見かけたので。それに「いや、別にウォータフォールは登っちゃだめっていうの入ってないし」ってなコメントが。

元というか紹介されてた論文はロイスの Managing the development of large software system ですね。1970か。いつもの宇宙開発系のソフトウェアをやってた人。

この論文、欧米の論文には珍しく図が多い。式と文章だけで図がないとかの方が普通だったりするからな。

で、図を見ると「一つずつ戻るとのがいいけど、そうもいかないよね」とか「一つのフェーズで残りをシミュレーションしてからでも良いよな、二度やることになるけど」

さらには、テストとかも前の段階から考えておこうとか、顧客を早い段階で巻き込もうとか書いてある。まとも〜

某F社と一緒に仕事した時には「プロジェクト管理について教えてもらえれば」とか言ったら、巨大なプロジェクト管理マニュアルとか持ってこられて。

　　おまえら、何も考えてないだろ〜　今からやるプロジェクトなんだと思ってるんだよ

ってなところでしたが。でも、まぁ、今では、ロイスの手順は一通り理解できます。どんな小さなプロジェクトでも各段階はあるよね。

http://www-scf.usc.edu/~csci201/lectures/Lecture11/royce1970.pdf

tmux and screen

なんとなく Ceph を build しようとしたんですが、cmake なんだけど -G ninja がうまくいかない。

make -j 8 とかするんだが、あんまり並列に動いてくれないんだよな。

なので、back ground にするかってところなんですが、screen かと思ったら入ってないのか。どうせなら、使ったことないもの。

　　yum install tmux

どうもtmux 派結構いる感じ? で、

　　detach どうするの?

あぁ、^-b ね。で、D か。ふむふむ。

で、attach どうするの?

　　tmux attach

なるほど。特に screen に恨みがあるわけではありません。log の先頭に行くとsearchがわからんな。

普段は、どっちも使わない。

　　make >& ers
　　disown
　　tail -f ers

してることが多いです。screen/tmux もキー食うからな。

ラウダン 科学と価値

クーンで停まってるのあれでしょ的な話をTwitterで見かけたので... もっとも、これも既にかなり前。

4章までは、クーンの革命とかパラダイムの方を批判していて、連続的な変化だが急激に起きてるとか、科学者の気が変わらないわけじゃないとか。

部分的に入れ替え可能な網状モデルとかは、ある意味で当たり前なわけで、全体的にはクーンとそれほど対立しているわけではない感じ。

割と普通。この手の議論は科学技術の現場的には各論的に変化しているので「一緒くたな理解」とはそぐわないかな。

ところが、5章では、どちらかと言えば科学哲学の研究者の認識的実在論をばっさり斬りまくる。気持ちよい。

　　科学が実在に沿って発展したからうまくいっている

みたいなのを、後付けとか別に実在と関係ないとかで片付けていく。まぁ、そこで尻切れとんぼ的に終わってしまうんですけどね。

訳者の解説が長いのですが、ラウダンの立場、自然主義とかが説明されてます。でも訳者は実在論よりなのね、

いまどき、物理理論を学んで実在論者でいるのはかなり難しいんじゃないかと思うんだけど。

　　計算もできなければ予言もできない紐理論
　　ラグラジアンとハミルトニアンと観測値の関係としての物理理論
　　高次理論を予想しながら、それを見えないものとして作られた繰り込み理論
　　質量や真空の非対称性から導出する
　　情報論的重力理論

とかに実在としての思い入れってできるの? ラグラジアンとか作用って実在なのか?

解析力学は観測値の相互関係みたいなものを定義するからなぁ。

エイヤーは論理実証主義は死んだみたいに言ってたわけですが、また、物理学者や数学者が引退して哲学者になるといろいろ賑やかになるのかも。

パラダイムに関しては今の

　　検査シーヤ派とスンナ派の議論
　　統計学者のベイジアン的立場の選択
　　BI/リフレ論者とハイパーインフレ論者の喧嘩
　　構成主義的数学の扱い

とかがわかりやすい例になっている気がする。科学哲学は、それらに正しい指針を提供するべきだと思うけど、

　　それほどの成果と理論と説得力を科学哲学は持てなかった

ってのもそうかな。

ラウダン 科学と価値
https://www.amazon.co.jp/gp/product/4326199547/ref=as_li_qf_asin_il_tl?ie=UTF8&tag=shinjkonoshom-22&creative=1211&linkCode=as2&creativeASIN=4326199547&linkId=688121e84ae0927991e4e808834d6d63

レナウン倒産

関係ないと思ってたら、

　　ダーバンとアクアスキュータム

それかぁ。何着か買って着潰しました。ありがとうございました。

作業着だと思ってるので、スーツにそれほど思い入れがあるわけでもないけど。いや、

　　作業着だからこそ思い入れがあるのか?

洋服の青山で買って、即座にぼろぼろにした記憶もある。

Graph to CCC

元ネタの本では1ページなんですけどね。

　Graph → Positive Logic → Sets

はできたので、CCC全体の圏からGraph全体の圏への忘却関手

　Cart → Grph

と組み合せて随伴関手にするわけですが、

　Graph の Set のLevelが合わない

ここで判明したのは CAT (圏全体の圏)も異なるLevelの対象を許さないってこと。Agdaの限界かな。

で、Grph {suc n} から Grph {n} への変換を仮定することに。ダサいけど。

Sets ではなくSetsの部分圏って話はあったのだが、

　　 Hom = λ a b → Hom B (FObj F a) (FObj F b)

だけではηは書けて solution の関手

　　 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c

のFObjまでは書けるんですが、FMap が書けない。

　Graph　1 → Positive Logic 2→ Sets 2
　　　↑　　　　　　　　　　　　　　　　　　　　　 ↓
　Graph　1 ←　 Graph 2　 ←　　　　CCC 2

というのが普遍問題の流れ。

異なるPositive LogicはSetsで同一視されてしまうので情報が消えてしまう。生成手順を覚えてない。なので、部品な射のGraphからCCCを構成できない。

Hom PL を使うとCCCにならないからだめ。結局、

　　　fcat-pl : {a b : Obj PL} → Hom Sets a b → Hom PL a b
　　　fcat-eq :　{a b : Obj PL} → (f : Hom B a b ) → FMap CS (fcat-pl f) ≡ f

を仮定することにしました。

　Graph → PL → Sets

で作ってるんだから元の fcat-pl はあるんだが結果のSetsの射(=関数)から構成的には逆は取れない。

これは CCC の射から Positve Logic の射つまり具体的な証明手順を見つけることに相当するのではないかと。完全性定理ね。

で、それは構成的には証明できないので仮定するしかない。

もちろん Positive Logic なので個々の決定続きはあるんだが任意の対象についての証明は構成的ではないらしい。

そんなところではないかと。これで solution のFMapも一応書けた。まだ、uniquenessもやってないし、穴も多いが、ここまでかな。

　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/tip/CCCGraph.agda

写真の管理

もうカメラもほとんど使わないわけですが、

　　iPhone → Photo Stream → Photos.app
　　iPhone → Google Photos

の二系統です。Photos.app の馬鹿さ加減にはいろいろ困ってるわけですが...

検索は Google Photos でするからいいです。

　　iCloud storage は高すぎる。なので iCloud Photo Library はパス。

でも、backup だけは仕方ない。なのだが、最近、

　　50GBのoptionが追加されたのに気がついた

5GBの無料分ではさすがに無理。いや、がんばればいけるんだが... 130円/月ならまぁ。ちなみに使ってるのは 5.5GB。二人分です。

昔は、iTools にお布施してたんですけどね。iChat とか楽しかったな。会員制クラブ的な。

なんですが、Photos.app のだめな DB から hard link で日付別なfolderにマップしてるんだが...

　　なんか、また日付がずれてる。しかも、HEIC

この前、HEIC 切ったと思ったんだが。また、元に戻ってるのか。まぁ、HEIC でもJPGでもいいけどさ。

読み込みの日付ではなく exif 見てるはずなんだが...

いや、ずれてるのは Photos.app が管理してる方だ。link した方はちゃんとしてる。

キーボード

まぁ、あんまりこだわらない方です。今の

　　ストロークの浅い MBP のキーボード

は気に入ってます。嫌いな人もいるみたいだっが疲れなくて良い。

ただし「esc が物理キーボードでない」のがな。Emacs/vi ユーザには致命的。

まぁ、touch bar に固定で出してるので、それほどでもないかな。

有線派なので無線キーボードは嫌い。電池切れるし。最近のAppleのキーボードは有線でも使えるの? なら買うか?

院生時代はVT(といってもCITなやつ)で、超深いストローク。これはこれで楽しい。

　　ADM3AのキーボードとディスプレイでのRogueの味わい

ね。CITも500とか600ではかなりストロークがあさくなってて。

Sun3/50 のType III、NeXT Cube のキーも良かった。あれも長く使った。94年まではそれだったかも。

でも、

　　Libretto 50 のキーボード

長く使ってなかったか? 4年くらいそれだった気もする。そんなもので平気なら

　　本当になんでも平気

だよね。学生は HHK だの Realforce だの言ってますが、

　　無刻印のDovrakとかは僕は打たないからな

いや、まだ、OASYS は打てるかも知れん。親指ぴゅんは、Dynabook 時代は打ってたかも。

　　でも、JISかなは打てません

でも、最初の自作機とかPC8001/if800はJISかななんだよな。

JISかななキー刻印だがASCIIな配列のキーボードを打つのが得意かも。サーバ落ちた時は、そればっかり打っていた。

なんでもありです。

YMO

自分はそれほどは。ジュリアナとかクラブ系につながっていくわけですが... 最初の

　　スペースインベーダーの音を真似る

辺りとか、Cosmic Surfing あたりとか。また、あの面子がやらかしてるなくらいで。

増殖あたりが盛り上がってたけど、体操とかは嫌いでさ。沖縄音楽系とかは迷走してる感じで...

電子音楽だけど、毎回音が違うので、あのversionが好きだったのにが探せない残念さがある。

去年のお正月もなんかやってたんだよな〜

ケムール星人にやられてしまった跡

沖縄では良くある

Rust

プログラミング言語ですね。mkdir ~/src/rust ってやったら既にあるとか言われた。1/27 くらいに一度やったらしい。

rustc でコンパイルして、 cargo ってのがあって、cargo built で module 作れるってところまでは見ました。

mut で mutable の宣言か。const 書きまくる C++ よりは良いかも。

rust-lldb で debug ですか。はいはい。

ってのをやるくらい修士の授業が盛り下がって暇でした。もう少しRustやっても良いかな。

今年は Ceph 読もうかと思ってるんですが、誰も準備してくれないらしい。

プログラミングIV

いつもの「自分で好きなプロジェクト」な授業です。フライング気味に始めた遠隔授業で

　　基本的な技術としてWeb Service一つ上げよう。あ、OAuth でユーザ管理くらいしてね

で始めてるわけですが、

　　どうせなら、面白いフレームワーク使ってやろう。Rails/Java 禁止な。

だったんですが、結構、面白かったです。

　　Unity / WebGL
　　golang / gin
　　Haskell / Yesod
　　Elixir / phoenix

むしろ、node.js とか Django とかは古くみえたりするな。 こういうのって、

　　時間と資源あげて勝手にやれ

がよいんだよね。いや、それは授業とは言えないけど、大学でやるべきことはそういうものだと思う。確かに、自分もそうだった。

そういうことをやらせてくれた人がいたってこと。

オンライン授業だと課題出しすぎになることが多くて、OSの授業もそういうところがあるんですが、

　　優秀な学生は好きにさせるのが一番

な気がする。

もともと、教室でTreeVNCで画面切り替えでプレゼンとかやってたので、遠隔授業でもいつもと変わらない感じでもあるな。

いや、なんか「お、自分が音声聞こえない、ちょっと待って」で reboot とかあったんですが、そんなのトラブルとは言わないな。

https://ie.u-ryukyu.ac.jp/programming3/

Zoom 中継

昨日のサーバ復旧は、

　　全部、Zoom 中継されていたらしく

まぁ、だれが見ていたかは知らないんですけどね。

ぶつぶついいながら、ググりながらキーボード打ってる後ろ姿だけだけど。

　　「お、通った」
　　「やっぱり、だめだ」
　　「わからん」
　　「わかった?」
　　「でなにすればいいの?」
　　「pcs constraint show」
　　「先生、見えてます」
　　「え、なんで」
　　「なにもしてないのに動いた」

サーバ復旧

まぁ、実働時間の大半は

　　gfs2 の fsck 7 時間

なんですけどね。初期のエラーは「could not mount /mnt/whisky」なので、fsckというわけ。

Zoom / MatterMost (MatterMost はサクラにあるので見れる) で最初は remote で。 fsck 入れてで、

　　「ちょ、ちょっ、そこ別なのノードから FS が見えてるじゃん」

他のノードが見えてる時に fsck してはいけません。普通は他のノードを落として fence を入れて fsck らしい。

で、午後5時くらいに fsck は終わったんですが、

　　pcs status で node b (burbeny) の dlm が FAILED

で動きません状態。はぁ? ググりながらなんですが、昔懐かしい atton の blog が引っかかる。素晴らしい。

　　全部のノードでpcs cluster stop した。
　　しかし一つは止まらない。
　　pcs cluster start —all
　　node b のdlm FAILED で止まる
　　pcsd をsystemd で再起動
　　もう一度、pcs cluster start —all でダメ
　　pcs resource failcount reset をすべての資源に実行
　　node b の dlm を systemctl で止めたが停まらない
　　node b の dlm を kill -9

しばらくしたらgfs2が見えたんですが、何が効いたのかは不明です。午前中の「別なノードからFSが見えてる」段階で治ってたかも。

というわけで、シス管のみなさんお疲れ様でした。

https://attonblog.blogspot.com/2015/11/centos7-hacluster-gfs2.html

システムトラブル

なんかやらかしました...

うちのシステムは4台構成で一台はOSの課題専門だったりするんですが、残り三台は KVM / GFS2 で使ってます。

9月には次のシステムが来てしまうので、

　1台はずして、そこに構築しよう

ってことなんですが、pcs ではずして接続してとかやってるうちに、

　GFS2 が全部落ちた

あぁ、GFS2 は、そういうところがあるんだよ。まぁ、ハードが壊れたわけじゃないから、がんばって治せばよいんだが、

　かなりめんどくさい

です。

うちは、GMail/MatterMost ですが、GMail はDNSが生きてれば大丈夫。DNSはサクラ上なので大丈夫らしい。

なのだが、MatterMostの認証をする GitLab が落ちてるので

　MatterMost をlogoutしてしまうと再ログインできない

らしい。なので、もしはずれちゃったら Slack の方を使ってください。

いろいろ、すみません。復旧予定は未定です。mount できたとか、fsck できないとか言ってるな。

まぁ、2台だから、だめだったら手動 mount でいいよ...

minimum, ε-induction, choice

ZF と ZFC は分離するべきだよなと思って、少しいじったんですが、

sup は常に ord→od の形で使っていることに気がついた。OD は順序数方程式なので「全部が解」という最大値があるので、ord→od には最大値がある。

なので、常にsupがあるわけね。なのでそう書き直しましたが

ZFSet : OD

には変わりはない。ZFSet には最大値つまり順序数全体は入らないわけですが、ここだと入りそうな気がする。しかし、仮定からは OD の最大値がある。

この辺は少し変。でも、そういうものなのだろう。

正則公理の存在記号を関数に置き換えると、実は選択公理と同じになってしまう。その代わり、ε-induction が使えるんですが、

正則公理を 、ε-induction から出すには選択公理が必要。でも実際にやってはいなかった。なので、やってみることに。

が、いがいにかたい。ε-inductionはすべての集合で、自分の要素で成立している仮定で証明できれば全部の集合で成り立つというもの。

OD ではもちろん TransFinite から出るんですが、それより制限がきつい。正則公理の minmam は共通集合なので TransFinite では使えるが、ε-induction　ではだめ。

なので、ちょっとチートしてぐぐったら、

　自分を含む集合で成立するのを induciton すれば良い

ってのが出てて、それでできました。なるほどね。これだと自分を含むから空集合でないのは自明だし。

ただし、選択公理は使いまくり。まぁ、選択公理の別形式を証明しているようなものだからな。排中律も使うし。

圏論は、この手の構成的でない推論を区別しながら展開できる。そのたのツールなのかも。

コーエン先生の本には「選択公理や連続体仮説を仮定しない数学が展開されるようになる」と書いてますが、圏論がそういうものだったんだろうな。

集合は扱いづらいしね。集合論は残りは Cardinals と Filterを使ったモデルだが、どこまでやるかは謎。

そういえば、Agda で構成した ZF は選択公理抜き。ただし、ODは整列されてる。しかし、排中律抜きには、そこから順序を取り出すことはできない、そんな感じみたい。

順序数は全順序だからな。

クロスロード

クリームの曲ではなくて、災害時のいろんな決断をシミュレーションするゲームみたいなものです。

　3千人いる避難所に2千食の非常食が届いた。今配る?

みたいな奴ですね。

　正解を当てるゲームではありません

コロナ禍でも、いろんな決断があるわけだが、どれも正解があるわけじゃない。でも、極端なものが正解になるわけでもない。

　強力な封鎖を2ヶ月すれば収まる
　どのみち5-10%死ぬんだから何しても同じ

みたいな奴ね。

　コロナ禍は罰じゃない

ので、自粛でしおらしくしたり、マスクで苦しいジョギングしたりしても、収まらない。

悲嘆期の反応でみんな気が立ってるのはわかるけど

　みんながおなんじようにしなれば罰するべき

みたいなものとは違う。むしろ、いろんな場所でいろいろ試して、うまくいったものを真似するくらいがいいかな。

米国の真似をするのはやめて欲しいです...

http://www.bousai.go.jp/kohou/kouhoubousai/h20/11/special_02_1.html

岩波の現代数学概説 I

実家から回収してきたものの一つ。冒頭にいきなり

　　今は集合論とかは重要ではなくて、射とか可換とかの圏論の考えが大切

とか書いてある。でも選択公理は使うのでずるいんですけどね。

引っかかったのはテンソルのところだが、章の冒頭に

　　多重線型写像

って書いてあるじゃん。それがテンソルのこと。なのだが、なんとテンソルの定義は出てこない。だって、多重線型写像という言葉で十分だから。

で、Tensor積の話に突入。今読むとするするわかる。だって圏論しこたまやったし。要するに、

　　積の定義の可換性と uniquness をチェックしているだけだ

学部生の頃は、何しているのかさっぱりだったのに。

紙も残念でばりばりに酸化してしまってる。なんかすると防げるらしいんですけどね。いろいろ残念な本だった...

物理の教科書の方でも、数学の方でも「テンソルは多重線型写像のこと」って、はっきり書いてあるのがなくてな〜

現代数学概説〈1〉 (現代数学 1)

OS研究会はオンライン

5月は沖縄でやる予定だったんですけどね。別にすかすかの会場でやれば良いじゃんと思う方ですが、

　うちから三件

出します。(が、まだ、一件でてない。おい) なので沖縄っぽいと言えばそうかも。

ついでに Zoom 宴会もするか〜

Union in ZF

集合論の話。(いや、最近はCCCの方をいじってて、進捗あったようなないような状態なんですが)

Agda で書いた ZF のモデル、そういえば選択公理を分離しておいた方が良いなとか思って見直したんですが(逃避ともいう)

　Union (A , B) ⇔ A ∪ B

とかをBool代数関連で証明してるんだが、なんか選択公理を使うとある。え? それは変だろ。まぁ、右辺を左辺で定義すれば良いんですが、右辺は、

　(x ∈ A ) ∨ (x ∈ B)

で、( A , B ) は A と B の非順序対、つまり、A と B を要素とする集合だな。いや、当たり前に成立するべきでしょ。

なのだが、Union の公理は

∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))

これで、∃ を関数で書いて

　　 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
　　 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))

としてます。¬ で右辺の ∃ を逃げてる感じ。なので、Union (A , B) → A ∪ B を書き下すと

　　¬ ¬ ( x ∈ A ∨ x ∈ B )

となり二重否定を解除する必要がある。でも、

　　直観主義論理だと二重否定は解除できないが、選択公理があればできる

なので選択公理が必要ならしい。

で、なんとか手に入れた Kunen 先生の本を見直してみると、

　　 ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z

しかない。え? 片方だけ? 双方向じゃないの? どういうこと? いろいろ見直してみると、

　　田中先生の公理論的集合論は⇔
　　コーエン先生の連続体仮説は⇔
　　Wikipediaは⇔
　　シェーンフィールドは分出公理と置換公理からUnionを作る

みたいな感じ。やっぱり双方向だよな。古典論理だと二重否定は解除できるのでこれで問題ない。でも、自分のやり方は直観主義論理だから困る。

Kunen は pair と Power Set も片方向なんですが、そこで思いついた。Kunen先生の pari の公理、

　　∃ p → x ∈ p ∧ y ∈ p

だと、他にも要素が入ってることを排除できないので片方向なのだが、分出公理でさらに限定すれば良い。分出公理は双方だから逆も言える。

UnionもPower Setも同じ方法が使えるかも。で、読み進めてみると、

　{ z ∈ p | z = x ∨ z = y }

という形で使うらしい。この形は分出公理そのものなので、やっぱりそういうことか。

この方法だと、入力に使うと条件に否定が付くので自分が書いたのと同じになる。つまり、

　　Kunen先生の本の定義は、直観主義論理にも対応した形になっている

ってこと。さすがです。Kunen 先生。

https:www.amazon.com/dp/0444868399

Singularity

学生の演習向きの Docker ないのって話をしていたらB4の学生が見つけ来たもの。Conatiner に良くそんなかっこいい名前付けるな。

https://sylabs.io/docs/

割と良さそう。

彼自身は、演習用Dockerを管理する Whale Mountain なんての作ってくれているらしく。「そのUse case図はいいけどさ、それ全部作るの?」

　「いや、ほとんどできてます」

え?

　「コロナでひまで暇ひましょうがなかったので」

創造的な人に必要なのは＊時間＊なんだよな。なんとなく、いろいろ身につけてもらいたくて、いろいろ用意してしまうが。

　「いや、ほとんど借りものなので」

それができるのは、実はすごい。

16:9 vs 4:3

未来少年コナンは 16:9 のトリミングだったのでがっかりです。ナディアは4:3だったのに。

4:3の時の隙間になんか模様を出すのとかあってなぁ。あれは残念。昔は、

　　ブラウン管の焼き付き

とかあったんですけどね。今もスマホの画面の焼き付きとか気にしている人いるんだろうか?

もっとも、最近のネットの動画はかなり画質悪くて、HDとか書いてあってもぼろぼろだったり。

まぁ、学生はあんまり気にしてないみたい。そういえば研究室のテレビの縦線も放置のままだ。

もっとも、研究室に学生が来るのもだいぶ先かぁ。

Ingress First Saturday Okinawa 5/2

土曜日の話。本当は琉大の予定だったんですが。

　　おうち FS

ということに。

ってのが4/30に決まって。ま、

　　Zoom 飲み会

ですよね。で、 Niantic 公認 Recharge 大会と。PlSP の司会、長丁場なのにがんばるなあ。いや、もちろん、

　　本職

だからなんですが。しかし、ギャラは出ない的な。すみません。いつもありがとうございます。

Recharge 大会、結構、本気な人たちが。いったい、そのPower Cubeとキーをどうやって貯め込んでいたのか。

キーだけは無駄にたくさん持ってるんですが、LPC(もうLPCではない)が10個ぐらいしかなかったので、そんなような順位でした。

いろんなところで開かれていたみたいですね。沖縄はアノマリーもあるはずだったんだよな。

猫密

こうしてると仲良さそうだが...

マイナーナンバーポータル

がんばってみました。iPhone 7+ なのでカード読み取りできる。まず、login から。

　　噂通り、ぜんぜん、読み取れない

iPhone の充電ケーブルを抜くと気持ち確率が上がるような気がする。10回に1回成功するような感じ。

で、login すると、

　　でっかく「close」ボタンがあるページが

ここで close を押すと最初からやり直し。このページから抜けるやり方は良くわからない。Menu ではないらしい。上のバナーかな?

メールアドレスは二回入力で、二回目はコピペさせない方式。さすが、いじわるも年季が入ってますね。しかし、メールは送ってこない。

なんかすると抜けて、ポータルのトップページへ。そこからサービスを探して、その給付金何とかを選択。

そこでいろいろ入力して、

　　もう一回、カード読み取り

ここで、Web からアプリが起動されて、そこで PIN を入れて読み取りなんだが、もちろん

　　読み取り10回に挑戦する

んですが、そこで PIN がロックされましたを食らいました。3文字くらいでloginしてしまうことがあるらしく、そんなのが

　　3回の間違いにカウントされた

らしい。市役所にいかないと解除できないらしいです。ゲームオーバーだな。4文字暗証番号は何種類かあって

　　確実に間違えてロックするようにUIを設計した

ようです。やるな。

ちなみに、

　　この作業にタイムアウトもある

らしいです。がんばれ〜