歯医者

特にとらぶるはなく、むしろ、絶好調かも。飲みすぎで少し体調悪いにも関わらず。

3/6 以来らしい。だいたい東京にいく直前にいくパターンのようですね。

最初にみてくれた先生、結構、手抜き感じ。まぁ、特にとらぶるないんで良いんですけどね。

歯石は結構あったらしく、わりとがりがりやってました。

iNetSec MP 2040

PFU のネットワーク振る舞い検知システムですね。この手のは研究で流行った時があった気がする。

なんと、学科のネットワークに接続して解析してもらえました。

続々引っかかる

　　PS4のゲーム

ああ、まぁ、そうだよね。無害。

あと。

　　Installcore

悪さをする installer みたいなものらしい。

あとは、

　　Tor

ですね。5月の土曜日に二回。土曜日? なんかロボコン関係のイベントがあったらしく、おそらくは持ち込んだ何かなのではないかと。

割と少なかったかな。うちは Windows がほぼないので、この手のだと結果が良いことが多い。別に Mac に比べて Windows が脆弱ってわけでもないけど。

もはやネットワークは、

　　外側よりも内側が危ない

時代なので Firewall とかがあまり意味ない。意味ないんだけど、やられてしまったものを検知するのは重要。なので、こういうのは良いかな。

UIとかが9801時代感じ(Browser baseの癖に黒に原色な線グラフとか...)。

でも、表示が適切だな。この手のは振る舞いのデータベースが重要なんだけど、PFU頑張ってる感じ。えらい。

単に log 吐くだけのSnortとか意味不明なSELinuxとかより良い感じでした。

まぁ、うちでいれるかと言うと、どうかな。どっちかっていうと、総情センタに置いて欲しいものだな。

https://www.pfu.fujitsu.com/inetsec/products/mp/

リチャージ大会

もはや、cross faction でも良いんじゃないかと思われる ingress event ですが、

　　韓国でのanomalyを、recharge で援助

というわけです。もちろん、

　　青はボロ負け

だったのですが。でも、香港では勝った的な話もあって。

でも、前回よりは rechage しがいはあった感じ。ただ、助けになっていたかどうかは。

ちゃんと作戦建てて、遂行できればなぁ。負け癖付いてると難しいですね。

まぁ、僕は青は居心地良いので、それで十分かな。大域的な勝ち負けはミクロなゲームとは別だから。

さらに、8/3 には、また First Saturday やるらしく。そんなに頑張って、

　　また沖縄に Anomaly 来ちゃったら、どーするんだよ〜

cmake sub project

cmake は、普通に使ってる分には簡単で良いんですが、

　　xv6 の cross compile build に使う

さすがに、いろいろ混迷。mkfs は普通のコマンドだったりするし。

cross compiler の指定とかは cmake コマンドライン オプションで渡すのが良いらしい。CMakeList.txt の実装依存が少し減るので。

まあ、でも、あまり意味はないんですけどね。

usr command の compiler option は kernel のとは別。

さらに、link の command line は、さらに特別。

なので、これらすべてを生成する perl script を書いて、cmake を呼び出すことに。

で、だいたい動いたんですが、

　　user command を含む fs.img を作って、それを kernel にlinkする方式

なんだけど、kernel が先に作られてしまう。add_subdirectory した sub project への dependency はどうするの?

なんですが、生成された Makefile を見ると、top の Makefileに

　　fs.img : ....

とか書いてある。make fs.img とかすると作りにいく。ってことは、

