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は教科書買ってない学生が...

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

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

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