⊆

集合の包含関係なんですが、Agda で、

　　_⊆_ :　( A B : OD　 ) → ∀{ x : OD　} →　Set n
　　_⊆_ A B {x} = A ∋ x →　B ∋ x

を使ってたんですが、変数 x がうっとうしい。省略可能にしてるんだけど消せないんだよな。

プロシンの発表資料書かないといけないので、twitter でぶつぶついいながらやってたら、record にすれば良いってのが降ってきました。

　　record _⊆_ ( A B : OD ) : Set (suc n) where
　　　field
　　　　 incl : { x : OD } → A ∋ x →　B ∋ x

なるほどね。∀を隠すのはこうするのか。

　 ⊆-trans :　{a b c x : OD}　→　_⊆_ a b {x}　→　 _⊆_ b c {x}　→　 _⊆_ a c {x}　　
　 ⊆-trans a⊆b b⊆c a∋x　= b⊆c (a⊆b a∋x)

が、

　 ⊆-trans :　{a b c : OD}　→　a ⊆ b　→　 b ⊆ c　→ a ⊆ c　　
　 ⊆-trans a⊆b b⊆c = record { incl = λ a∋x →　incl b⊆c (incl a⊆b a∋x) }

おお、まとも。この手の「二項関係を data や record で表す」ってのは面白い。

東京のIngress

昨日は研究室OBと渋谷でビール飲みまくってました。最後は新宿ゴールデン街にいたっぽい。

そこから高田馬場まで歩いてからタクったので割とタクシー代は安上がりだった。

最近は東京は緑が強いみたいですね。もっとも要町周辺は青い。レゾ差しは結局2020ぐらいまでいったようです。

でも、既に都内だと、もはや廻るところがなぁ。江戸川橋周辺を廻りましたが、1時間くらいで「ここ、前に来たよ」な感じ．

UPV/UPC だと、もう少し遠征しないとだめかな。

ガザ法要

怪しい爺さんたちの怪しいもの探検の一貫です。イスラエルのガザ侵攻に関連する戦争犠牲者を法要するのに参加してきました。

　　お経を上げながら犠牲者の名前を読み上げる

というもの。平和記念公園の名前みたいなものだな。お経は天台宗由来です。政治的なものでなく、宗教的なものだというのが自分の理解だな。

いや、まぁ、なんか、ロックというかパンクというかそういうイベントです。アラビックではなくて片仮名なので読み上げるのは簡単。

1500人くらいらしいんですが、1時間半くらい。あとは、パレスチナ料理での精進落としです。

いろんな解釈があると思うんだが、

　　宗教とは人が明確な意図を持って作り上げるものと自覚する

というのが素晴らしい。人は自然や現象からいろいろなものを読み取るのだが、それはあくまで人が読み取ったものと自覚する必要がある。

そこを諦めたらダメだと思うんだよな。この人工的に作られたキメラみたいな儀式には、もちろん科学的な意味とかはない。しかし、

　　名前を読み上げることで、因果的に、ガザのその場にいた個人個人とつながる

というのが反証し得ない事実として自分に起きる。この感覚は、まさに宗教的なものだと思う。自分的には、それは、

　　量子力学的な現象、つまり、観測とかそういうもの

だと思うのだけど。なので、もっと、

　　名前がちゃんと原語で書いてあったり、発音指導があったりする

方がそういうつながり的なものは強化されるような気がするが、一方で、読み上げると言うこと自体が重要で正確さとかは関係ない気もする。

そこに、声明を入れる意味があるのかってのは記号論的にはないんだけど、別な効果がある感じ。波動的なものが関係するのかなぁ。

こういうのを神妙に粛々と行うってのが必要なことであり、尊重するべきものだというのは、科学とは別だが、重要だと感じています。

http://zipangu.com/sakurai/

パンツと靴下

実家に置いていたパンツと靴下は捨てられてました。シャツとワイシャツはだいじょうぶだった。

なので買いにでるのだが、どこで売ってるのか良くわからないんだよな。昔はヨウカ堂とかあったんだけど。

丸井に入ってみたんですが、なんかブランドものだし、

　　靴下の色がが少しずつ全部違う

いや、そうじゃなくて「5足で千円で、全部、同じ色」みたいなのが欲しいんですが。

結局、東武の中のユニクロへ。まぁ、そういうことかな。なんですが、

　　パンツのMとLがどっちかわからない

自分で買ったのずいぶん昔だからな。ウエスト84cmが境界らしい。いや、わからん。店員さんに聞いたら、

　　見本があるから見ればわかる

いや、わからんし。じゃぁ、どうすればいいんですかって、いや、

　　「メジャー持ってないですか? 計ってもらえます?」

で、計ってもらったら86cmでした。くそ〜　昔は76cmだったのにな。

東京

さすがに那覇空港が混んでて、入場の行列が真ん中のところまで。入口は両端なのに。「間に合わん」とか言ってったら「先頭にいけ」と並んでいる人が。

まぁ、やるか。で、行ったんですが、JGCのカード見せたら「優先搭乗なので行ってください」で、優先搭乗ゲートはがらがら。

う、それってどうなのかな。優先搭乗させれば良いわけで、一般搭乗も処理した方が良いんじゃないの? OSのタスクスケジューラー的にはさ。

で、入ってみると出発は30分遅れで結局楽勝でした。

途中結構揺れたけど、そんなに長くは揺れなかった。羽田は強風で滑走路閉鎖があったみたいですね。

で、寒い。Ingress で手がかじかむ。レゾ差し1440は、東京では一日で終わるみたいですが、レゾが足りんな。

スターウォーズ ep9

見てきたので、ネタバレバリアー展開終了ってなところです。西海岸パルコは、あの程度でちょうど良い混雑か。いや、映画館はガラ空きだったんですが。

話はね。きっとハリウッドには深い意味のある話は作ってはいけないって法律でもあるんでしょう。くそじじい万歳。

あとは、学生とちいちいぱっぱしてました。Rakudo の Configure.pl に

　　Darwinだったら、ar/ld/ccが GNUでなかったらエラーで叩き落とす

ってなコードが入っていてひどいと思いました。

プチエトワール

なんか、三年連続でクリスマスディナーはここだったらしい。近所に歩いているいける、こういうレストランがあるだけで素晴らしいです。

まぁ、ここに歩いていくのは沖縄では自分一人だけかもしれん。夜がいっぱいの時はお昼はお休みらしいです。

今年は、お店の前の道が半年くらい工事で不通。なので余計に隠れ家レストランになっていたようです。

歩いていく分には問題なかったんですが。良いお店は通わないとね。

キジムナー

建築事務所のマスコットらしい。Ingress のポータル。

だいぶ頭がはげてきてるんだよな。

帽子を被らせているのは正しい。

png on LaTeX

なんか学生が苦戦しているので...

　　LaTeX Error: Cannot determine size of graphic in FILE.png (no BoundingBox).

あぁ、それ。-shell-escape を付ければ良いんだよと言ったんですが、なんかだめ。

2014のTeXLiveかなんかを参照してたので削除して brew reinstall mactex したんですが、だめ。

いろいろググって、見つけたのがこれ。これで解決ですよ。くそ〜

　　画像ファイル名から、ドットを削除する

https://ez-net.jp/article/93/Xalaor1B/_KAV6LiFINyt/

経塚駅

てだこ浦西もかなり謎なんですが、経塚駅はなぁ...

　　駅の裏はお墓な山
　　反対側は安波茶まで住宅街

そして、厚生園のバス停は、その山を越えたところ。いろいろ調べましたが、人が通れる抜け道はないっぽい。

ここには友利さんのレストランがあるわけですが、経塚駅からいくのは実用的はない感じだなぁ。

ちなみに、少しゆいれーるが曲がっているのもお墓の関係らしいです。

Why と聞くな

これで思い出すのは、石原藤夫の宇宙船オロモルフ号の冒険です。

オモロルフ号に表れた謎の宇宙人、これが会議室にいて、それを廻りで「どんな質問するか」という議論。そこで部長が制止を聞かず、

　　「何故、ここに来たのか」

と聞いてしまい、宇宙人はそこで溶解してしまう。残ったのは回転を表す公式! それは回転するブラックホールのこと9だった的なお話。

だから、Why と聞くなと言ったのに的な。How とか What とか使えと。

オモロルフは複素関数の正則性を表す言葉らしいんですが、それを使ってる数学書を読んだことはないです。

あと出てくる数学は複素関数論とかカタストロフィ─とか。

このあと、石原氏はシロートの数学談義なファンレターをさんざん受けとることになったらしい。

この話は、もちろん、ボークトの宇宙船ビーグル号の冒険の数学パロディなのですが、会議ネタは当時の研究所のそれらしいです。

https://www.amazon.co.jp/dp/4150301913

docker の演習

なんか面白いのないかなってことなんですが... マイクロサービスっぽいものが良いかということで、適当にググったら、

　　gRPC の呼び出し

なんてのが。それを元に作ってみました。 最近は、docker-compose で複数の docker を上げるのか。しかも、

　　状態をcopyして取っておいてくれる

ふーん。昔のDockerっぽくないな。

　　hg pull して、docker-compose up --build で終わり

おっと、

　　docker-compose rm

を忘れずに。でも、これって、中身読んでもらえるのかな。

昔、並列オブジェクト指向やってた頃は「RPCはダメだよね」って議論してて、Restful Web Service でも「RPCはダメだよね」って話で。

それで、今更、

　　マイクロサービスを RPC でやってるの?

この時代に逆行する感じなのなんとかならないのかなぁ。IBMは stream とか昔やってたはずだが。

IBMのやってる良さそうなものは広まらないというジンクスか。Eclipse とか。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Docker/GRPCTest/

暑い

なんか昨日今日と28度あったらしく。

大学に行く時に一つ早めにバスを降りて、ポータル取りに行くんですが、

　　汗かいて大学で着替える羽目に

なんか、詰め物が取れたので、明日はまた歯医者に行ってきます。

オーバーマン キングゲイナー

昔、まだRD-Z1使っていた頃に観たはずなんですが、

　　最終回前を録画し損ねていた

なんか、いきなり敵味方が逆転していて。AT-X で珍しく再放映していたので見直し。

ちゃんと観れたんですが「いきなり敵味方が逆転」しただけでした。あだだだ。

当時は割と名作だと思ったのだが、あれはなんだったのか。

状況とか道具立ては面白いんだけど、まとまらずに富野節でおいていかれる感じ。まぁ、御大はそういう芸風なんですが。

てだこ浦西駅の使い方

だいぶわかってきたかも。主に那覇琉大で使うわけですが...

(1) 高速バス
　　私道経由での乗り換えが早い
　　ただ、案内板とかまったくない。県庁前からだと、高速バスだけがわかりやすいかも
　　古島乗り換えとかも使えるので選択肢が広い。その分、使うのが難しい感じか
　　古島乗り換えやんばる急行とか。

(2) 125上りからの乗り換え
　　西原入口から私道経由がやっぱり早い。夜は鎖張られちゃうので微妙。
　　時間的には儀保乗り換えと変わらないかも。

(3) 125/56下りへの乗り換え
　　終バスが早いので、まったく実用的でないです。タクった方がまし。
　　56は、まだ遅いのあるが...
　　だったら駐車場から出てバス通りでタクシーを捕まえる方が良い。少し安くなるし。

(4) 97上りからの乗り換え
　　西原入口から私道経由でしょ? Ingress で取りたいポータルがある時しか使わない。

(5) 97下りへの乗り換え
　　例の橋の途中のバス停を使えってことらしい。駐車場から出て結構歩く感じか。
　　琉大に行くなら高速バスが20分以上早いので論外。20分に一本はあるし。

(6) 56上りへの乗り換え
　　浦添前田だと駅降りてすぐ。本数も割とある。てだこ駅は論外。
　　どこに行くかと言うと大平とかなのであまり使わないかも。