　　add_custom_command {
　　　 DEPENDS fs.img
　　　 ...

で良いらしい。add で定義された TARGET は、top level の Makefile に全部定義されるわけね。

あと、BINARY_DIR とかをちゃんと参照してなくて、off the shelf な build でない。つまり、

　　 mkdir build
　　 (cd build ; cmake ../xv6-source)

みたいな使い方ができないみたい。cmake . だけ。

しかし、うっかり cmake 使ってしまいましたが、それが正解だったかどうかは... 疲れる〜

Printer

Xerox DocuPrint 305 ってのを使っているんですが、なんか、ご機嫌斜め。

　　デンゲンヲオンオフシテクダサイ(010-349)

ですか。赤いボタンじゃないのか。なんと、

　　すぐにonにしてはだめ。少し待ってからonにする

でよみがえったようです。でも、ラベルには 2006 年とあるな。

13年もありがとうございます。感謝の言葉しかないですよ。

まぁ、購入の見積りと卒論修論にしか使ってないんだけど。

授業録画配信システム

ってのを見せてもらったんですが、割と良くできてる。というか、こんなものだよね。なんだが、

AJA HELO

なる機材が。ちょっちょ、それなに?! H.264 とか書いてあるんですけど! 17万円か〜

大学によっては「授業は全部録画義務付け」みたいなところもあるらしく、先生の監視的な側面もあるらしい。それを嫌がってる先生もダサいとは思いますけどね。

https://www.aja.com/products/helo

Nutanix

システム更新絡みで来てもらいました。いや、別にそんなにわらわら来なくても... 沖縄に来たい気持ちはわかりますが。

Nutanix 、どうも、イメージつかめなくて。Nutanix bible なんてのがあるらしい。

VMWare base という印象があったのですが、KVM base の AHV と (おそらくLinux baseの)AOS の組合せが40-50%なんだそうです。

お、virsh できるの? と聞いたら、

　　libvirt に手を入れてるので限られた機能だけ使える

なるほど。うちは virsh-wrapper でやりましたが、そう来るわけですか。で、

　　AHV には login できず、CVM (Control VM)からのみ操作できる

らしい。AHVのFile System にはCVMからmountするという技が可能らしい。なるほどね。Linux だとCVM経由のNFSプロトコルで操作すると。

PCI thru とかの技術もあるらしい。ってことは「なんでもかんでもCVM経由」って感じかな。

KVM base になったのは良いかな。あと、学生にVM作成権限を渡すには、

　　Self service portal

というのが使えるらしいです。テナント用らしい。結構、良くできている。楽そうで良いね〜

Container は基本 VM の中で扱ってくれと言う感じらしい。「Hyperviser には絶対に入らせない」というのがいさぎよい感じ。

VMWare だと中身に触れる感がないんですが、KVMだからな。

これだったら自分で作れそうな気もするが...

ジブリ展

沖縄国立博物館ですね。ここでは OS 研究会やったこともある。

作成時の資料とかポスターもあるんですが、

　　王蟲のモデル
　　猫バス

とかが主なんだろうな。

外にあって無料で見れる

　　ラピュタの飛行機械

のできが良かったです。こっちは写真撮っても良いらしい。

ジブリの森も行きたいとは思うけど... それよりは天気の子でも見に行った方が良いかな。

ε-induction

ちょっと、blog お休みしてました。

まだ、しつこくやってる Agda → ZF ですが、正則公理の minimum が選択公理の choice function になってしまう問題だけど、正則公理

　　∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )

の ∃ y ∈ x が論理式の中に閉じてる時には独立選択公理といって、選択公理よりは弱い公理ならしい。これを、

　　 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
　　 regularity : ∀( x : ZFSet　) → (not : ¬ (x ≈ ∅)) → (　minimul x not　∈ x ∧　(　minimul x not　∩ x　≈ ∅ ) )

みたいにスコーレム関数として要求してしまうと、選択公理になってしまうので、minimulが choice functionなのは正しい。

でも、これでは困るわけですが、直観主義論理用の別な正則公理の表現があって、ε-induction と呼ばれているらしい。

　　 ( ∀ x y → ( x ∋ y → ψ y ) → ψ x ) → (∀ x → ψ x)

古典論理で変形すると普通の正則公理になるらしいです。で、こっちは証明できた。この induction は要するに、

　　集合を空集合から ∋ を逆にたどって任意の集合にたどり着ける

というもの。確かに∋の列には終わりがあるのと似てる。今は OD と順序数の対応があるので、x y に対応する順序数のinductionで証明すれば良い。

なかなかできなかったんですが、順序数は要するに二次元配列なので、それを展開してinductionしてやるとできました。

で、前に power→ 仮定したのは少し気まずくて直観主義論理では禁止されている ¬ ¬ A → A に相当するらしい。

なので、そこは諦めて、

　　power→ :　( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)

ここまでかな。 少し弱いけどAgdaだとここまでらしい。これで、正則公理と選択公理を分離できて全部終了という感じらしいです。

少し文献を探してみると、1974 の Osius and Lawevre の Categorical Set Theory というのがあって、Elementary well-pointed topos (EWPT) ってので、集合論のモデルを作れるとある。こっちは、

