Sets の Completeness できた

集合と射の圏 Sets が Limit を持つっていう奴なんですが、なかなかできなくて。Product と Equalizer は割とはやく片付いたんだが。

6月ぐらいに Stack overflow に投げて諦めてたんですが、

　　8月に解答が付いていた

のに10月になってから気がつきました。

やっぱり、Heterogenous Equality を使うんだが、λ式を避けるとできるらしい。

そこから、また少しすったもんだはしたんですが、結果的には Heterogenous Equality の Functional Extensionallity と Irrelevance を書いてやるとできました。

3月ぐらいから、はまっていたので、ちょっとうれしいです。

https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda

PS4

PS3 の一台が壊れてしまったので、ちょっと不便をしてて。で、PS4 を買ってみました。初代がかっこいいのだが、安い最近ので。Pro ではありません。 DLNAクライアントは結構快適。さくさくだ。

残りのPS3も時間の問題なので、少し、残ってるPS3のゲームもやらないと。FF13 三部作とか... なので良くわかりませんが、PS4買ったのでPS3のゲームやってたりします。

歯医者さん

なんか左上の奥歯の奥が不調で。といってもたまに痛むぐらいなんですが。繰り返しの治療が必要らしい。これくらいが歯医者さんのお得意様なんだろうな。いや、もっと金かける人たちか。

治療するたびに詰め物をはずすわけですが、で、「外れない時は外れないのですからね」というわけで、

　　詰め物にポッチがある'

これが結構気になる。ポッチといっても小さいんだけど、別にもっと小さくてもいいんじゃないの?

　　ポッチ

としている必要ないだろと思うわけですが。

まぁ、気になったら来てくださいとか言われたけど、そこまででもないかなぁ。

どうせ細菌が住んでいるだけだろうとは思うのですが、身体のあちこちにそんな細菌の巣があるような気がする。たまに痛みます。

学生のやりたいこと

プログラミング3/4 は、自分のやりたいプログラミングプロジェクトをやる授業なわけですが...

　　学生のやりたいことって、実は、はっきりとはない

まぁ、そうだよなぁ。

それでも、4,5年前は、いろいろ言ってきたものなんですけどね。今は、

　　先生の顔色を伺って、望む答を探す

なんだよそれ。聞いているのは「自分のやりたいこと」なんだけど。そういう意味では、

　　機械学習をやりとか、VRをやりたい

とかは、僕のご意向とは違うよな。必要なら使うけどさ。

普段の自分の生活で「これが良くない」とか「これが欲しい」とかを見つけて、それを改良したり実現したりするってのもよいと思うんですが、

　　ちょっと、こじんまりとしているかなぁ

別にそれが悪いと言うわけでもないですが。TreeVNC とかは、そういう風にできたものだし。

先輩達のやってきた、あるいは、やろうとしてきたことを聞かせると「おぉ〜」とは反応しますが、それも期待の反応をしただけか?

ちまたのほげほげコンテストとかほげほげハッカソンとかメーカーなんちゃらも、

　　そういうアイデアの行き詰まり

の結果なのかも。何をすれば良いかわかってないのは、こちらの方かもな〜

クラウドの課題

OSの課題にさくらクラウド上にVMを作るってのを出しているんですが、

　　ssh でloginするぐらいしかしてないから、要らないんじゃないか

ってな話が。まぁ、学科のサーバ上にVM作るのと差はないからな。

でも、まぁ、その差がないってのを学ぶ課題ではあるんだけど。そもそもAPIが、さくらクラウドのとは違うので「ぼたんぽちぽち」感がない。

じゃぁ、どんな課題が良いのと聞いてみると、

　　Web service の tuning contest

って、この間やってたあれ? まぁ、出してもいいけど。

徐々にクラウドの比率が上がるんだろうとは思うんですけどね。センタ側ではAWS結構使われている説もあるらしく。

円の描画

ちまたで、Illustrator の円はベジェ曲線による近似で誤差があるみたいな話が。

昔、マイコンの自作をやってた時にはグラフィックスは自分で書くわけ。誰も書いてくれないので。それで、マイコン雑誌に載っていたのが、

　　DDA Algorithm http://tinyurl.com/qa48sjv

ですね。その当時、東工大では Fortran の演習があって。ちなみにカードだったんですが。それで DDA で円を書くのを提出したことが。「なんで、そんなのやってるの? 他にもアルゴリズムあるけど」みたいなコメントが付いてましたが、だったら、その他のを紹介して欲しかったかな。

で、それで実装した自前のグラフィックで遊んでました。まぁ、ライブラリ書いた時点でかなり満足してしまうものなんだけど。

その後、大学院でレーザプリンタが導入されるわけだけど、こいつにも「円を書く」とかいう機能はなくて。PostScript 以前の時代だから。で、

　　LaTeX書いた論文に図を載せる

とかいうと、やっぱり円を自分で書く羽目に。ところが、

　　円をアフィン変換する