結局、(1),(2)を良く使ってます。

いや、Ingress もあるからな。いろいろ使ってます。那覇からのタクシー代節約だけでもかなりうれしい。

写真は高速バス下りへの入口。黄色の柱のところから右に曲がれます。

英語の語彙数

いや、結構、sensitive な話題かも。

語彙集・・・・・Nativeレベル
5万　　　　　　　　　成人(50k幅大)
3万　　プロの通訳
2万　　難関院留学　　GRE、GMAT(この付近)
1.5万　院留学、難関大留学 　SAT(この付近)　　小学生辞書例
1万　　英検1級(12～15k)　 　アルク12000　 (7歳以上6k、9-12歳16k)
9000
8000　大学留学、駐在員　　　英検準1級(7.5～10k)..　新JACET8000 (神大)
7000　業務の一般目標(私見)　　　　　　　　　　　　 　　　　　
6000　難関大入試(5～6k)
5000　一般大入試(4～5k)　　英検2級(5k～)　　　　　AWL(GSL3.5k+AWL1.5kとみて)
4000　　　　　　　　　　　　　　　　　　　　　　　　　 　　　　　.GSL(3.5kとみて)
3000　高校必修(1.2k+1.8k 神大)　　　　　　 　　　　　　 Oxford3000米
2000.　　　　　　　　　　　　　　　　　　　　　　　　　　　　　 　Longman2000　Macmillan2500
1000　中学必修(1.2k 神大) 　　　　　　　　　　 　　　　　 .VOA Special 1500
　　　　高知教委、教科書6社(H28～31年度)

とか Web には書いてあるんですけどね。要するに、

　　高校必修三千と英検準一級八千

に結構ギャップがある。琉大だと三千で合格してるかも... なので「今の大学入試ではダメで民間試験」って話が出るのだと思います。

1万以上に上げるのはやっぱり時間がかかる。大学4年はそういう時間なのだと思うけど学生にそういう自覚がないのがなぁ。

飛行機の中で辞書引きまくってた頃を思い出すが... なんかペンみたいなOCRな辞書ってのがあったんだよな。今ではiPhoneかざして終わりか。

Web 上のテストがあるんだけど、なんか結果が安定しなくてなぁ。考えない方が点が良ってのはどうなの? 2万とか出たような気もするが気のせいかも。

こういうの見ると漢字が3千とかあってもだから何っても気もする。要するに

　　自然言語って不必要に複雑なんじゃないか?

ってのはあるかも。この辺を乗り越えると人類は次の階梯に進める、なんてことはないんだろうけど...

https://uwl.weblio.jp/vocab-index

歯医者さん

一応、ブリッジ再建で終了。なんか、飾りが付いてるな。昔の単なる金属の橋ってのが気に入っていたのだが。

最初に見てもらった時は調子いいとか言ってたが、今年は二ヶ所治す羽目に。

だんだん、ダメになっていくってことね。

それでも上の世代の歯の悪さに比べればましな方なんだよな。下の世代は、もっと丈夫な歯なはずなのでうらやましいです。

iPhone cameta shutter

Short cut 以外にも Timer とか音声も試してみました。音声はみっともない感じ。

カメラのアプリによってはズームとか画角の設定ができないものもある。

なんかだんだ Apple のが良くできてるってことね。

そういえば、イヤホンのボタンが使える説が。

付属の中間に付いてる白い棒みたいなの。あれを

　　背面側を折る感じで押す

でシャッターが切れる。これが便利かな。

自動でシャッター切って欲しかったが。

さば定

だんだん、どうでも良くなっていると言うか... 昔は、Joyful は絶対拒否みたいな感じで、まぁ、いまでもだいたいそうなんですが...

　　焼きサバ定食

になんとなく、はまってます。近いしな。いや、サバ美味いし。

昔、愛用していた美童(みやらび/ボンジュール)にもサバ味噌とサバのフライの定食があって、美味しかったんだよな。

確か、その時の料理のネーネーはサンエーに引き抜かれたはずなのだが... まさかな。

首里城再建 @ Ingress

那覇に首里城アートを作るcross factionな作戦です。緑主導なので、作戦が丁寧。

最初は廻りに六角形のガードリンク張るとか言ってたんですが、当日の朝にあっさり撤回。いや、青の全力なら可能なんですが...

　　主なのはそっちじゃない

この辺の判断が的確で早いのが素晴らしい。

あと作戦の指示書がわかりやすい。いや、Google Spread Sheet とかは読みませんけどね。

どうも前の作戦でポータルの取り違えが頻発したらしく「ポータルのスクショ付き」正しすぎる。

自分の担当は割とすぐすんで、隣までやったり、あとはビール飲みながら修復してました。

前倒しで16時から構築で19時完成。1日経ったが、まだ、結構残ってるな。

　　─　＊ 　　─　＊ 　　─　＊ 　　─　

打ち上げが波の上で、ちょっと遠かったんですが、そのまま松山公園経由でゆいレールで帰りました。終バスより遅いのが便利。

ただ、浦西から歩いて帰るのは厳しいかな．半分くらいで挫折してタクるパターンが多い。それでも全タクよりはだいぶ安いので助かってます。

駐車場経由でバス通りに出てるのは僕だけかもな。

研究室OBが連チャンで

なんで今頃? いや、まぁ、歓迎ですが。

そして、積み重ねられるお土産。

歯医者さんの続き

ブリッジなので二つの歯をがりがりと。前の方はだいぶやられていて神経抜かれてしまった。後ろの方も結構削られて痛かった。

「(麻酔の)効きが悪いですね」。ぐ。ま、そんなもんか。型取ってもらって仮詰め。来週、入ればそれで終わりだが... その後が心配ではある。

90年にイギリスに行く直前に、卒業直後の同級生に、歯をかなり治してもらったんだけど、あれは、まぁ、やりがいがあったんじゃなかったと。
前歯二本に、奥歯の根っこに穴が開いた奴、その他、大勢みたいな感じを一ヶ月くらいでがんがん。あの要領の良さはすごかった。

その前歯は、いまだに使ってます。奥歯は抜いちゃったけどな。

Linux Kernel の source

毎年読んでます。今年はFedora 31。Linux version 4.20.0-rc1+ ですね。でも、最新は5.4.1かぁ。読むだけだったら最新を使いたいところだけど。

kernel build だけでも面倒くさいのですが、最新のFedoraで debug用に kerel build する ansible script がある。

なんですが、どうして、

　　こう毎回、違うんだ?

去年読んだときは「あり、tableから sys_table を生成するようになってる(いまさらか?)」と思ったんですが、今年は、

　　一度、Cの関数 do_syscall を呼び出して、その中で table call してる

去年まではアセンブラレベルだったのに。さらに、

　　直接、sys_read にkernel callのABI修飾子(マクロ)を付けるのではなく、
　　ABI修飾子マクロの付いた関数から、ksys_read を呼び出す方式に変更

されてる。いや、その SYSCALL_DEFINE3 とかの超ダサいマクロやめろと思ったのも2,3年前だった気がするんだが...

既に C に入ってるんだから、SYSCALL_DEFINE3 は、もう何もやってない気がするんだが、そんなことはないのか。

でも、stub 経由で通常のfunctionを呼び出す方式自体は正しいとは思います。

とかやってたら、さっさと、qemu を使った gdb による kernel debug するつもりだったのをすっ飛ばしてしまいました。

いや、授業中に MBP の freeze とか、display adaptor を不調で交換とかやってたので時間を取ったってもあったんけど。

罫線書類

.doc とか .docx は、ちょっとなぁ。なので、HTML で書いてしまうことが多いです。

LaTeX のスタイルの背景に罫線書類のコピーを置くなんていう技もあるらしいが、そこまでする気もないかな。

<table border="1" cellspacing="0" align="top" width="100%" height="600">

とかで始めるわけだが、rowspan/colspan がめんどくさい。なので、それを生成する Perl Script を持っていたりするんだが..

tab で区切って、- とか書くと、そこが前の column とつながるとか、そんなの。

vim が tag を閉めないと文句いうので、そっちが便利かも。

そのまま、MS Word とか Pages とか LibreOffice とかにコピペすると、.doc になるっぽい。いや、あとは知らん。

blog 書こうと思っていたのに

間に合わないな

饒波公民館 Nova

いつもの Ingress。 饒波はのはと読むらしく。要するに、ダジャレ作戦です。

車じゃないから、作戦への貢献度はゼロなんだけど、本数増やすくらいは。

南部のど真ん中からだからなぁ。リンク切りは大変だったと思いますよ。琉大は少しは整形したけど...

那覇の飲み会のあと、帰ってきてから、琉大病院までいって、そこから32本稼ぎました。琉大掃除してくれた人たちありがとうございます。

工学部側からは、微妙に入らなかったけど、入れば40まではいったかな。

久しぶりのNovaで、楽しかったです。この手のは、他の位置ゲーではできないからな。

ついでに、Recurs 後で Lv14 まで来ました。

12/7には crossfaction な首里城アートをやるらしく、絶賛、参加者募集中です。

iPhone Short Cut

これがなぁ。AppleScript らしく。まぁ、仕方ないのだが、

　　application 毎にできることが違う

やりたいのは自動的に々写真を撮るだけなんですが...

どうも設定すると、AppleScript をネットから読めるらしい。でも、AppleScript の言語的なダメさ加減はな..

　　Dictonary 死ね!

的な。JavaScrpipt 使える説あったのに。

Camera を起動して、写真を撮るのは Preview しないを選択するとできた。なのだが、

　　今どんな写真を撮ったかが見れない

ぐ。Quick look だと、抜けるのを待ってしまう。それは

　　自動的とは言わない

ですね。Quick look して何秒後かに抜けるみたいなのが欲しいんですが。

うーん、自分で書くか? なんかある?

安安

安易な焼肉チェーン店です。新しく東口にできたとかで、学生が行くと言うので付き合いました。

この手の焼肉だと、石嶺のキムチ屋を愛用していたのだが、なくなって既に2年。満福が近いのだが、最近は行ってないな〜　でも、

　　焼肉いくのに理由はいらないし。

新しくできたからと言って、特にキャンペーンがあるわけでもなく。

でも、七輪で焼くのは良いな。肉はまぁ、そんなもの。

最近はメニューが中華タブレット。TECって書いてある。ってことは、

　　コンセントがある

これが便利だな。

Agda の不等号の推論

最近いじってた Data.Fin とか < とか ≤ とか良くでてきてて、substとか<-transで適当に片付けていたんですが、

某所から降ってきたのが、結構、使いまくり。

　Agdaの特徴である推論使えないの?

だよなあ。で、

lemma1 : suc (suc m + n * suc m) ≤ suc (k * suc m) → suc (suc m + suc n * suc m ) ≤ suc (suc k * suc m)
lemma1 (s≤s lt) = s≤s ( s≤s (subst (λ x → x ) (
　 begin
　　 suc m + n * suc m ≤ k * suc m
　 ≡⟨⟩
　　 suc n * suc m　　 ≤ k * suc m
　 ≡⟨ ? ⟩
　　 m + suc n * suc m ≤ m + k * suc m
　 ∎ ) lt ))　where open ≡-Reasoning

とかやってみる。でも、これはだめ。suc n < suc m と n < m は等しくないから。

Bool で Setoid すればできるんじゃないかと思って agda-stdlib 見てたら、

　　agda-stdlib/src/Data/Nat/Properties.agda
　　-- A module for reasoning about the _≤_ and _<_ relations
　　module ≤-Reasoning where
　　　open import Relation.Binary.Reasoning.Base.Triple

なんだ、そこかぁ。

　　 lemma : {n k m : ℕ } → n < k　→ suc (k * suc m) > suc m + n * suc m
　　 lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
　　 lemma {suc n} {suc k} {m} lt = begin
　　　　　　　　 suc (suc m + suc n * suc m)
　　　　　　　≡⟨⟩
　　　　　　　　 suc ( suc (suc n) * suc m)
　　　　　　　≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
　　　　　　　　 suc (suc k * suc m)
　　　　　　　∎　 where open ≤-Reasoning