　　P : A → Ω

という CCC 上の Power Set Function を使って、Transitive Set Object を作り、それとさらに、A との A ∩ (P A)を取ってSet Object を作ると言う方式らしい。使っている公理が圏論で書かれてるので読みづらいです...

自分のは

　　Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )

なので、近いっちゃ近いかな。Def は transitive なので。

でも Oisus のはモデル論なので、実際に公理の論理式を証明してみせているわけではないけど、
証明論的なのもできるとは書いてあったので、それを確認したと言うこところかな。

満月コント

毎月、満月の夜に首里のコントというお店であるワイン会です。三杯セットでとどめておくと良いが...

珍しく土曜日から酒抜いていたので、三杯までにしておきました。

木曜日はだいたい屋富祖で飲んでますが、明日は、

　　台風の状況によるな

まぁ、多少風があるくらいなら。沖縄の人は台風だと飲みに出ると言う慣習があるみたいだし。

ハリーズ、おばちゃん復活

いろいろ、ありがとうございます。ネーネーたちはスイーツ中心にやっていきたいんだろうなぁ。

割と元気そうでした。

ZF集合論一段落

なんか、前にも一段落と書いた気がするが気にしない。

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

順序数上の述語を集合と見なすのを順序数定義可能集合(Ordinal Definable Set)というわけですが、これが

　OD ≈ Ordinal

という順序同型写像を持つというのと(あと色々な仮定)を入れてZFの公理を証明してやろうというわけですが、

この写像の→は良いんだが←を集合の∈と見なすと「全部の集合が順序数になってしまう」つまり、必ずOD(+仮定)が空集合を含んでしまう。

ってので困ったので←をはずそうっていうわけですね。結構、難航してたんだけど、

　 ¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )　→ p

ってのを入れるってのを思いついたので、一通りできました。直観主義論理なので∃を使えない。なので、対偶を使ってやろうというわけ。

ちなみに証明できてないので仮定。順序数上の定理なので証明できそうな気もするが...

A のPower Set を順序数のPower Setの要素 x を A ∩ x に置換するってのを思いついたのだが、その時に、

置換公理の Elimination が ∃ を要求するのに気がついて、苦し紛れにこれを使いました。

結局、Union もこれで乗り切った。しかし、Union を使う無限公理がおかしなことに。それも適当に乗り切れた。

でも、選択公理を証明しようとしたら、正則公理の minimum がそのまま選択関数になっていることを発見。

まぁ、いろいろ変だが、空集合を含む集合のモデルは作れたみたいなので良しとするかというところですね。

あとやるとすると、

　　濃度の定義
　　連続体仮説
　　選択公理を満たさないモデルの生成(minimumはどうするんだ?)

くらいでしょう。

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

秘密兵器

なんか気がついてなかったんですが、靴の中敷きが新しくなっていたようです。

Ingress 始めて足がぼろぼろになったので、中敷きを使うようになったんですが、

　　代わりに中敷きがぼろぼろ

なにせ、9000km だからな。

まぁ、気がついてなかったくらいなので、まぁ、効果は良くわからないです。

オープンキャンパス

プロ3割と人数はいたんですが最近の学生の「ここまででいいや」という目標が低いのがばっちりでて残念な感じ。

どれも、もう少し頑張れるだろという感じでしたが、まぁ、オープンキャンパスにはちょうど良いのかな。

シス管の方は参加してくれている1年生が来てくれていたのが良かったです。

Oculus Quest の方は「安い」を連呼してて、Holo Lens の方は高いを連呼してたのが少し面白かった。

琉大は少し背伸びしてくるぐらいの方が良い。これから頑張れば琉大とか楽勝で入れる的な話をしてたかも。

なんか群馬から来てくれた人たちも。

今の学生に聞いても何人かはオープンキャンパス見てきましたという人がいるのでがんばりたい感じ。

ハリーズ閉店

いろいろあったハリーズですが、やっぱり閉めることになったようです。五時前に閉めたりとかしてたからなぁ。

ちゃんと儲かる商売やって欲しいと思いますが、開いてないとどうしようもないというか。

復活する説もないことはないらしい。うちの研究室はハリーズで廻っていたところもあるので、

　　ちょっと、困ってます