必要がある。問題なのは楕円の回転ですね。DDAでやればできたんだろうけど、結構、面倒くさい。なので、

　　ベジェ曲線で近似する

方が簡単。ベジェ曲線自体の描画はやさしい。

いろんなベクタグラフィックスのフォーマットを相互変換する時にも、楕円の回転問題が出るので、ベジェを使ってました。

今は、主に OmniGraffle を使って SVG で表示してます。

Kindle 本

OSの教科書は Tanenbaum の Modern Operating System なんですが、一応、Kindle 本もあります。でも、

　　学生がなんか買えない

とか言ってる。おかしいなぁ。去年買って手元にあるんだけど。でも、unavailable とか出てる。

この Kindle 版かなりのクソで、

　　コピペができない

課題出す時に問題が写せない。なんだよ。さらに、

　　一つのデバイスでしか読めない

普通は、Kindle は登録デバイス全部で読めるんだけど、一回に一つの Kindle デバイスにしかdown load させない仕組みらしい。消せば他のデバイスに down load できます。

ま、重くないとか、その場で辞書ひけるとかの利点はあるんだが、

　　Kindle / Amazon くそすぎる

のは確か。まぁ、ペーパバックは買えるようなので、そっち買ってくださいってところだが...

なぜ、買えなくなったのかは謎だな。去年買ったのはとりあえず、そのまま読めてはいます。

英語アカウントと、日本語アカウントは、まだ使い分けているのだが、com/jp どっちもだめらしいです。

Modern Operating Systems: Global Edition
by Andrew S Tanenbaum et al.
Link: http://a.co/iFi1ipC

目医者さんと歯医者さん

眼の方は薬が効いているらしく、徐々に良くなっている感じ。診察でもそんな感じ。ちょっと、その眼底写真見せてくれませんか? まぁ、でも一喜一憂するものでないからなぁ。

歯の方は奥歯の方がちょっと奥がたまに痛くて。根治する必要があるらしく、9月は割と通ったのですが、

　　薬入れて仮止め、また来月

みたいな感じ。血圧の方も薬を少し強いのに替えられちゃったしな。

まぁ、徐々にお医者さんのお得意様になりつつある感じ。まぁ、どれもそんなに高くないのが助かってるんですけど。

どれも診察とかあんまりたいしたことないんだよな。検査専用のクリニックとか用意して、そこで引っかかったら診察とか言う方が診察待ち時間がなくて良いんじゃないかなぁ。


Ingress のイベントの方は 450 まで来ました。500は明日には取れるんじゃないかな。2000は沖縄でも数人取った人がいるようです。根性とJarvisとUltra Linkですね。キー取るのがかなりつらいらしいです。一日50ぐらいのペースだと、それほどはつらくないです。

iOS, OS X upgrade

そんなわけで、iOS と OS X の両方の version up をしました。ほとんど差がないな。

先に、iOS 側をupdate 。OS Xは、xcode を先に update してから、High Sierra に上げる方法で。OSのupgradeよりも xcode の方がでかい。

どちらも特に問題なく上がりました。この前、SIP は外したのだが、OSのupgrade をしても外れたままだ。

今回の目玉は、もしかすると、

　　iCloud drive のファミリー共有

かな。App store のファミリー共有は、あまりにうっとうしくって切ってしまったんですが、iCloud drive なら使えるかも。

設定は iCoundのWebからはできなくて、MBPのコンパネから。え、なんだそれ。その場でパスワード入れてもらう方式もあるようですが、invitation 送るのが普通だと思う。

で、iCloud drive の容量を増やして... ってこれも、コンパネからかぁ。2TBにしましたが、どのように使うかは謎です。

昔の iTools/.Mac/MobileMe の時にも iDisk は結構便利だったんだが、いきなりなくなるとはね。Apple の Internet に関するセンスのなさは、今でも同じらしい。iCloud が無料になったのは良いけど、昔から有料で使ってきたユーザに対して、その値段の分のサービスを提供できなかったのは残念過ぎた。

iCloud drive をファミリー共有ありで引き継げていたら、そのままお布施してたんじゃないかな。

iPhoneのbackup だけなら、無慮魚5GBで十分なんだよな。

-

OSを上げないと...

iOS側とOSX側と一緒に上げよう思ってますが、少し憂鬱。でも、OSの授業では「最新のOSで」といってるのでやらんとあかん...

IngressのCF event は348まで来ました。まぁ、500はなんとかなるみたいです。

Ingress CF challenge

100は割と簡単に取れました。廻りのガチ勢も100までは楽勝らしいです。うちには、

　　初日で1000な人とか、600な人とかが...

初日に140いったので「理論的に取れることを実証した」とは思うんですよね。consequences are demonstrated ってやつね。

500まではいくとは思うんですが、まあ、2000は良いかな〜 (つうか無理)

既にある多重を反転してポータルを落としてお代わりするというのが基本的な戦略なので、ポータルをあまり堅くしないという風になるのは良いかな。AXA x 2 とか良くないなと思っていたので。