みたいに使うらしい。使い方は stdlib を grep して見つけました。

傘

超雨男なので、傘は必須。いつも、持ち歩いてます。「こんな天気に傘ですか?」とかいってる人が、僕と一緒だと1時間後に顔色変わるとか。

さこ飯のさこさんもそうらしい。農連市場の土砂降りはすごかった。

この間、大学にお客さんが来てる時に傘なくしてしまって探しまくっていたんですが...

いつものお昼の佐真下のコートドールで見つけました。この傘割と調子良いのでうれしい。

バス停でなくした時には見つからなかったので残念だった。

年末の予定

12/27-1/13 東京で、1/9-12 はプロシンなはずです。年末、東京にいくのは久しぶりかも。

もっとも実家に行っても特にやることはないのだが。それは、家事やらない人のセリフか。

この時期だと飲み屋さんもやってないので、実家に閉じこもってたり。

Finite Set

今週末は、Agda でそんなのやってました。首里で Ingress で遊ぼうと思っていたのに。結婚式の帰りは公栄あたりを廻ってました。

NFAの受理を調べるのに、有限集合から検索ってのをやるので、書いたんですが、Agda だと

　　Data.Fin

だけでやるものかも。これにdata とか、いろんな集合(Agdaでは関数の型だ)を対応させるわけ。

Automaton だけでも、Finite Set の和集合、'積集合、Q → Bool と一通りでてきてしまう。個数はそれぞれ、足し算、掛け算、exp 2 になります。

その結果が、Data.Fin つまり個数制限のある自然数に写像されるわけだ。小学生でもわかる内容なんですが...

これが思ったより、はまる。Data.Fin との写像には「ちゃんと範囲に収まっている」というのを示す論理式があって、それを持ち歩くことに。

それに対する ISO つまり、

　　record ISO (A B : Set) : Set where
　　　 field
　　　　　 A←B : B → A
　　　　　 B←A : A → B
　　　　　 iso← : (q : A) → A←B ( B←A q ) ≡ q
　　　　　 iso→ : (f : B) → B←A ( A←B f ) ≡ f

を確認することに。超絶面倒くさいです。

和集合とか仮定してすませてたんですが、まぁ、そういうわけにもいかないかと思って始めたんですが、結構難しい。

和集合は足し算なので、Data.Finの加減算と格闘する羽目に。ほとんどできたんですが、そこで、

　　要素を一つ付け加える操作を∨で定義して
　　それをn回繰り返して、A ∨ Fin n を作り
　　Fin n に B を対応させる

というのを思いついた。ISOがあれば同じ Finite Set だからな。これで、加減算とはほぼおさらばできた。素晴らしい。

和集合ができれば、積も同じように、∨をn回繰り返せば良い。

次は、Q → Bool ですが、List Bool でも良い。これも空列から始めて、一つ増えると、∨で倍に。倍々なので exp 2 。わかりやすい。

なんですが、Q → Bool と List Bool のISOが難しかった。プログラマって、

　　要求される入力よりも広い範囲の入力を受け付ける関数

を書くよね。でも、これが ISO の範囲をはずれて調べる羽目に。当然、そこではISOは成立しない。

結局、範囲を正確に受けとる関数に変換する羽目に。しかも、行きと帰りと両方。

これで、Q → Bool までできた。

そこで終わりにすれば良かったんですが、部分集合欲しいなと思って。m 個の Finite Set から n < m 個のFinite Set を作るわけですが...

個々の要素を Q と Q に付いている番号が n よりも小さい条件を一緒に持ち歩けばよい。結果的には、

　　data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
　　　elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa

というdataを持ち歩けば良いわけですが、A←B で生成した条件を、iso← 側で検算することになる。そこその大きさの項を検算する羽目に。

そこで、積やListと同じでzeroから増やす方法もやってみたのですが、複雑はほぼ変わらない。まぁ、どの方法でもできそうなところまではいったのだが。

結局、この data に対する合同条件

　　get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less n<m fa → A
　　get-elm (elm1 a _ ) = a

　　get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
　　get-< (elm1 _ b ) = b

　　fin-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
　　　 → (x y : fin-less n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅　get-< y → x ≡ y
　　fin-less-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl

を書いて頑張って検算する方法でできた。

ここでわかったのは、この fin-less の data は、集合のLimitiを作るものと同じ。Data.Fin の構造を保つ部分集合を作るということは、結局は、'

　　圏のLimit、つまり、随伴関手

を作ることと同じことらしい。どうりで難しいわけだよ。

結果的には割と短い証明でできたので良しと言うことにしよう。


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

結婚式

吉浜さん、おめでとうございます。

この年になると結婚式に呼ばれるのは普通はないんだけど。まぁ、あの沖縄流の三百人呼ぶやつですね。

入場、かじゃで風から花束贈呈と言う、伝統芸なのは、もはや珍しいかも。

超上品な加奈よ〜が観れたのが良かったです。

料理は中華系ですが、なんか、でかいフォアグラが... 新郎の趣味だな、きっと。

グランドキャッスルは日航からヒルトンで、ダブルツリーブランドになったわけですが、レストランのレベルは維持できてる感じかな。

今時は、外資系の方が人を大切にしてるかも。

成美おばさん

東京に行くたんびに顔出すようにしていたんですが、昨日、息を引き取ったようです。四人姉妹の三女。

子供の頃からかわいがってもらったからなぁ。キャラクター物が好きな人でした。

次女の母のクモ膜下出血の時にも、いろいろ助けてもらいました。母と一緒にいてくれるだけで助かった。

施設にいたのも長かったような短かったような。

8月に会ったのが最後だったけど、穏やかな晩年だったかな。いや、そんなことはないのだろうけど、そういうことしよう。

今年の年末はそんなわけなので、東京にいるようにします。

引き潮のとき

先日亡くなった眉村卓のおそらく最大の著作です。随分前に司政官シリーズをまとめたものと消滅の光輪を読んだので読みたいとは思ってました。

が、ハードカバー五冊。もっとも当時2,500円x5だったので買っておくべきだった... 今は古書で一冊一万円近い。でも、文庫でるんじゃないか説。

宜野湾図書館にあるのをWebから検索してもらっていたので、Ingress で寄ったので借りてきました。

　　倉庫にあるけど、5分で持ってこられる

お役所っぽくない。素晴らしい。5冊は重いので取りあえず2冊。図書カードも作ってもらいました。コピーは一部までとか書いてある。そういえばそんなことになっていたっけか。

400 x 5 ページかぁ。ひたすらモノローグが続くのは、80年代当時、SFマガジンの立ち読みで知ってはいるんですが...

司政官はロボット官僚を使って植民星を管理するみたいな話なんですけど、どちらかと言えば、

　　司政官の黄金期の話を読みたかった

気もする。もっとも。人類史上、成功した官僚制度とか一つもないわけなんだ3けど。でも、SFなら、そういうものが読みたい気がする。武器店みたいな。

歯医者さん

今年は結構いってる。今回は右下のブリッジのところ。「前の方ははずれてますね」で、中がやられてしまった。

割と調子が良かっただけに残念すぎる。前の方の神経抜いてブリッジ作り直しですか。もっとも9年使ったのでそんなものか。

でも、前歯の方は20年以上使ってるんだよな。

麻酔が抜けないまま昼飯食ったら、口の中をかみまくりました。

いろいろ壊れる

昨日の夜にシス管が「321のMac Miniが死んでます」で、見に行ったんですが、超熱くなっててだめぽい。TreeVNCが暴走するってのがあってなぁ。

しばらく電源切って冷やしてと思ったんですが、やっぱりだめ。Rescue mode からのOS再インストールからでもこける。あとは PRAM reset くらいか。

もっとも、これは現システムの一部なので修理してもらえるかもしれないな。こいつ経由で画面共有に使ってるだけなんですけどね。

Apple TVでも接続はできるのだが、学生への配信がな。

まぁ、自分のMBPから配信することもできる。ただ、プロジェクタに接続する必要はある。あるのだが、

　　HDMI display adator が反応しない

あれ。教卓に汎用のを置いてくれてたので、そっちを使うと写る。戻すとだめ。そういえば最近使ってなかったからなぁ。

あと、自分は使ってないんですが、ケーブルを使わない充電器が

　　充電できないわけじゃないけど遅い

と言う技があるらしい。置いといたら使えないから意味ないじゃんとか思うけど、学生は便利だとか言ってます。

でも、最近はイベントとかでDeNAとかが配ってくれてるので、それを回収しました。

Adaptor どうしようかなって話題は、Facebook でもみたな。

てだこ浦西の乗り換え(続き)

今度は高速バスの下りに乗り換えてみました。雨男なので、スーツが絞れるくらいの土砂降りくらったが...

いや、この坂は無理だわ。これは滑落したら死ぬだろ。ちなみに最短距離は私道のようです。

県庁前から直接高速バス使うのに勝てるとは思えないな。97には余裕で勝てます。

まぁ、選択肢があるのは良いか。古島からやんばる急行とか。

だんだん出てくる

まぁ、猫だからなぁ。オス猫二匹は、あんまり、そういことしなかったんだが...

Automaton の結合

Automaton で受理される言語(文字列の集合)の個々のものをつなげたものを受理するAutomatonがあるって話。

途中でどこでわければ良いかわからないから非決定性Automatonを導入するってやつです。で、非決定性Automatonは決定性に変換できるから証明終了と。

なんだけど、ちょっと待て。確かに非決定性Automatonは作ったけど、それが正規言語AとBの結合に等しい言語を定義しているかどうかは調べてないよね。

いや、確かに、図を見ると自明なんですが。でも、そもそも非決定性Automatonの受理のルールが複雑だからなぁ。

で、実際に Agda で証明に行くわけですが、予想通り、かなりはまった。

　　split : {Σ : Set} → (List Σ → Bool)
　　　　　→ ( List Σ → Bool) → List Σ → Bool
　　split x y　[] = x [] /\ y []
　　split x y (h　∷ t) = (x [] /\ y (h　∷ t)) \/
　　　split (λ t1 → x (　h ∷ t1 ))　(λ t2 → y t2 ) t

　　Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
　　Concat {Σ} A B = split A B

こんな感じで言語の結合は定義できるわけですが、 contain A x で Automaton A が x 受理するとして、

　　closed-in-concat :　{Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )

こんな感じで Concat が、でっちあげたNFA である M-Concat A B と等しいことを見に行きます。すると、

　　　(1) closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true

と

　　　(2) closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true

とを示すことになる。まぁ、そうだよな。

finiteSet 有限集合の∃関連の述語は一通り書いたし、split の逆とか使って、(1)はスムースだった。仮定から二つの入力が
あるのがわかるので、それが実際に受理されることを NFA をたどって示せばよい。

なんですが、(2)が良くわからない。

　　　ずーっと A で動いていて、Aが終わりで残りが B なら Ok

つまり、A until B 見たいな時相論理式を証明にいくわけだな。

　　aend (automaton A) qa) /\　accept (automaton B) (δ (automaton B) (astart B) h) t

を調べて真なら、それで成立。成り立たなかったら次の状態に進む。

なんだけど、M-Concat A B が非決定的なので、

　　　途中、B になりそうになるが、いつか B でなくなる

ってのがある。つまり、 accept (automaton B) s x ってのが、その時点では判明しない。この辺、専門なはずなんだけどな。

　　ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
　　ab-case (case1 qa') qa x = qa'　≡ qa
　　ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x　≡ true )

