プロ4

好きかってなプログラミングをする授業プログラミング4ですが、今年は「勝手にどんどんやります」的な学生が4人ぐらい。なので、とっても楽です。

こじんまりとしてるのはそうだけど、あんまり高望みしてもね。このこじんまり感は今時の学生っぽい。

ちょっと前の学生は「ぶち上げて自爆」パターンが多かった気がする。

その前は自分で「ここまで、できるだろやれ」的な感じでやってた気がするな。着いてこれるなら、まぁ、良いんですけど。なかなか、そうもいかず。

サーバダウン

OSの授業でにこやかに、VMの課題をやろうと思ったら、

　　ssh できません

ぐ。先週も ssh できませんだったのに。先週は、NAT内のDNS serverと外向けのDNS server のどっちかを選ばないといけなくて、外向けを選ぶとNATの逆引きが中からできず ssh できない。内向けを選ぶと内部の外向けのサーバからは接続できなくなるという2択だったらしく。まぁ、どうせ外からは直接は接続できないので、適当な踏み台を選ぶだけの問題なんですけどね。

でも、いろいろ試してたら、

　　シス管のSlackになんか書いてあります

ってことで見てみると、

　　 今サーバー室に来てみてるけど, kernel 壊れたっぽい
　　 ```dracut-initqueue[259]: Warning: dracut-initqueue timeout
　　 Warning: /dev/centos/root does not exist
　　 Warning: /dev/centos/swap does not exist
　　 Warning: /dev/mapper/centos-root does not exist
　　 がでてboot 失敗してる

ってことで授業が終わってからの「シス管ミーティング」で、IPMI ( Dell の iDRAC っていう管理ソフト)経由で console にアクセスするんですが...

　　字が小さすぎて見えないよ

Javaのアプリでなんとかできるらしいんですが、さっぱり動かず。仕方ないので、サーバ室へ。要らないといったディスプレイスイッチで。

　　なんか緊急 shell かなんかに落ちてる。

「df コマンドないんです」え〜 でも、ls あるし、mount はあるし、fsck もあるぞ。log 見ると time out の連続かぁ。でも、sici RAID Controller の認識から sda1 sda2 までは正常なみたいだな。lvm command はあるんだが、

　　lvm pvscan

では何もでず。fsck もない。Boot しなおしてみると「ほら、Rescue boot あるじゃん」で立ち上げ見ると、さっきのと同じ。df ないし。しばらくいじっていたんですが、「CD付いてるし、CDからRescue しましょう」うんうん。

　　ちゃんと df, fdisk ある!
　　お、lvm pvscan でなんかでる。sr0? あ、そうか、CD差したからな

でも、もちろん、ぜんぜん、sda は表示されず。sda1 は boot partition で Linux 。なので、LVMからは認識しない。

で、いろいろググったんですが、lvm vgchange -a y しろとしか出てこず。lvm pvs で何も出ないのにそれは無意味だ。なんだが、

　　https://www.redhat.com/archives/linux-lvm/2006-November/msg00063.html
　　delete the partition within...

え、partition 削除するの? 結構、行き詰まっていたので、やってみるかと。partition はすぐに元に戻せるし。

　　delete してもなんにも起きず

ぐ。まぁ、なぁ。じゃあ、元に戻すか...

　　あれ? なんか、設定する値と、fdisk の示してる default value が違うんですが

じっと見てみると「0が一つ多い」ってことは、

　　一つ、partition が抜けてる?

そういえば、このシステムの設計実装した卒業生の城戸が slack に fdisk の出力載せてたっけ。良くわかるな。

　　結果的には、最初の一つのboot を除いて、全部、LVM volume

にしたら、それで lvm pvcan で認識しました。Rescue からはうまく認識しなかったんですが、

　　そのまま元ので立ち上げたら、上がりました。/etc/lvm の下がないと認識しないよな。

ここまで3時間。お疲れ様でした。でも、これくらいなら、今のシス管でも復帰できたんじゃないかな。

　　partition が壊れたのは、誰かがいじったせい

らしいので。command history に残っていたみたい。いろいろやって学ぶものだから、問題ありません。

研究室配属の季節

まぁ、それなりに人生を左右するイベントなんですが、どこに行ってもなんとかなるものなので。まぁ、相性もあるけど、それも、融通効かないわけでもないです。たかが2,3年だし。博士まで行くと結構長いが。

配属が決まると、カレーパーティだな。

その前に、コンパイラの授業の読み会があるはずです。

12/6-11 は東京にいますので、適当に呼び出してください。

というわけで、年末進行だな〜

Applicative Functor の続き

Applivative → Monoidal もできたので一通り終わりました。Applicative Law の使い方がさっぱりわからなかったんですが、

　　pure f <*> x = fmap f x

と、Haskelll の Applicative に書いてあって。これは、さらに関手の uniqueness から出ると。でも、Agda で書いた奴だと、そんな uniqueness なんか証明できそうにないんですが... でも、数字のリストとか、文字のリストとか確かに一意に決まる。

さらにググると、Free Theorem からでるとか書いてある。関手 fmap, fmap' に対して、

g o h ≈ k o f → fmap g o fmap' h ≈ fmap' k o fmap f

で、まさに関手の一意性なんんですが、そんな便利なものがあるのか? と思ったら、

　Agda では証明できないらしい
https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities

個々の具体的な関手では証明できるけど、可能な関手全部とかを取り扱うことはできないとかそんな理由らしいです。

でも、それがわかれば、あとは展開してまとめると同じ形になるって感じでした。

Ingress キリ番

100,000,000 は、あっというまに過ぎて諦めたんですが、今回は早めに。なんですが、5周年かなんかで、

　　AP倍

え、それって、偶数APしかもらえないってこと? 末尾は偶数。まぁ、諦めるかと思ったんですが、

　　なんか、末尾が奇数になる

履歴見ると、敵ポータルをグリフハックすると奇数になるらしい。あとは、

　　リンクで末尾6
　　リチャージで20
　　レゾアップグレードで130

あ、なんとかなるかな。で、琉大で調整したんです、

　　まだ10万AP足りず早過ぎた

なんですが、夜に屋富祖で少し壊したらあっという間にあと2万。

リンクはったり壊したりすると末尾が狂うし、グリフハックは禁止だしで、少しいらいらしましたが、最終的には寝床でリチャージで合わせました。

Applicative Functor and Monoidal Functor

なんか、Haskell のMonadがApplicative を要求するようになっていて、Monad を作るのが面倒になって困っていたんですが、そもそも、

　　なんで Applicative が必要なのか良くわからない

て問題が。

　　http://learnyouahaskell.com/functors-applicative-functors-and-monoids

とか、まぁ、面白いんだけど、

　　で、それって圏論的にはどうなの?

という疑問が。Functor は、

fmap :: ( a → b ) → f a → f b

で、これが関手の射の写像に対応するってのは、まぁ、わかる。だからなんなのってのは置いといて。

　　pure :: a -> f a
　　<*> :: f (a -> b) -> f a -> f b

こっちはなぁ。fmap の写像が関手、つまりHaskellのデータ構造に包まれてるみたいな感じ。

なのですが、MacLean には Applicative Functor とかなくて。で、

　　https://stackoverflow.com/questions/35013293/what-is-applicative-functor-definition-from-the-category-theory-pov

これによると、圏の積の構造を保存するFunctorである、Monoidal Functor と同じなんだとか書いてある。MacLean だと Monoidal Functor は一章使ってある。それかぁ。面倒くさそうなの避けていたんだけど。

で、Monoidal Functor ってのは、

unit :: f ()
φ :: (f a , f b ) → f ( a , b)

のことだそうです。あぁ、まぁ、積を写像しているような感じ。

** :: f a → f b → f ( a , b )
** x y = φ ( x , y )

としても良いらしい。逆に、

　　　φ ( x , y ) = ** x y

ですね。要するに引数に出てくる積は Curry 化でなくせるというわけ。そういう風に、Monoidal Functor から直積をなくしたのが Applicative Functor ってことね。

実際に、Monoidal functor と Applicative functor の相互変換もできるんですが、ちょっとしたパズルみたいな感じ。Sets だから射とかも集合の要素としてとってこれるので、変換できるらしい。つまり、

　　Sets 以外には Applicative Functor は無意味

な感じらしい。

ついでに Monoidal 圏と Monoidal Functor も Agda で1日で書けたんですが、忙しい時期にそんなことやってていいのか?

この後、Applivative law から Monodail law だすとか、その反対とか、Sets が Monodail 圏なこととか、いろいろやらないといけないようですが、ちょっと量が多い感じだな。


で、結局、Applicative Functor なんの役に立つの? ってことですが、まぁ、あんまり良くはわからないです。データ構造に写像も格納できて便利ってことかな。なんか最初の理解から進んでないぞ。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/808b03184fd3/monoidal.agda

沖縄寒い

今頃で20度切るのは珍しいんですけどね。南国行きたいとか言っているバカものも見かけました。

まぁ、Ingress にはちょうど良いです。うちのtop agentの cena 女史が faction change というのが最近の話題かな。Double Top とはやるな。

少しこまめに実家に行こうキャンペーンで12月上旬に、また東京にいこうと考えてます。その代わり、年末年始はパスかな。プロシンが後ろにずれたので、そんな感じにしようかと。

コンパイラの授業

いつもの授業ですけどね。途中から GCC とか LLVM とか読むわけですが、

　　放置していたGCC版のCbCを最新に対応させるか?

というわけで、GCCとLLVMの最新のを、うちのrepositoryに merge! いや、これ自体は授業とは関係ないんですが...

GCCは4.6から7なので、いろいろ変わっているわけですが...

　　ファイルの位置が変わっている

くらいかも。まぁ、そんなに簡単には移行できないだろうけどね。

GCCちょっと読んだので、来週はLLVMを読んで、その後は、12/1,2,3 で

　　Rakudo ( Perl6 実装)

を読もうかと思っています。YAPC もあるしな。

Windows 7 から Windows 10

まぁ、Windows とかロクなことには使ってないんですが...

　　OS X Marverkics 上のVMware Fusion 8.5 上の Windows 7

だったんですけどね。Windows 7 な Disk full とおっしゃる。VMだが60GBもあればいいでしょ? 100GBまで拡張するか。と、思ったら、

　　Snapshotを削除しないと拡張できない

え、てめーなにふざけたことをいってる。Snapshot こまめにとってるわけでないのですが、

　　VMWF は Snapshot の削除にとっても時間がかかる

まぁ、取りあえず削除は放り込んで... でも Diskfull って変だよな。っで、なんとかなったんですが、今度は、

　　共有フォルダに赤バツが付いてる

ぐ、なおらない。Windows って長く使ってると腐るんだよな。

そういえば、そろそろ Windows 10 にしても良いかな。それが罠だったわけですが...

Windows 10 は学科がライセンス保っているので、それをもらえば良いだけらしい。岡崎さんにDVDもあるとか言われたんですが「ないので、imageで」まぁ、それでも問題ないです。

で、image 落として、VMWare から入れるわけですが、

　　立ち上がって「インストールするイメージがない」で止まる

あれ? どういうこと? 8.5 で Windows 10 問題ないはずなんだけど。でも、新しいVMWare Fusion 入れてもいいか! と思ったら、

　　VMWare Fusion 10 は High Sierra でしか動かない

そこで諦めるべきだったんですが... いいや、ついでに High Sierra に上げるか。ところが、

　　App store が開かない

ぐ。なにそれ。そこでいつもの、

　　Shift 押しながら Safe boot

で、App store は治りました。そこから、High Sierra の install に。ちょっと待て。

　　Time Machine を止めて、別なHDDをつなげておく

そろそろ切り替えるべきだからな。よしよし。で、

　　問題なく High Sierra に

素晴らしい。そこで、VMware Fusion 10 を入れて。Windows 10が...

　　このハードはリアルモードをサポートしてません CPUID Early

は? 何言ってんので、しばらくぐぐったところ...

　　VMFware Fusion 10 は、2010 iMac では動かない

くそ〜 無駄足だったか。まぁ、それはMBPで使えば良いが... で、8.5 で Windows 10 が上がらないのはなんで?

　　簡易インストールを諦めてみると…

Windows のライセンスを入れるところで

　　ライセンスに対応するイメージがない

最初から言ってよ。なので、ライセンス無ならインストールできました。VMにinstallだとタイミングによって無効になったりするらしいが... こんなこともあろうかと、

　　ライセンスは二つもらっていた

ので、二つ目のラインセスを入れて解決。長い道のりだった...

Windows 10 ですか? キーボードの配置がJISでUSにならないのを除けば快適です。Windows 7 より遅いだけ。右クリックが多用されるので、Mac のマウスだと使い辛いかな。

コインランドリー

なんか、最近、派手で綺麗なコインランドリーが流行りらしく。うちの近所にもできてました。

で、少し冷かしに行ってみたところ、

　　河野先生ですよね

え? なんと、うちの卒業生が経営者らしく...

大学の勉強役に立った? と聞きましたが、普通にWebとかを使えただけで、直接には役に立ってないみたいです。

研究室にも、初期の頃のOBとか来てたな。ちょっと沖縄に戻ってくるのは早いんじゃない? とか思うけど、まぁ、それも良いか。

かばん壊れた

Twitter と同じこと書いてると言われるでしょうが、こっちにも書きます。年一回は壊れてる気がするよ。

バスから降りたら「バスっ」とかいう音とともにかばんが落下。もはや、いつものことなので驚きはしないんですが。

既に、付属の肩紐は使い物にならず実家の別なかばんの肩紐に交換済。なので、少し金具が元の違う。で、壊れたのは、肩紐側の金具かぁ。油さしておくべきだったかも。削れちゃうんだよね。

だいたい、革の方もリングになっているので、そこにOリングを通すのが良い。それが一番もつ。

　　最初から、Oリングにしておけよ!

と思います。デザイン的にもそっちの方が良いと思うし。

なんだけど、Oリングあったかな。4Fの実験室にいけばあるんじゃないか? メイクマンいけばあるのは知ってるのだが... なのだが、山田さんが「ここになはない。前も買った」というつれない返事。予算で買う時には余計に買うんだよ。秋葉原で電子部品買う時には必ず余計に買っていた。すごすごと部屋に戻ったのですが、

　　もう一度探したら、ロッカー置いてあったポーチの中にあった

旅行用のポーチでカミソリとか綿棒とか入っている奴。旅行には、Oリング必須だったのか。そうだろうなぁ。イギリスに行った時に既に、3.4kgのダイナブックをかばんで持ち歩いていたからな。

だた、キーホルダー用みたいな小さいやつなので、あまり保ちそうにないな。メイクマンにいくしかないか。少し余計に買うことにしよう。いや、既に買ってある可能性も高いな。

論理式と方向

いつもの Agda の話題ですが、論理式には方向がない 例えば、

　a = b

と書いてあっても、a が出力とか b が入力とかない。一方で、関数(λ式)には方向がある

λ x → y

では x が入力で、y が出力になります。

Agda だと、数学的構造は record や data で書きます。record は積で and でつながったもの、data は排他的論理和で case 文の集合みたいな感じ。

で、Agda の library とかを見ると、record Hoge と record IsHoge とかが組で出てる。良くわからなかったんだけど、どうも、

record Hoge ( input : InputType ) where
field
output : OutputType
isHoge : IsHoge input output

record IsHoge ( input : InputType ) (output : OutpoutType ) where
field
property : ppro inupt output

みたいに使うらしい。filed は名前と型、つまり、名前の付いた変数とか論理式が来るわけですが、record の引数は入力、field には出力、つまり、その数学的構造で存在が主張されるものを列挙します。例えば、有界な実数の集合には最大値にになる極限が存在して上界というとか、そんなの。

その入力と出力は数学的構造の性質(公理)が要求されるわけですが、それらは論理式なので方向性はない。それを IsHoge にわけて書くという方式らしい。

こうすると、

lemma1 : (input : InputType) → Hoge input → ...
lemma1 input hoge = ...

とすると、Hoge i での IsHoge の性質が使えるようになる。つまり、

∀ input → ∃ output such that IsHoge input output

というわけ。Hoge の存在を示す時には、

lemma2 : (input : InputType ) → Hoge input
lemma2 input = record { output = ... ; isHoge = record { property = ... } }

という風にするらしい。なるほど。

で、今までにやった圏論(クライスリ圏とかLimitとか)を、これにそって書き直したんですが...

　　仮定が余計とか、仮定が足りないとか

が若干でて、少しはまりました。一通り書き直して、だいぶ、見通しが良くなったみたい。普遍問題では入力は圏A,Bと関手Uで、それがUに対するLimitの存在につながるとか、ちょっとあやふやだったところが理解できたみたい。形式大事だな。

IsHoge のみで書くことも可能で、初期の頃のはそういう風に書いていて、必要なものは module input に書くとかしてたみたい。楽なんだけど、

Hoge → Fuga

みたいにならないで、

(x y z : ...) IsHoge x y z ... → IsFuga x w q

とかで、 x y z とかの仮定にいろいろ余計なものが入ったり、うっかり書きそびれたりしていたようです。

Programming 的には Hoge が interface で、IsHoge が実装だと言えないこともないかな。

Twitter の文字数

日本語 vs English だと

　焼肉 vs steak

っていう例を良く出すんですが、倍くらい違うみたいです。

Agda とかソースコードとか数式とかも twitter に書くのだが、すぐ足りなくなる...

なので、言語ではなくて文字でカウントして欲しいんだが。どういうカウントなんだろう。


Tweets 106K Following 5,989 Followers 5,907 Likes 94.4K

ぐらいなみたいだな。この間、6000 まで増やしたのに、また減ってる。思ったより Like 多いな。

目医者さん

「良くなってますね」

ということなので、まだ、少し残ってるようですが、薬は飲まなくて良くなったみたいです。

Retina で少し眼に負担をかけすぎたってのもあるかな。

生活習慣変えなければ、どうせ再発だとも思うけど... 血圧は低めになってきますが。

　　薬のせいもあるが、怪しい血圧計を新調した

のが大きいかな。

東京 short visit

既に帰ってきました。 母も歳なので、たまに長くいるよりも短くして、頻繁に行った方が良いかと思って。

でも、週末だけってのは「酒飲んで終わってしまう」なぁ...

　- * - * - * -

ついでに Agda も少しいじってました。初期の頃にやった equalizer と product から limit を作るという課題。Sets の Limit をやって、やっぱり少しおかしいことに気が付きました。

少し自力でやってみたがうまくいかず、Categories for Working Mathematician を見直すわけですが、

　　お前、前に読んだ時に何を読んでいたんだ?!

ってくらいに違うことが書いてあって。まぁ、でも、大筋は合ってたんだけど。一部の等式を、仮定を強力にして安易な証明ですませたらしい。だめだな。いや、おかしいとは思ったんだけど。Sets Completeness の時に使えなくて気がついた。

元の証明に Product 二つ足して東京にいる間にできたみたいです。

あと何やるのかは、まぁ、やっても良いものはたくさんあるが、Kan Extension とか、Cartesian Closed Category の一連とか。ZFC やってみるのも良いかな。

　- * - * - * -

なんか、xterm が勝手に focus 外れるんだよな。もう使ってる人はほとんどいないと思われるので誰にも聞けないところがつらい。

Blade Runner 2049

見てきました。なのでネタバレだいじょうぶになりました。

なんか時間の関係で4DXになりましたが、あんまり意味ないかな。4DXではまれる映画ってどんなものなんだろう?

年末にはスターウォーズも控えているのか。

こういう拡大再生産は、歌舞伎とか紅白歌合戦っぽいかな。