というわけで、これが最後のハリーズか!

少子化と移民

うん。もう10年前に勝負はついていて、受け入れるしかない感じですね。都市部が先行するので、既に感じている人も多いはず。

　　日本は、もう移民が支える国になっている

別に日本だけじゃなくて、欧米が先行している現象でもあるな。

団塊Jrが自分で選択してきたことだと思う。もはや、それは良い悪いではなくて、

　　少子化と移民をポジティブなものとして受け入れていくしかない

ということだと思います。日本は受け入れるの得意だし。若い移民たちが日本を活気づけてくれる。

別に無理して子供作る必要もない。子供一人産むと一千万円とか面白いと思うけど、あるいはフランスのようにすれば良いだけとも。

でも、それで増えるのは移民の子なので日本人種自体の減少はもう避けられない。

社会の多様性が上がるのは、ある意味では辛いことだけど、全体的に見れば社会全体を良くするはずです。

　　そう思って、そうなるようにがんばるしかない

自分の振る舞いが社会の方向と雰囲気を作っていくので、せいぜい明るく社会の変化を見ていきたいかな。

あ、そうそう。外国語の勉強の必要性が上がることは確かだな。

眼鏡治りました

宜野湾の愛知(っていう沖縄の地名。京都もある)にある眼鏡一番を使いました。だって、

　　そこで買った眼鏡

だから。なんか無料でやってくれるのね。ありがたい。

ついでに予備用の撥ね上げ眼鏡も見てきましたが、2万円から3万円か。ちょっと高いんだよな。

店員さんも「フレームはしっかりしてるから大丈夫」ってことなので購入は見送り。

眼鏡

なんか鼻がいたいなと思ったら、眼鏡の鼻当ての部分が片方ない。ソファに落とした時か、MBPを縦に乗せてしまった時か。

ネジで停まっている部分はそのままでプラスチック部分がはずれたらしい。

　　もしかすると直してもらえるかも

父がちり紙挟んでるのを見たことあるけど、

　　気に入っていた眼鏡だったんだろうな

と今は思います。この撥ね上げは割と調子が良いので直したいが、呼びも欲しい感じ。

ZF集合論 on Agda

順序数を作って、OD (Ordinal Definable Set)を作って、集合論の公理を満たすところまではできたんですが...

どうも全部の集合が順序数になってしまう。record { def = λ x → x o< y } という形が順序数なんですが、

どの集合も、どれかの順序数に一致してしまうらしい。教科書には OD は順序数と順序同型だと書いてはあるんですが、これだと、

　すべての空でない集合がΦ(空集合)を含むことになる ( 0 o< x だから)

いくつかの仮定を削ると避けられるようですけど、結構、証明できない公理が... でも、うっかり仮定を増やすと空集合を含んでしまう。

まぁ、ここまでかな。

録画の整理

まぁ、そういう季節です。今の録画環境は気に入ってはいるんだが、少し高く付いてるかも。8月になると

　　WOWOW一ヶ月分がおまけ

みたいになるはずです。そうする去年やった映画とかが録画できるので便利。

最近は、昔みたいに手間かけてない。でも、この前、リストは作ったのだった。

ナデシコとかオーバーマンとかとかやってるのが懐かしいな。ナデシコはDVD持ってたりするんですが、HDなので綺麗。

でも、当時もアップコンバーターなテレビで観てたので十分綺麗だった。問題は、

　　最近は見る根性がない

ってことね。取りあえずBD-REで一部HDDに放り込んで終わり。出掛けにしかけてという感じです。

Made in Abyss はなんとか見終わりました。
Made in Abyss は一直線にアビスに向かっていくのが面白かった。そういう道を見つけられる人は幸せかもな。
お涙は良いので次が見たい気がします。

が、懸案のサイコパスを見る根性がない。2 が行方不明だ。

Ingress First Saturday

八重瀬町なんですが、南部のど真ん中

　　ポータル全然ない

20万APくらいは取れるだろって思ってそれくらいで調整していったんですが9万APで Lv12 に上げるにの失敗しました。

いや、ちゃんと20万AP上げていた人もいたので、やり方しだいだったらしい。バスターとか足りなかったしな。

その周辺で打ち上げもなので「バスで帰れない」いや、送ってもらったんですが。

え、また来月もやるの?

キャッシュレス