　　contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
　　　　　→ (qa : states A )　→ (　(q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )

とかいうのを思いついて、ようやっと突破できた。

いや、でも、ちょっと複雑すぎるだろ。NFAに閉じれば簡単になるかも。co-induction とか使えれば面白いんだが。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/regular-language.agda

てだこ浦西駅のバス乗り換え

幸地(那覇向け)側から乗り換えてみました。まぁ、夜は暗いんだが、最近はスマホを懐中電灯代わりにしてるので平気。

思ったより近い。3分くらい。坂の上り下りはあるけど。車椅子でもいけるかというと、階段があるのでだめです。

125/56/97から便利な道の方は、やっぱり私道でチェーンが張られてました。が、まぁ、歩きなら通っても怒られないかも。

途中には異世界へ続く道が。上の会社かなんかをどかして道にするらしい。

もう琉大までは来ないかも知れないけど、来るとすると、坂田でまた90度曲がるのだな。

終電が遅いのは便利なんですが、だいたい半分くらい歩いたところでめげてタクるパターンですね。全部歩けばバスより安いけど。

ストレスチェック

紙で URL とパスワード送ってくるってどうなの? まぁ、うちの学科でも学生の初期パスワードは紙で配っていたりするわけですが。

いや、教職員は全員メール持ってるわけじゃん。メールで送れよ。

　　読まないから

まぁ、そうだよなあ。メールで送ってくるストレスチェックなんてSPAMかウイルスに決まってるからなぁ。

で、まぁ、入力したのですが

　　ボタンがおせない

え、ちゃんと11/15金からって書いてあるじゃん。え、

　　今日は金曜日じゃない

あ、そうですか。あ〜　ストレス貯まった〜 こんなんでも、どうせ役人の引退先だろと思うと余計。

Libretto 50

Mobile Gear とかの話が出てたので、思い出しました。東芝のノートPCの名機。たぶん3年くらい使ったかも。

CPU は Pentimum 75MHz / Memory 32MB / 640 x 480/ 24 bit true color なはずです。もちろん、英語キーボード。

日本語キーボードだと少しきーが小さくなって右寄りになって打ちづらい。

電池は持たなかったので二本持ち歩いていた記憶がある。

当時、このTFT画面は綺麗に感じたな。ピッチが細かいので写真が綺麗。これで取り込んだ写真が結構ある。この時は DVR PC7 かIXY 200 か?

このPCMCIAにPHSを刺して使うわけだな。だいたい remote login でメールとかは処理していたはずです。

これで予算申請通していたりとかしてた。kernel build とか OSの課題作りとか。

Libretto 20/30も使っていた(当時はお金持ち)けど、HDDの換装のせいか結構不安定になった記憶。50はそういうことはなくて、

　　4GB HDD

まで増やしたはずです。これくらいあると平凡社の世界大百科とかが入る。いろいろ便利だったな。

OS X PB が Dula USB iBook と一緒に出て、そちらに乗り換えるまで使いました。あれは重かったのだが、その後、もっと重いのを使う羽目に。

今の、MBP 15inch は、それに比べると軽いな。

HTMLの中の写真

研究室紹介で、いつものHTMLを使ったら写真が巨大に... 去年も一昨年も同じことやったんだろうか?

ググると「pixcelで指定しろ」とか。それはないな。まぁ、ポスターみたいなWebなら、そうかも知れないけど。

width="80%ぐかいが普通か。変換系使ってるので、なかったら付け加えるくらいしても良いかも。

貧乏くさい話シリーズ ピコピコサンダル

ビブラムソール使ってるんですが、靴の底が減ってくると、ゴムに穴が開く。別に貫通しているわけではないので問題はないんですが、

そこに小石が入って、歩くたんびに「からから」言う。まぁ、穴を大きくして、石をだしてやればいいんで8すけどね。

なんと、沖縄の靴屋さんだと靴底を張り替えてもらなくて、東京のいつもの靴屋さんに送ることに。これが割と高く付く。

まぁ、靴なのでたかは知れてるし、毎日使うものなんだから、ちょっとは良いもの、手入れの行き届いたものと思うんですけどね。

え、続くの?

http://www.ne.jp/asahi/jibiki/seika/

Data.Fin と∀と∃

NFA 非決定性オートマトンの条件は、非決定的というだけあって集合から適当に取り出すということをします。

無限集合だと選択公理とかあるんだけど、有限集合なら全部調べればよい。というのをAgdaで書くのだが、これがはまる。

Fin n で n 個の自然数が取れるので、n から始めて 1 で終わるわけなんだけど、実際の要素は i-1 を使う。ややこしい。

条件に合うものを見つけて終わりなんだけど、なぜか、

　　0 に行った時にどうするか

が問題になる。それは起きないはずなんですが「それを証明する必要がある」。あぁ、まぁ、確かに。そうだよね。

あるとわかっていて探しているので「なかったら矛盾」で良いわけですけどね。なので、

　　「i>mの時はない」ってのをnから始めれば、m=0になった時に「あるって言ってたのにないじゃん」

と言えるというのに、昨日、Bar で飲みながら Agda を書いてた時に思いつきました。これで解決。

なのだが、これはテンプレだからライブラリにあるはずだよなと、Agda の Data.Fin を見ると、

　　¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
　　　　　　　¬ (∀ i → P i) → (∃ λ i → ¬ P i)
　　¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)

とか三行で書いてある。いや、そこまで来るのに、いろいろあるので、これを使うかどうかは微妙なんだけど。

Agda まだ、知らないことたくさんあるらしい。

もう一つはまったのは、Data.Fin とData.Natの変換。

　　toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
　　toℕ-fromℕ≤ (s≤s z≤n)　　　 = refl
　　toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))


これだな。自力で証明できるところまで来てライブラリにあることに気がつく、いつものパターン。

遭難中のルンバ君とコタ

どっちも同じくらいの年齢なんじゃないか説。敷物巻き込んだようだ。

新入りと比べるとコタのアホさとヨボヨボさが目立つこの頃です。

ルンバは猫毛掃除機としては優秀。

Subset Construction

なんか去年苦労してた気がするんだが... NFAからDFAを作るってやつですね。作ったものが元と一致する証明さぼってたんですが...

授業が終わった後、書いてみたら一発だった。どういうこと。やっぱり、Agda力が上がってるってことか。

　　　　(NAutomaton Q　Σ ) → (astart : Q ) → (Automaton (Q → Bool)　Σ )

状態Qの非決定性オートマトンを、状態(Q→Bool)な決定性オートマトンに読み替えるだけだから、入力をたどれば一致することは自明。

FiniteSet は Q が Fin n (0..n)に isomorphic (1対1)だってのですが、ちょっとださいかな。

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

読書会

高校時代も高2高3辺りで読書会とか良くやってました。友人の趣味でエーリッヒフロム。僕はラッセルの方が好みだったが。

大学に入って、 すぐ友人が読書会やろうというのでやろうと言ったのですが、それが

　　ベルグソンの自然の弁証法

なんで、そんなものだったかと言うと、まぁ、当時の生協がそういうところだったからなんですが、これがクソな本でな。

読書会では、もっぱら本の内容で大爆笑シリーズだったはずです。だれだよ、こんなのお題に選んだの。

で、その後もいろんな本を集まって読んでました。吉田夏彦先生の哲学の授業と研究室の周辺の人たちですね。日本語英語手当たり次第にいろいろ読んだ。

　　浅田彰
　　事的世界観への前哨
　　ノーベル賞受賞論文集
　　WVO Quine 経験主義のふたつのドグマ
　　力学の入門書
　　観測問題論文集
　　量子力学
　　Diracの一般相対論
　　Diracの量子力学
　　資本論 (1-4)
　　経哲草稿
　　連続群論
　　回転群の表現
　　層圏トポス

まぁ、楽しかったな。全部理解できたわけではないですが、計算を追うくらいは。この辺にいろいろ影響されていたことは確か。

院生時代は、分厚い英語の教科書を朝集まって問題解いていくとかやってたみたいです。データベースとかオートマトンとか。

もっとも、これらに一貫したものはないわけですが。たまにうちの学生も勉強会とかやってるようですね。

浦西駅

125番のバスで行ってみました。前田入り口つまり紫雲閣からだと駐車場経由で行けるんですが、ちょっと遠い。エレベータ付き。

西原入口だと、なんと駅前に降りる道ができてました。これは車も通れそうだが...

125/56/97 が駅経由で乗り換えできるようになると便利なんですけどね。こいつらの相互乗り換えもかなり不便なので。

この道、バスは通れないこともない気がするが... 私道っぽい。そもそも西原入口を通れなくする必要あったの?

まぁ、いろいろ未完成ではあるけどさ。バス会社側のやる気のなさっていうか悪意っていうか...

琉大まで来るとしても10年後でしょう。

ズボン破れた

これ、Ingress で一番やせてたころにつくった奴じゃないかな。でも生地もけっこうぼろぼろ。Ingeess も結構長くやってるからな〜

新しいScannerが、どんどん遅くなってて残念。サーバーとの同期がよろしくないらしく、詰まったりずれたり。どうせ、サーバレスとかだろうけど...

はっかーずちゃんぷるー

いや、一応、きたんですが、

　　昨日飲みすぎて、二日酔い

なので、さぼって、Agda をいじってます。すみません。

なんかヨガやってたり、トラブル対応の演習やってたり、わりとカオス。

民間英語試験

なんか延期になってしまってがっかり。うちは院試には最初からTOEFLを使っているんですが、割と便利。先生が問題考えなくていいから。

採点基準も安定しているので「今年は英語のできが悪い」的な評価も可能。ただ、PBTで400の下の方が多くて、

　　それでは使い物にならない

って方が問題。高校の教科書の語彙は2千くらいらしいんですが、大学生レベルだと6千は欲しい感じ。PBT 550からが実用的なんですが、語彙的にはそんなものかも。

僕も高校時代はあまり英語は勉強しなかったんですが、理由の一つは勉強しなくても通るから。あの受験校でもそんな感じ。

まぁ、おかげで浪人時代にだいぶ勉強する羽目になって、受験のレベル的にはそこそこまでいった。でも、

　　それでは使い物にならない

哲学の本とか論文とかSFとか知らない単語ばかり。先生には「なんだ、こんなもの読めないの?」とか言われちゃうし。 実は

　　語彙2千から6千まで上げる

のがつらい。2千まではそんなに大変じゃない。学生を見てると千ぐらいな感じ。コードに書く変数の綴りが怪しいレベル。

　　コメントに日本語書くな! ベトナム語でコメント書いてあったら困るだろ

っていうんですけどね。卒業までに英文5千ページ読めと言ってます。

言いたいことは、

　　大学受験の英語レベルが低すぎて早めにサチってしまうことの対策には民間英語試験が良い

だろうってことです。

まぁ、必須にするには準備不足だったようだが、お役所の「受験スケジュールに合わせろ」的な指導がダメだった説も。もう少し落としどころなかったのか?

Agda の List と Vec

朝起きてニュースをWebで見たら、首里城のあれだったので、よどよしてました。

それとは関係なく、 授業で、Agda で Automaton ってのをやってるんですが、だいたい r_0 とか r_i とか書いてある。これが Agda と相性が良くない。

List で入力データを表して、Automaton に食わせるとかの方が楽。でも、自然数添字の方も書いてみたんですが、あんまりうまくいかなくて。

でも、授業終わった後で、「そうだ、普通に ℕ → Q と書けば良い?」と思いついて。でも、長さで切らないとだめ。

　　r : (i : ℕ ) → i < suc n → Q

こんな感じか。「そうだよ、Cとかでもポインタでアクセスする時にはちゃんと正しい範囲のアクセスだと明示しろ!」とか思いました。

で、まぁ、それで書けたんですが、そういえば、

　　固定長の Vector ってあったよな?

と思って、Data.Vec を読んでみると、これが、長さ付きのList。そうなのか。そして、

　　Data.Vec と Data.List は両立しない

Agda は Polymorphism ないので、異なる型に同じ関数名を使えない。ま、いいか、全部、Vec で書けば。で、書き直せたんですが、

　　ほとんど、差がない

