⊆

集合の包含関係なんですが、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 書こうと思っていたのに

間に合わないな