クレカ派です。既に実績のあるものがあるのに、他のものをたくさん入れてリスクを増やしてもな。

iPhone のSuicaも使ってない。Sucia 便利っていう人も多いけど、

　　東京に住んでないなら関係ない

といっても、ゆいレールではようやっと使えるようになるらしい。どういう経緯なのか知りたいところですけど。

Suica はサーバとはその場では通信してなかったりするわけですが、それがVisaのSecurity 基準に満たなかったらしくVisaでは使えない。

もちろん、F1 と同じで、

　　Felica が使えないように、その基準を作ったわけ

だからね。といつつ、Apple は日和ったわけですが。まぁ、iPhone は日本でしか売れてないというのがあるからな。

その iPone を使ったクレジットカード決済もたくさんあって、高い加盟料を払わなくてすむようになっているので、

　　クレカ決済を避ける理由が店にはもうない

と思うんだけど。もっとも○○ペイ系が結構押しているらしく、それが置いてあるお店も多くなってきた感じ。

でもユーザに値段入れさせたりクレカよりも面倒くさくするとか何考えてるんでしょうね。日本はITサービスに関してはだめだめだな。

中国ではQR決済は既に一巡した感じ。後出してダメダメてのが昔の日本と違うところなんだよな。後出し有利なはずなんだけど。

黒い砂漠

PCゲームだったのかな。iPhone でできるので少し手を出してみたんですが、

　　生成できるアバターがかわいい

何人か作れるようになってる。これだけでも楽しい人は楽しいだろうな。

ゲームは適当に撃ってれば良い的な感じで... で、

　　オートモードがある

少しやってて思ったんですが、

　　これってゲームの面白い(はず)のところをやらずに、つまらない事務作業的な部分

だけをやってるんじゃないか? いや、まぁ、

　　釣りやったりとか、何やっても良いゲーム

らしく、結局は、作ったキャラで戦って競うみたいなものだったらしいんですが...

事務作業で挫折。いや、キャラはかわいいんですけどね。

Open Cumpus 準備中

プロ3の授業中心にしたいんですが、今年は時間割の関係とかで、

　　B4 でプロ3取ってるのが...

それは無理筋だろ? 卒研に集中しろよ。まぁ、がんばって。Project driven な緩い授業ではありますが。

来週末 7/13 です。一般の人もふらっと来てもだいじょうなんじゃないかな。例年だと午後は空いてる感じ。

いつものように Unity とか HMD とかシステム管理絡みとかそんなのを出していると思います。

今年もぼっちプロジェクト多いな...

Subject: Brew upgrade で library が消える

うっかり、やってしまったんですが、(ちなみに、まだ、macOS 上げてない。そろそろ上げないと)

　　勝手に、library を消す

ってのをやられて、Agda が

　　% ./dist-2.6.1/build/Agda/agda
　　dyld: Library not loaded: /usr/local/opt/icu4c/lib/libicuuc.63.dylib
　　　Referenced from: /Users/kono/src/public/agda/./dist-2.6.1/build/Agda/agda
　　　Reason: image not found
　　zsh: abort　　　./dist-2.6.1/build/Agda/agda

とか文句を言うように。cabal で build しなおせばよいかと思ったんですが、ちゃんとやってくれない。

で、Time Machine から戻せば良いと思ったんですが... Time Machine は少し前のなら、その場で戻せます。なのだが、

　　/usr の下が Time MachineのFinderから見れない

なんだよそれ。仕方ないので、教官室の外付けHDDを取りに。そっちは、

　　mountすれば、そのまま任意の日付が見れる。しかも、sh から

で、rsync で戻して終わり。

 rsync -av /Volumes/leoBackup2017/Backups.backupdb/lll/2019-07-23-154627/Macintosh\ HD/usr/local/opt/icu4c/lib/libicu* /usr/local/opt/icu4c/lib/

まぁ、いいんだけどさ。たぶん、cabal の configure しなおしみたいなのがあるかも。

メタリックナノパズル

割と良くできてますが、一部、壊れてまいた...

この前買った iPhone 用のマクロレンズ、ちょっと便利

-

柿の種

割と好きです。常備してるかも。学生にばれたのか、研究室にこんなのが。

なんと千円するらしい。通販で箱買いしようかな。

結構もったような気がするが、2週間くらいか?