差があるのは、length を明示的に書く替わりに、引数に長さを表す { n : ℕ } が増えるだけ。あぁ、まぁ、そんなもんだよな。

もっと、ありがたいはずだとと思ったのに〜

まぁ、でも教科書の定義とListを使った定義の同等性とか、正規言語のUnionが正規言語とかできたらいいか。

舟を編む

プライムビデオにあった手元に録画のないものシリーズの一つ。2009ぐらいに書かれた、たぶん、2004くらいに日本語の中辞典を作る話。

なんで、それくらいかと思うかと言うと、前半はガラケーで終盤にスマホになるからですね。どうも10年経過みたいな気もするが...

辞書の編集の話だが、

　　コンピュータを使う話がいっさいない

パソコンは置いてあるんですが使う場面なし。全部、原稿用紙ベース。活版は出てこないから、おそらくは写植。完成時にも使ってない。

これは異常だと思う。辞書をDB抜きで作るとかもはやあり得ないわけだけど、23万語をアルバイト総動員で紙で再チェックする話とか出てくる。

46Mbyte くらいのデータ量だと思うのでフロッピィには入らないけど、既にGByteなHDDはあったはず。

アニメでも「今はコンピュータでこうこう」みたいな説明は一切なし。考えられるのは、

　　コンピュータ導入を全力で拒否していた

ってことだろうなぁ。2000年にはTeX入稿もやってたはずですが、そういう部署もあったってことかな。

22万部刷るとかいう話も出てましたが、あの時代に電子版を出さないってのも不思議な感じ。CDROMな電子Bookとかは90年代に既にあったし。

そんなんだから日本は滅んだ的に観てました。まぁ、そういう時代もあったよね的なドキュメンタリー的なものか。

http://www.funewoamu.com

golang test

InteliJ から golang のテストを書くんですが、なんか、構造体の配列を作ってループするみたいな感じのコードが生成されるんですが、

　配列の書き方が良くわからん

結局、

　　type args struct {
　　　 u fileIO.FileIO
　　}
　　u1 := fileIO.FileIO{}
　　var tests = []struct {
　　　name string
　　　　　　　　args args
　　　}{
　　　　 {"test",args{u1}},
　　}

で、通ったのですが、いろいろ納得いかん。最後の「,」はなんだよ。これがないと

　 main_test.go:18:20: missing ',' before newline in composite literal

ううーん。あと、

　　args{u1}},

これ。単に u1 とか{u1}だと通らない。

　 {"test",u1},
　 main_test.go:18:11: cannot use u1 (type fileIO.FileIO) as type args in field value
　 {"test",{u1}},
　 main_test.go:18:11: missing type in composite literal

いや、まぁ、気持ちはわからなくもない。{} だと anonymous type になるってことでしょ。でも、それくらい推論できるだろ? しない理由あるのか?

猫を飼う

Twitter で tableau で解くなんてのを見かけたので、Agda でやってみました。

仮定
　 猫か犬を飼っている人は山羊を飼ってない
　 猫を飼ってない人は、犬かウサギを飼っている
　 猫も山羊も飼っていない人は、ウサギを飼っている

問題
　 山羊を飼っている人は、犬を飼っていない
　 山羊を飼っている人は、ウサギを飼っている
　 ウサギを飼っていない人は、猫を飼っている

record で書くと、

　 record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
　　 field
　　　　fact1 : ( Cat ∨ Dog ) → ¬ Goat
　　　　fact2 : ¬ Cat →　( Dog ∨ Rabbit )
　　　　fact3 : ¬ ( Cat ∨ Goat ) →　Rabbit

こんな感じか。これを仮定したmoduleを作って

　module tmp ( Cat Dog Goat Rabbit : Set ) (p :　PetResearch　Cat Dog Goat Rabbit ) where
　　open PetResearch
　　problem1 : Goat → ¬ Dog
　　problem1 g d = fact1 p (case2 d) g

簡単簡単。だけど、排中律は証明できないから仮定する必要がある。

　postulate
　　 lem : (a : Set) → a ∨ ( ¬ a )

ということは、validな命題論理式でも証明できないものがあるってことね。排中律を仮定すれば全部証明できました。

Bool代数を使う別な方法もやってみました。

　 problem1 :　( Cat Dog Goat Rabbit : Bool ) →
　　((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>　( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>　Rabbit ) )
　　=> ( Goat => ( ¬ Dog )) ≡ true
　problem1 c false false r = refl
　　...

この方法だと、入力をtrue/falseで選択ていく感じ。本来のtableauだと、絞っていく過程で式の簡略化もするはず。
こっちの方が機械的にできる利点がある。

そういえば、Solver あるはずと思ったら、一応ある。

　 open import Data.Bool.Solver using (module xor-∧-Solver)
　 open xor-∧-Solver

　 problem0' :　( Cat : Bool ) → (Cat xor Cat ) ≡ false
　 problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl

とかすると動くっぽいんですが、なぜかエラーが。壊れてるかな。SAT solverと連携させる話は、少し昔に流行ったはずです。

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

JPHACKS 2019

去年に引き続きやってます。こういうのは続けるのが大切だからな。この手の

　　ハッカソン

は割と良くあって、学生たちも自分たちで「ほげほげゲームジャム」みたいな感じで企画しているみたい。

楽しんでやってもらえればと思うけど、一方で、

　　大学生っぽいもの

を作って欲しいかとも思うかな。せいぜい背伸びして欲しいと思うけど、それが今の学生のやらないことの一つかも。

隙間を縫って...

一時期ほどはしゃかりきにはやってないのですが、Ingress で、

　　こういう隙間を縫って、省エネでfield稼ぎ

が面白いかな。ANAの運動公園の裏かまわって、伊租公園まで。一時間もかかってないかも。

わた琉

宜野湾にできた新しいラーメン屋さん。あっさり塩ラーメン。醤油は試してません。割とまとも。良いんですが...

前の横浜家系のところなんだよな。あそこよりは、まともラーメンで店舗もおしゃれになった。なんですが...

　　あっさり系のラーメンって難しくない?

前のきんのすけも敗れ去ってたしな。タカネは、まぁ、頑張ってるんですが、担々麺とかあるんだよな。頑張って欲しいけど。

日本の飲食店って半端なく安いから難しいんだよな。店出す方は一応考えてはいるんでしょうけど。前にあったVCの人とか

　　「そんなにひどい赤字にはならないですよ」

とか言ってたし。ハリーズの支店が琉大北口に欲しい的な話をした時だと思うけど。

逆に言えば、社会的に飲食店をサポートすれば成立するってことでもある。子供食堂とかいう話もあるけど、

　　街にある飲食店が街を構成する

ところがあるよね。みんなが家で家族だけで食事しているのって、独り者が一人で食事しているのと似てるし。

日本は外食が安いのが売りな国になってるわけだけど、どうせなら、それで推していけばどう?

最近人気のないシス管の飲み会

たまには、打ち上げやろうみたいな感じで。なんですが、

　　沖縄は風邪が流行っていて

教員と学生のかなりの部分がダウン。結局、参加者は5人に。まぁ、学生的にはそこそこの豪遊か?

温野菜のしゃぶしゃぶ食べ放題でしたが「食べたことありません」的なのが出るのが学生なんだよな。

久しぶりのCetOS updateとか、来年のシステムの構成(おそらくはContainer base)のこととか、やることは多いんですが、戦力がなぁ。

でも、1年次がいるからいいか。

一応面接での受けはよいようなんですよ。

ただ、ちまたではクラウド中心になっているようなので、それとの対応が問題だな。クラウドは誰かが張り付いてケチくさく使うもの。

それでもクラウド使うのでも実装を知っていた方が良いんじゃないかとは思うんですけどね。

sudo のbug

例の -1 入れると root になれるって奴ですが。sudo のversionあげようよって言ったら、

　　CentOS の yum な sudo は古いまま

くそ〜 CentOS8 に上げるのは、そんなに簡単にはいかないだろうな。

で、sudoers 見ろとか書いてある。

　　＊ もともと root になれる奴なら、特に問題ない
　　＊ root なれない奴がいると問題
　　＊ なので、!root と書いてあるのだけなんとかしろ

あぁ、まぁ、そうだよな。ということは、

　　何もしなくて良い

らしいです。ちゃんちゃん。大問題っぽく、おおさわぎするんじゃね〜よ。

僕だけがいない街

いろいろやらないといけないことはあるんだけど、まぁ、それなのでアニメを観てしまったりするするわけなんですが...

Primive Video で、なんか手元に録画のないものというので探して引っかかったものです。このアニメは720pを意識しているのか
高圧縮でも画質的な破綻は少なかったかも。東北設定なので色調が白黒だからか。

Reset もの。小学生に戻って今の事件を解決する的な。まぁ、一気に観たので、そこそこ面白かったことかな。

29歳漫画家志望な主人公が微妙。 まぁ、微妙なところから成長する物語なはずなんですけどね。 ちょっと切り貼り的。

登場人物が少なすぎて犯人が早くからバレバレなのがなぁ。最初からばらしてしまった方がコロンボ的に面白くなったかも。

主人公に思い入れて達成感を共有できるのは良いかな。とすると、終盤は蛇足かなぁ。

マイナスゼロは出てきてましたが夏への扉は見つけられなかったな。良く見るとあったかも。輪廻の蛇的なパラドックスは?

https://bokumachi-anime.com

Prime video の画質

PS4側でPSYCHO PASS 2を見た時にも違和感あったんだけど、iPhone 側で down loadすると、

　　25分で80MByte

う。それは圧縮しすぎでしょ。と思ったらHDは別価格ですか。なるほど。

もっとも、学生は d-amine store とかも使ってて、あんまり画質は気にしてないみたいだな。SDでも平気らしい。

でも、気に入ったものは円盤買ってお布施とかいってますね。

スカパー側の録画はLSRだったりするので、25分で900MByteくらいか。これがBSのDRだったりすると2.5GBくらいいくからなぁ。

スカパーも送ってくるレートはそんなに高くないのでDRでも大したことはないんですけどね。

時代は低画質ってなところですか...

やらかした...

ちょっと油断してたら、学生に廻していた仕事をぜんぜんやってなかったらしく。いや、

　　そういう時になんとかするのが先生の仕事

なので、できないならできないって言ってくれれば良いんですが。なんだが、ping かけたら、

　　翌日から学校に出てこない

というわざが... そっちの方が「何もしてない」よりも面倒なんですけど。困りましたよ...

割と簡単な奴だったので油断してました。

そんなわけなので、うちのポチを見かけたら叱らないから学校に来いと言ってください。

まぁ、僕も自作マイコンにはまって大学にいかなくて呼び出されたってのはあったんだけどな。

何このバス停

てだこ浦西駅のバス関連のひどさは「ず」がさんざん書いてくれるとは思いますけどね。

陸橋側には、なんかバス停用のふくらみがあったのは完成図から見れたのですけど、連絡橋ぐらいできるのかと。

それが、これですか。これ橋の末端、つまり坂田のTSUTAYAか上のバス通りかどっちかでしか橋から出れない。

　　何考えてるの?! 馬鹿か?

バスの運転手は「儀保で乗り換えろ」みたいなこと言ってたけど

　　駅に繋がらないバスになんか存在価値ない

です。いや、もちろん、駅前にいく道はあるわけさ。

まぁ、これからいろいろできるはずではあるが... 高速バスへの乗り換えとか。

でも、高速バスが一度インターを出るようなことをすると遅いし、乗り心地良くないんだよな。

Graph の表現

Agda でやるオートマトンの授業の一環ですが...

　　record Graph　{ v v' : Level } : Set (Suc v ⊔ Suc v' ) where
　　　field
　　　　vertex : Set v
　　　　edge : vertex　→ vertex → Set v'

この edge を data で書くってのが一つ

　　data edge012b :　ℕ → ℕ →　Set where
　　　　e012b-1 : edge012b 1 2
　　　　e012b-2 : edge012b 1 3

これでいいんですけどね。dgree といわれてちょっと困った。一つのノード(vertex)に接続された辺(edge)の数。

数え上げられない。なので、List を使うかと思ったんですが、

　　list012a : List ( ℕ × ℕ )
　　list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ []

こんな感じ。 ところが上に合わせようと思うと、なんか残念なことに。結局、

　　conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool

を書いて、

　　graph012a : Graph {Zero} {Zero}
　　graph012a = record { vertex = ℕ　; edge = λ s t → (conn list012a s t) ≡ true }

とすると良いらしい。

なんですが、すべてのvertexのdgreeの和とかいうと、それなりに複雑になってしまうっぽい。

まあ、さぼって、すべてのvertexのdgreeの和は偶数ってのは証明はできました。

どこかでお会いしましたっけ

まあ、なんぱの常套手段的なものなんですが... スイスかなんかでやらかしたことがあって。(数十年前) で、気がついた。

　　この人、レイア姫に似てるからだ

いや、もちろん、それは口には出さなかったんですけど。

この前のオクトーバフェスでも、隣のお嬢さんがなんか見覚えある... 今回はすぐに思い出せました。

　　TNGのバイナー星人の回に出てきた女性に似てる

でした。あれはTNGでは実は常連さんなはず。

人の名前なんて全然覚えないのにね〜

普天間宮

だいぶ片付いて、一応、通りから見通せるように。

今後はどうするんだろう? 交番はどくんでしょうけど。

PSYCO-PASS 2

大学にいくつもりだったんだが、宜野湾マリーナのオクトーバフェスタでビール飲んでました。

PSYCO-PASS 2の録画がないのは機材故障とかで録画をすっとばしていたので、その影響でしょう。

なので、Amazon Primeのお試しで。Netflixと同じで任意の機器で視聴できるのは良い感じ。ダウンロードもできるがライセンスがないと見れない方式ですか
。

1の最後で割と陳腐なビックブラザーものになったので、2も終わりはそんな感じ。

自己言及命題に突っ込むなら、もっと頑張って欲しかったかな。いや、クラシカルなSFなら、そこは爆発するところだとは思うけど。

でも見るべき所は、そこではなくて、一気にベテラソになった朱女史と、無能な新人女史の戦いだったかな。

Prime video は結構有料なものが多いのか。まぁ、そうだよな。

Ingress Event

いつものイベントを琉大で。いや、オクトーバーフェスで飲みながら良かったんじゃないの説。途中で抜けて、そっちにいっても
良かったかな。

東京の方は台風が大変そうですが、風は大したことなさそうだが、雨がな。

子供の頃、近所の谷端川があふれたのは覚えてないんですが、

　　それで父は家を建て直す時に1mも土盛りした

ようです。その後は深く浚渫して暗渠に。暗渠になってからはあふれたことはないな。

でも、荒川が東京の弱点なのは相変わらずみたいだなぁ。耐えると良いが...

ロウソクの科学

一応、学校の図書館にはあったと思うし、読んだとは思うけど、記憶にございません。増刷とかじゃなくて、

　　電子書籍でいいじゃん

と思う。

どっちかというとガモフとかブルーバックスとか読んでた方ですが、それより高校とか大学の教科書読んだ方が良かっただろうな。

相対性理論や量子論知りたければ線形代数勉強しろってことね。

MatterMost

Slack alternative ですが... なかなか使ってもらえない。既に、

　　Slack の書込があふれて読めなかった重要案内

とかもあるらしく。Slack の有料オプションも考えたのですが、

　　卒業生のアカウントとかを考えると論外な値段

まぁ、そうだよね。なのだが、

　　連携させてるgitlabのhostname変えたので、MatterMostにloginできなくなってました

おいおい、そういうところだろ〜 Slack から移ってもらえないのは。今はなおった?

Slack 自体は「外部のアルバイトで使っていたり」とかで駆逐はできないんですが、せめて学科内くらいは移行したい。

PSYCHO-PASS

2012で、かなり古いのですが、後期はシーズン3があるらしいし、割と好きな人もいるっぽいので見てみました。

なのだが、シーズン2を録り逃したっぽい。ついさっきまでBS11でやってたじゃん説もあるんだが、再編集版が22話から11話とかで逃しました。

中学生の頃に江戸川乱歩とかを全巻読むとかやったことがあって、そのせいもあるのか猟奇ものはあんまり好きじゃないんだよな。

とはいえ、シビュラシステムとかドミネーターは面白いし、猟奇ものっぽい辺りが一番面白かったかも。

ホームズとかの推理ものをレスペクトしてるところもあるのだけど、終盤は

　　憶測を言うと、それが当たり

的な感じでなぁ。結末も含めて陳腐化した感じだな。そういう脳/コンピュータの世界での死の意味とか自由って何かとか、その辺が3で展開される...

はずもないので、2をどう視聴するとかとか3どうするかとかは考え中です。Amazon Prime のお試しでいいか?

民間英語試験

学科でも採用するところとしないところとあるようですけど。

　　民間試験の方が大学入試より信頼されている

ってのが世間的な事実。英検準一級なら入試の英語免除は妥当かな。

国立大のトップクラスなら理系でも英語のセンター試験は満点狙いなんじゃないかなぁ。そして、

　　それでも学部で使い物にならない

なので差が付かない。英検も一級だけ別もの的なところがある。

日本人、あるいは学卒の英語能力の低さは作られているのかも。一部の民間試験導入に対する激烈な反対は、そういうことなのかもなぁ。

先週のOSの授業ではサイドチャンネル攻撃のWikipediaの日本語と英語を比較して見せました。日本語は2012の引用が最新。英語は2018のSpectraとか。

でも、日本語ばかり見てると、その情報がどんなに時代遅れなのかわからない。Googleの馬鹿用検索システムがそれに輪をかけてる。

ネット(特にYoutube)が早い頃から英語で情報を集めている人と日本語だけの人の格差を広げているなんていう話も。

大学で学生に英語勉強しろと言っても、からまわりしている感じだな。

怪しい黒い影

なんか、カーテンの辺りに。おかげで、カーテンがぼろぼろだ。大きくなるとやらなくなるのだが...

寝てる時に、猫じゃらし持ってきて「遊べ」ってやるので、隣の部屋に閉じ込めました。

持って来いができる猫は実は初めてかも。そんなに頭良さそうでもないんだがな。カリは無駄に頭は良かったが。

ゆいレール延伸

恩納村から呼び出されて那覇まで出たので、帰りに使ってみました。なにせ、

　　バスの本数が減って23時以降のバスがない

ひどい。東京に比べればタクシーは安いんだけど。ゆいレールは

　　23:42

まである。平日は23:54か。

うちあるいは琉大は浦西から歩くと40分くらいですけど、タクシーなら10分かからないかな。

登りは浦西は今のところバスでは使いづらいので微妙かな。でも、下りは使うでしょう。

トンネル区間が思ったよりも長い。

HPC VDI

最終日。Porco の発表時間を午後だと思ってたら午前中だったというミスが。すみません。琉大からだとタクシーで大謝名からバスみたいな変態経路なので...

自分の発表は割と手抜きな感じで。次期システムな話。SAN抜きのSSD/RAID構成ですが。Ceph 使えばみたいな話が。その辺は百鬼夜行できっと楽しめると思います。

Ubutsu 付いていけるの的な話も。いや、もうCentosはちょっと。そんなに大変なの? Ansible あるしなんとかなるでしょ?

VDI 自体はH.264使うのとかいろいろあるらしい。BYOD で持ち込んだデバイスのセキュリティの管理はしない。インターネットにはつなぐが社内ネットにはつながない。

いや、ちょっと杓子定規過ぎない? 電子会議をBYOD上のVDI経由って、それってちょっと。オフィス用途だとGPU VDIは不要なんていう話題も。

自分的には

　　VDIは、メインフレームのTSSの再来

なので、ちょっと違う感じあるかな。学生も課題とかはほとんどMBPで片付けてしまうわけで。でも、Mac Book Air だとどうかな。

OIST High Performance VDI Conference 2019

バスで来ました。先月もOISTには来てたな。明日も OIST にいる予定です。明日は夜までいます。

このConferenceも3回目かな。続いているのは素晴らしい。PCI 5 だと波形がなまるからみたいな話とか。

OIST側が「女性の発表枠」みたいなものを要求するらしく「なんでもいいから」見たいな感じで呼んだ人が何人か。
参加してくれた人たちありがとうございす。でも、そういうの「ちょっと違うものが混ざる」のが良いと思う。
もともと、いろいろ混じってる会議だしな。アカデミック系とも違うし。

自分の発表ネタはこれから考えます。

https://groups.oist.jp/ja/external-events/event/high-performance-vdi-conference-2019

4S

やっぱり高級感はあるかな。もっとも、

　　この小ささに戻る気はない

ですが。しばらくは、iPhone 7+ の予定。次は iPhone にこだわる気はないです。

金融系を iPhone に結びつけるのはリスクでもある。ICカードに対する利点もそれほど明確でもない。まぁ、

　　暗証番号やサインは絶対いや

って人もいるとは思うけど、そのリスクはカード会社が吸収するというのはバランス的には悪くない。

セキュリティをデバイスに頼っても、本質はリスクをカバーできるかどうかだから。

火曜日に集中するパターン

朝の歯医者から始まって授業二つとゼミでした。

　　OSは教科書買ってない学生が...

勉強する気あんのか?! タネンバウム使ってますが、なんかいいのないかな。

歯医者は詰め物詰めて終わりなんですが、なんか危ない感じが。仮詰めの相性が悪かったのか口内炎がつらかった。

少しお休みしてから帰ります...

ぼろぼろの本

ここ数年付き合ってる Higher order Categorical Logic ですが、

　　ぼろぼろ

Part 0 はA4にコピーして書き込んで読んでたり。最近だと PDF で読んでたり。つまり、

　　ぼろぼろにしたのは最近じゃない

無駄に持ち歩いていた時期が長いんだよな。重かったろうに。

もう一冊欲しい気もするんですが、

　　飾っておく用に

どうしようかな。

iOS 13

僕は先行導入とかは最近はしないので。速攻で、smart fullwidth space は切りました。

　　英語の一筆書き入力がすごい

速いし、oと入力するとiになるのとか結構困っていたので。辞書に載ってないとだめなんだけど。

ただ、そこで複数形じゃないしとかで戻るボタンを押すと「全部消える」おいおい。

あと、長押しするとカーソル移動ではなくて選択になる(しかも後ろを選択する)ってのがなんだかな。

カーソル移動は「チョン押し」みたいな感じにするらしい。

お医者さんから ingress

来週から授業が始まるし、OISTのGPU VDIのもあるし... で、血圧の薬をもらいにいくわけなんですが、来週だときつい。でも、

　　行きつけの医者はなんと土曜の午前中も開いてる

ありがとうございます。血圧はとっても低かったんですが、薬は要らないよねとはならず。

で、そのまま、気になっていた城間の緑を落としに。330からサンパーク通りを58まで抜ける感じで。

そこで弾切れになったので、松山公園で補給して、99番のバスで小湾まで。そこから興南高校のローソンに抜ける。

みたいな感じで楽しく散歩して来ました。昼間だと日に焼ける欠点があるがな。

のむりえ最終日

うーん、この快適なWifiがもう使えなくなるとは〜 そしてMBP広げるのにばっちりのカウンター

今日はいちげんさんお断り状態みたいです。というか、今週はそんな感じだったらしい。

たまに那覇に出てくるのが良い感じ。Ingress 的にも。ぷからーさだとちょっと遠くて。もっとも、大学から直行便があったわけではないのだが。

でも、なんかこう相性の良いお店だったな。そういうのってなかなか見つけられないからなぁ。

実は床屋のぐるぐるが目印だったんだよな。

天気の子(2回目)

2回観るものですかとも言われますが、カナと一緒に。

まぁ、ねぇ、池袋生まれだからなぁ。山手線で目黒まで通ってたし。

Ingress 始める前から歩くのが好きなので、東京の地図(東武デパートのリニューアルの時のか?)に歩いたところを書き込んでました。

Ingressで歩いたところもたくさん。池袋の北口通路とか山手線をまたぐ陸橋とか。また、

　　山手線から見た風景

が多い。

水没の設定はいろいろ微妙であるけど、代々木辺りの海抜は22mだったりしてあまり高くない。

温暖化で今世紀末までに1m上がるとかだけど、地盤沈下の方が影響が大きいという設定か。

CO2とか関係ないというのも良いけど、一人一人の選択で今の世の中になっていて、それは世界の形を変えている。そんな話かも。

https://kamode.exblog.jp/30392734/

銀河帝国の興亡

最初に読んだのは中1くらいか。1万2千年続いた銀河帝国の主星トランターで、心理歴史学者ハリ・セルダンが銀河帝国の滅亡を科学的に予知する話です。

二つのファウンデーションが銀河の二つの端に通常なら三万年ある滅亡後の暗黒期間を千年に短縮するように設置されるわけですが...

その後、この三部作の続きで二作、若き日のハリ・セルダンの話で二作、さらに、ベアとかベンフォードが三部作を追加。

なんだが、Apple TVでドラマ化って話はどうなった? 2019 じゃなかったのか? いや、まぁ、あんまり期待はしてないんですけど、

　　最初のハリ・セルダンの審問

は、やってくれるんじゃないかと期待してます。第一部のその後の展開は微妙なところもあるからな。

地球幼年期の終わりは割と良くできていたので、ちゃんとやってくれればね。第三部までやってくれるなら素晴らしいですが。

心理歴史学とかかっこ良すぎなんですが、現代的にはどうかな。まぁ、アシモフのはちょっとあれなんだけど…

歯医者

上の奥歯の詰め物が取れてしまって。割と怪しかった。結局、結構削られて「また来週」来週には授業が始まってしまうな。

下の方も歯磨きすると歯茎が少し痛い。まぁ、あとしばらくもってくれればとは思うけど。

少し鼻風邪気味で咳が出そうになるのが困りました。

虫歯は徐々に減っていて、自分たちの上の世代がかなりだめ。下の世代がかなり良い。QoLに大きく関わるので大切にしていきたい。

ついでに、海浜公園から伊佐あたりの緑を削っておきました。

2匹目

コタは、ちょっかいだされるとフーッとか言ってますが、カリも一応文句は言ってた。因果報応だな。

まぁ、もう少し涼しくなれば。コタもだいぶクソジジイになってきた。ご飯よこせとうるさいです。

彼方のアストラ

なんとなくネットの評判見て。最近は録画していても見ないのが多い。

いや、楽しかったですよ。バカものジャンルってあるよね。I'll とかとか。

設定なんとかプロットとかとかとか、まぁ、

　　わざとですよね

という感じで、惑星に降りてヘルメットすぐはずすとか、ぜんぜん、問題ないです。どんどんやってくれ。

最後に勝つのはばかと筋肉みたいな話だったとは思う。え、文章も書けたの?!

台風17号ターファ−

そこそこの台風だったので家に閉じこもってました。

　　植木が横になったくらい

天井ファン

割と合理的だと思ってるんですが... 加藤食堂のは動力なしらしい。これでも、それなりに効果あるみたい。

golang とOSの課題

OSの課題を Java から golang に変更中です。

　　InteliJ は Go Plugin
　　Jenkins も対応

GoLand とかいうのもあるのだが、InteliJ + Go Plugin とほぼ変わらない。なので、Java もまったくやらないわけじゃないから。

InteliJ は、やっぱり Java と同じで GOPATH が鬼門なようですね。まぁ、compile してしまえば。

ちょっとあれなのは、 UnixのAPIと、golang のAPIがずれてる。なので、

　　Unix のAPI( fork/select/pthread )を学ぶのに向かない

と言う問題が... golang は、それら(とCAS)で実装されてるわけなんだけど。その実装レベルまでやるのが自分の趣味ですが...

例えば、Unix の shell を実装して fork/exec を学ぶっのは golang には向かない。そうね。

channel は、socket とは別。そうねぇ。

golang のdebuggerが割とだめ。どうせ、channel base だしなぁ。

まぁ、いろいろやってみます。golang のモデル検査器があると良いのだが。

USB-C 電源

Ankerのガリ砒素欲しいかなと思って、頼んだら「ないので替わりのでいいですか」にうっかりウンと言ってしまったら、

　　届いたのは20Wのでした

まぁ、充電できないことはないらしい。そういえば昔、NiCd を急速充電すると傷むからトリクル充電とかやってたな。

軽いことは軽いです。非常用的な。

OSの補講

うっかり、教室を予約してなくて特別講義に取られてしまいました。まぁ、でもがらがらなので新棟で問題なし。

結構、人がいて「そのやる気をなんで去年出さなかったのか」という感じですが、まぁ、そんなものかな。

　　OSのinstallから

という感じのようです。

風速70mに耐える鉄塔

20年間びくともしてないようです。

西原の停電も毎回ではなくなった? 今年の台風は割とたいしたことなかったからな。

てだこ駅

坂田から駅に向かう道を作ってました。10/1 延伸なんだけどどうなの?

駅に接続するバスは125/25/97だが特になんのアナウンスもなく。一応、駅前には停まるのかなぁ。

これだと、よなラボからの道はなくなる感じなのかな。歩けるようですけど。よなラボは流行りそうだな。

ハリーズは少し遠いが流行って欲しいかも。

Game Jam と Okinawa.pm

321では明日でゲーム作ってるようです。Leap motionとWii Fitがネタらしい。

新棟では Perl の話。

こういうのは続けるのが重要。がんばれ〜

いうそばから Web が update されとらん...

https://okinawa.pm.org

LuaLatex and Agda source code

いや、前のblogで解決したと思ってたんですけどね。verbatim環境で表示されてないという技が。

LaTeXは数学環境とそうでないのとか、まぁ、いろいろね。

　　\documentclass{article}
　　\usepackage{luatexja}
　　\usepackage{fontspec}
　　\setmainfont{STIX Math}%
　　\setmonofont{STIXGeneralBol}[
　　　Scale=MatchLowercase
　　]
　　\begin{document}
　　\ltjsetparameter{jacharrange={-3}}
　　\begin{verbatim}

ぐらいでいくらしい。いや、ちょっと typewriter っぽくないんだけど。何がいいのかな。

どうでもいいけど、BloggerのGoogle検索って lualate と LuaLaTeXを区別するのか。

https://seeker-s-eye.blogspot.com/2018/04/lualatex-and-agda-symbol.html

層圏トポス

大学で読み会したのが79年くらいなんじゃないかなぁ。初版が出たばかり。この時は買ってないので図書館で借りたか...

その後、買ったと信じていたんですが、実家では発掘できず。結局、古書で買いました。

当時でも米田関手までは読んだはずです。この本は Hihger order categorical logic のかなりの部分をcoverしているのだと再発見しました。

直観主義論理の完全性まで入ってるし。ただ、証明は「明らか」とかが多くてなぁ。嘘つき... MacLane がその点は細かく書いてあるので素晴らしいです。

3刷ですが、後書きがかなり追加されてる。これは1.3版でしょうね。Bool代数とTopsの関係とか半ページでさらっと追加してあったり。

さすがに、ここ数年圏論やりまくったので、ふんふんと言う感じで読めました。いや、まだToposに手を付けてないんだけど。

Topos での coequalizer の証明はToposでは難しいが直観主義論理でやると簡単と書いてあって、実際そこに来ると「それはなんでもない」せ、先生...

圏の本を見るとHom Setが集合(small)かどうかがしつこく書いてあったりするんですが、さすが竹内先生で「そのあたりはこだわらないのが良い」とばっさり。

ちょっと前に少し locally smallって何って話を書いたけど、その辺の話ですね。Limitをfiniteで片付けてるのはそのせいだな。正しい判断だと思います。

今なら、圏論と直観主義論理を平行して読むのが良いんじゃないかな。でも、

　　証明の省略がひどい

のはどうしようもない。この本だけでは絶対無理。そこを Agda で補いながらか?

古書だけど、レシートが挟まってて。名古屋の丸善だ。なんと一緒に買った本がISBNからわかる。メタマス、オメガの冒険。不完全性定理とかの話の本でした。

ゼロエネルギーハウス

寮の駐車場を一部犠牲にしてなんかできてました。いいんだけど、

　　クーラーないんですが

実際に人は住まないだろうけど、それでいいのか?!

PC Museum の現状

琉大工学部1号館5階にあるPC Museumですが... いろいろ電源いれてみました。

　　PET2001 電源ランプはついて、CRTにも通電してるが、それだけ...
　　MZ-80 カセットからHu-Basicがloadできて起動! しかしキーボードが...
　　Sun (2004くらい?) モニタに「No keyboard found」。USBのキーボードがもう一つあるが..
　　PC9801 一回MSDOSがHDDから上がったのは見たのだが、それで終了っぽい。診とったか?

PC8001も置いておいて欲しいかなぁ。モニタがないんですが。

Sophica system の開発システムがあるのだが、マニュアルがなくて起動方法がわからず。

OIST

産総研の杉田さんに付いていったんですが道案内の役にしかたってなかったかも。なんとなくOISTのクラスタの話を聞くつもりでしたが、

　　杉田さんの空調の話がずーっと

ま、面白かったので良いです。明日は琉大で話してもらえるはずなので、聞きたい人はどーぞ。

明日は救命講習と重なったので、むしろ今日聞いていて正解だったみたい。

お昼にイルドレに寄ったのも正解でした。

http://www.iledere-okinawa.com

のむりえ閉店

え〜 9/23までらしく。だから「良いお店は通わないと〜」といつもで言ってるでしょ〜

普通にご飯とお酒があって居心地の良いお店で良いんですけどね。本当は酒抜きでも。

崇元寺通りの中之橋のバス停に近いのも得点高かった。もっとも、家賃は高かったかも。

まぁ、今までありがとうございました。今月は、何回かはいくと思います。

grammarly

英文校正サイトです。珍しく英文書いたので使ってみました。

　　冠詞と三単現なおしてくれる

まぁ、それだけでもうれしいか。actualy とか入れると「余計だろ」とか言ってくる。まぁ、そうかもね。

これも subscritpion かぁ。有料サービスの方はどうなんだろ?

お手玉

なんか母がヘルパーさんとたまにやってるらしい。もちろん、僕はこの手のは苦手。

なんだけど、ちょっとやってみる。

　　片手に二つずつ持って、順に投げて反対の手で受けとる

これを三つでできるようにするのが最初の目標らしいです。

なのだが、微妙に穴が開いてるらしく、中身が出てくるな。次練習するのはいつだろう?

台風レンレン

パンダみたいな名前だな。一応、強風圏に入っていて雨もそこそこ降ってますが、

　　沖縄本島は平常運転中

です。松山公園で久しぶりに補給しました。

Ingress lv13 まで来ました。Recursion デメリットないから、lv16までいったら、もう一回Recurseするか。

玉手箱

実家に置いてあるかなの洋服を送ってくれと言うので...

ゆうパックの箱でも買うか? なんだけど、コンビニで「洋服送るように箱ください」と言ったら、置くからジュース用の段ボールとか。

いや、それじゃ小さすぎるだろ。女性用のコートと言ったのに。これだか男は... けむりで聞いたら

　　クロネコの配送所がバス通りにある

そうなかと思ったんですが、隣にイイダがあるので、結局、そこのお嬢さんに「女性用のコートを送りたい」と言ったら、

　　ばっちりなサイズの段ボールが登場

だよな〜　二つもらったんですが一つで収まりました。適当にほいほいと入れただけ。

でも、かなも開ける気にならない玉手箱のようです。絶賛放置中。

台風? ま、これくらいなら普通にしてるんじゃないですか。

飛鳥山のリフト

なんか頂上駅とか書いてあって何かなと思ったんだけど。

この手のバリアフリーというか贅沢というか無駄というか、割と好きかも。

Safari の Reading List と tab

うっかり間違えて入れてしまうことの多い Reading List のことです。

自分では良く見るのを一つの Bookmark folder にまとめて、Favarite Bar に入れておき、automatic replace tabs で

　　そのfolderのbookmarkを全部tabで開く

ってのを使ってます。tabs って名前にしてます。これをclick すると全部いっぺんに開く。

Reading List は横のメニューになるのだが、

　　clickすると、それを今から開けにいく。次のも今から開けにいく

でも、tabs 方式だと、次のは既に開いているので、開けにはいかない。

最初にまとめて開けるのに時間がかかるはずだが、

　　セッションを開けて接続するまでは待ちで何もしてない

なので、tabsでいっぺんに開けた方が IO thread 的に早くなるらしい。もっとも、

　　日経のID処理はたこなので、日経だけ遅い

日経って認証用に一度画面遷移するので並列処理を邪魔してるらしい。

というわけで、やっぱり、Reading List は役立たずで automatic replace tabs 方式が良いらしいです。

首里のダブルツリー

Hilton 系ですが、昔はグランドキャッスルだった。JAL系になって、それでHilton系ですね。

建物古いので天井が低いとか、昔の煙草の匂いがとかあったけど、まぁ、なんとか維持できてるかな。

レストランは変わってなかったり。今日は中華を使ってみました。昼に点心でビールは危ない。

斜めに降りる道があるので、山川ではなくて山川二丁目で降りる方が良いのか。紅型研究所とかがある細い坂は首里っぽい。

なんか下って、右に抜けて市立病院駅に抜けられるのか。それは知りませんでした。途中に真嘉比遊水池があるな。

Lush の...

石けんですね。新宿東口のLushは三階あって結構楽しかった。

食べられないのが残念。

男性にはスーッとするタイプを勧めるのは定番なのか?

locally small

こっちは圏論の話。圏論の本では良く出てくるんですが、

　　locally small とは圏のHom Setが集合なこと

って、何っているんだかさっぱりわかりません。そもそも圏論だと集合論やらないし公理も出てこない。

なんだけど、Agda で圏論の証明をやってると、

　　Hom Set の等号 ≈ には cong がない

ってのに気がつく。cong は congruent 合同なわけですが、

　　cong-≈ : ( x y : Hom A a b ) → ( f : Hom A a b → Hom A a' b' ) → x ≈ y → f x ≈ f y

のこと。Hom Set の等号は関係なので f が関係を保存しない限り、結果が等号になるかどうかはわからない。つまり反例がある。
群の写像があったとしても群の構造を保存しないなら準同型写像にはならないというわけ。圏の対象は群だったりするから。

なんだけど、集合なら

　　cong : ( x y : A ) → ( f : A → B ) → x ≡ y → f x ≡ f y

になります。これは Agda 的には x ≡ y が

data _≡_ {A} : A → A → Set where
refl : {x : A} → x ≡ x

と定義されてるから。つまり「項として単一化されるものが≡として等しい」ってことは、

　　項として同じ正規形を持つなら等しい

ってこと。λ式として記号的に等しいってことでもあるな。ということは、

　　圏論で Set ってのは、λ項の世界のこと

なわけ。なるほどね。Agda のSetであって、集合論のSetではないと。

　　≡←≈ : ( x y : Hom A a b ) → x ≈ y → x ≡ y

があれば、 cong-≈ は cong から作れます。上の逆は ≈ が同値関係なことからでるので。これは上の反例があるのでAgdaでは証明できません。

なので、≡←≈ を仮定して使ってれば locally small を使ってることがわかるわけ。

さらに、何か I : Set があって、

hom→ : Hom A i j → I
hom← : ( f : I ) → Hom A i j
hom-iso : hom← ( hom→ f ) ≈ f
hom-rev : hom→ ( hom← f ) ≡ f

であれば、確かに Hom A は集合だと言えます。正確には「ある集合に isomorphic 」だな。

じゃぁ、どういう局面で locally small と使うかと言うと、

　　cong-≈ を使いたい時
　　Hom Set と集合を対応させる時 (そのまんまやん)

一つは Sets の Completeness つまり Sets でのLimitの存在を示す時。同じだけど、 Limitを equalizer と product から作る時だな。
もう一つは米田レンマを使う時ですね。 フロイドの随伴関手定理は米田レンマを使うので locally small を使います。

これだけかな。

≈ は同値関係なので、 locally smallness は対応する同値類があることに相当します。じゃぁ、同値関係あるのに同値類作れないことってあるの?
選択公理がないと代表元が取れないので同値類を集合として作れない場合があるらしい。やっぱり選択公理お前だったのか。集合論に戻ってきました。

Product in ZF

結局、ZFいじってたんですが、

　　濃度を定義するのに onto-map 上への写像を定義する
　　そのためには写像を集合の関係で定義する

で、結局、pair から ordered pair を定義する羽目に。そこで、pair が間違ってることを発見。

いや、別な公理を使ったのかも。結局、論理式で、

　　λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y )

とするだけなので、どうってことなくて変更もたいしたことなかったんですが...

その後の ordered pair が迷走することに。論理式つまり一階述語論理で記述すると、ほぼ教科書通り。

なのだが、数学の教科書って、

　　省略しまくり

そして、Agda では省略は許されない。といっても大した量ではないんですけどね。

全部教科書通りというわけにもいかなくて、ZF→ZF ではなく Agda→ZF なので、ZFの集合とAgdaのデータ構造を対応させる感じ。

ordered pair はこんな感じ。

　　<_,_> : (x y : OD) → OD
　　< x , y > = (x , x ) , (x , y )

pair を使って表す感じ。普通は {{x},{x,y}} と書く奴です。これを使って、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

　　ZFProduct : OD
　　ZFProduct = record { def = λ x → ord-pair x }

こんな感じに。これで、pair ox oy が < x , y > に対応します。ox は集合 x に対応する順序数。

これで、直積の性質(射影π1,π2とか、uniqueness)とか示せば良いのだが、射影は簡単

　　pi1 : { p : Ordinal } → ord-pair p → Ordinal
　　pi1 ( pair x y) = x

そのものだ。constructor も普通。introduction とかいう奴ですね。

　　p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
　　p-iso1 {ox} {oy} = pair ox oy

ところが、uniquness (elimination)がわからない。わかってみれば簡単なんだけど。

　　p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
　　p-iso {x} p = ord≡→≡ (lemma p) where
　　 　　lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
　　 　　lemma (pair ox oy) = refl

data の定義が uniqness つまり、 p ≡ od→ord ( < ord→od x , ord→od y > ) を要求してる。そういえば、

　　data ord-pair : (p : Ordinal) → Set n where
　　　 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

だからな。でも証明の項は、

　　 　　lemma (pair ox oy) = refl

refl は x ≡ x のconstructorだけど。pair の型の unification でそうなるんだけど、気づいたのは4日目の飛行機の中でした。

まぁ、そんなもの。分かんない時は、どんどん横道にそれちゃうんだよな。ま、わからない時には refl って書くのがAgdaだが。

残りは面倒なので気が向いた時にでも。

果実園リーべル

まぁ、fj 同窓会なのかな。新宿だなと思って副都心線で。

　　新宿三丁目で降りて、地図を見ると「明治神宮の裏の渋谷区役所のところ」

あれとは思ったんですが、取りあえず、そっちに。区役所しかない。案内のお姉さんに相談したところ...

　　代々木三丁目はもっと新宿の方

げ。で、もう一回クリックすると新宿の方に。くそ〜 おそらくは移転前のとかが地図に残ってる。

ところが、その辺って駅まで遠い... なんかコミュニティバスがあるので乗ったのですが、

　　山手線の内側まで廻ってから、ハチ公前

おかげで、30分遅刻。

おかげで、ふぢーネーネーとゲーセンで遊べて面白かったです。CHUNITHM っていう奴。僕は苦手なんですが。

　　なんか 1000 combo とか飛ばしてる兄ちゃんを目撃しました

実家のリフォーム

壁と床の張替、一階二階のトイレの更新、浴室の棚の更新ですが、

　　見た目、まったく変わらない

俊子の方針で、少し色あせた、そのままの色で更新したみたい。

どちらかと言えば怪しくなってる風呂と湯沸かし器をなんとかして欲しい気もする。最近、浴室に手すり欲しい気もするし。

まぁ、お好きにどうぞというところですね。母の面倒見てもらってるので頭は上がりませんよ。

Gris

画面の綺麗な iPhone のゲーム(600円)。なんだけど、

　　アクション系

つまり、結構難しい。なんか飛び移れなくて。プレイ動画を見たら高さが倍くらい違う。それは無理。

しばらくやって判明したんですが、

　　double tap ではなくて、途中でぐっと押し込むような感じ

3Dではないんですが。先に進めると、二段ジャンプできるようにもなる。そんなこんなで、

　　指がつるゲーム

でした。まだ、上がってません。プレイ動画を見るだけでも楽しいかも。そっちがメインなのかもな。

いつもの習志野

介護施設にいる母の妹ですが、末の妹夫婦に車で送ってもらいました。

　　高速はがらがら

人が年老いていくのを見るのはつらいものだけど、昔、良くしてくれた思い出があるからな。

今回は成美おばさんの反応は前回と同じような感じだったんだけど、母が積極的に声をかけていた。

なんか張ってあった「上を向いて歩こう」を歌ってたし。そんなわけでは母はご機嫌でした。

デーサービスでも歌うたったりとかしてるのかな。少し母のデーサービスの現場も見れました。

お見舞いだけど、結構、エネルギーがいるもの。一緒にいくのが良いかな。

お休みなので ingress

いや、休みでなくてもやりますが。一昨日は昼間は、

　　池袋から中野まで関東バスで

あと中野のモール。今日は、

　　東池袋から都電で三ノ輪橋まで行って都営バスで戻ってくる

予定だったんですが、途中、飛鳥山が白ポなのを発見したので途中下車。そのまま、予定通り廻りました。

三ノ輪橋でバス停さがすのに手間取ったけど。ちゃんとぐぐれよ。

既に歩いてるところが大半ですが、飛鳥山公園は初めてだな。線路沿いから登る道とか、ケーブルかーとか面白い。

今日一日で200グリフハックポイント取れて500まで行きました。千は、まぁ、頑張らない予定です。火曜日までだっけ。

なんとなく都営一日券買ったけど、元は取れてないな。都電170円は安い。

寿司食べ放題

昨日のMeeting、あんまり、良く見てなかったんですが、秋葉原の寿司食べ放題でした。良く見てなかったので、

　　お昼は中野の回転寿司で千円分

だった。三崎口とかそんな名前でしたが、割と良かった。夏の五巻盛り。

僕自身は食べ残しをうるさく言うのはださいとは思っていて、外食とかどうせ量多いし、ご飯半分と言っても多いから普通に残します。

なのだが、おそらく「お寿司いっぱい」ってのをやりたかったんだろうなぁ。まぁ、子供っぽいとは思いますが。(ボケが始まった説もあるが)

3人なのにいきなり60巻とか頼まれてしまって... まぁ、そこそこがんばったんですが、そこで追加を頼むのか。本気ですか。

　　まぁ、でも、そこで止めたりはしません

残った分は罰金取られてましたが(他人事)、まぁ、1巻100円だったが少し負けてくれたみたいです。寿司は、まぁ、食べ放題だから、そんなものでしょう。

その後も行きつけの店によったりBarに寄ったりしたので、ちょっと今日は二日酔い気味です。

お土産はまだ開けてないんですが、明日かな。