Wednesday, 28 June 2017

新しいMBP

EnPITの予算関係でもらえるらしく。EnPIT ありがとうございます。学部でやってくれっていうのも、通って嬉しいです。

今のMBP、結構、引き継ぎ引き継ぎで来たので、さすがに clean install でいこうかなと。ほとんどのファイルはサーバ上にあるので、無理に手元におかなくてもよいかな。

つうか、このまま移行すると、ラズパイのimageとかあるので、かなり時間かかるはず。670GBも使ってるな。

というわけで、つまり、あんまり移行できてません... Ansible とか Docker みたいなので minimum install したい...

iCould にデータを全部移すかみたいなのが出てくるけど、ちょっと高いのがな。1TBなくすとか、また、せこいわざを...

File Vault とかもデフォルトで入れようとするようですが、 もちろん拒否。

無意味なセキュリティのおかげで、OS X上のOSの課題がめんどくなっているのがいくつか... dtrace とか gdb とか。

Unix系は、だいたい brew で入れられるはず。

Xcode
X11
TeX
Agda (Emacs/Haskell)
X11のAgda用のfont
hg
perl/Tk
nmh
ラズパイ用のqemu
Virtual Box
VMWare fusion
Papers3
FreeMind
Omni Graffle
Google Photo Backup
QuickRes (なんか有料になっていた...
滅多に使わない LibreOffice

あとは自前のPerl script 群か。Dockerも入れたんだが、ほとんど使ってない。

Google Drive も、もっと積極的に使って良いのかも知れんが、あんまり、気が進まなくてなぁ。

Monday, 26 June 2017

フードフリー and 黒ガー

日曜日は、いつもの宜野湾のフードフリー。なんですが、

割とすいてました

なんでかな。宣伝不足? 良くあるのは宣伝担当者が変わったとかかな。

で、真夜中に Ingress Guardian が150日に。1月辺りにも139までいったのがあったんですが、屋富祖だったので、最近activeになった緑(gurukamaとかfound000とか)にやられました。

1月に青の作戦があったんですが、

http://seeker-s-eye.blogspot.jp/2017/01/okinawa-ingress-resistance-operation.html

その時の反転ポータルの処理のやつみたいです。真夜中にあんなところに取りに行ったのか。

この所、沖縄は緑優勢。宜野湾真栄原も「網羅的に焼く」人が何人か。いや、僕もいろんなところを網羅的に焼きにいくわけですが。なので、真栄原辺りだとガーポは厳しいかな。

もっとも、ご近所指向の僕が取れるくらいなので、沖縄のIngressのactivity自体が結構落ちているってことだろうな。

Tuesday, 20 June 2017

土砂降り

今日は土砂降りで酷い目にあいました。

沖縄だと台風以外だと珍しいんだけどな。周回道路が川になってました。

まぁ、僕の移動がすんだら止むんですけどね。

Sunday, 18 June 2017

小澤の不確定性原理

昨日のOSCの飲み会でビール飲みまくっていたら「先生どこですか」的な呼び出しが研究室OBから。なんで沖縄戻ってきてるのと聞いたら、

* 科学基礎論学会/科学哲学/科学史
http://phsc.jp/conference.html

ぐ、懐かしすぎる。ぜんぜんアンテナに引っかかってませんでしたが、琉大でやってるのか! で、プログラムを見ると、

*  出口弘
*  小澤正直

ぐ、懐かしすぎる。東工大の吉田夏彦先生配下な人たちではないですか。

なんですが、さすがに三日連チャンで早起きは無理でした。遅刻しつつ、小澤さんの発表を聞くことができました。

*  σ(P)σ(Q) + ε(P)σ(Q) +ε(P)ε(Q) > hoge

だったかな。Hiesenberg のドイツ語の論文のアブストラクトとかが出てるのが吉田研っぽくって面白かったです。不確定性は indeterminancy から来ているのだけど、元のドイツ語は inaccuracy に相当する言葉だったらしい。それを英語の共著者が inderminancy とまずい訳をしたと。それにEinsteinが引っかかって、あんな議論になったかと思うと、まぁ、そんなことはないと思いますが。あの議論は量子力学の定義の精密化には訳なったわけだし。

というわけで、懐かしい面子に会えて良かったです。

Saturday, 17 June 2017

OSC Okinawa 2017

いつもの内輪の展示会ですね。そういえば、両親も業界の内輪の展示会では暇そうにしていたっけ。

展示はいつものなんですが、セミナーのネタがなくて。なので、

* 2月にいじっていた cmake の入門をやろう

と思ったわけですが、聴衆は自分の学生以外は三人でした。ま、まぁ、地味な話だからな。

cmake は、mavenとかgradleとかに近いかな。make が、わりと魔境になってしまっているので、

add_target ( target_name source1.c source2.c )

だけで、いい感じにやってくれるのは便利。まぁ、そこからいろいろやろうとすると、どうせ魔境なんだけど。

今回は自治会館。コンベンションセンタ、あるいは、OISTよりは、はるかに便利なところ。特に今日は雨だったので、沖縄では珍しい「駅から濡れずにいける会場」なのはうれしい。

Friday, 16 June 2017

GPU VDM

https://groups.oist.jp/external-events/event/gpu-accelerated-vdi-international-conference-2017-asia

いや、まぁ、琉大にはGPUクラスタないし。システム更新でも「GPUは毎年新しいのが出るから」で見送られたりしたので、いや、だったら、毎年なんか買えよ〜

と言うわけで、少し場違いなわけですが、まぁ、全然関係ないわけでもないしなぁ。今年の2月ぐらいはMac ProのGPUと格闘してたし。というわけで、プレゼンもすることに...

OISTなので、学生に車で送ってもらうわけですが、

8時と言ったのに、ぜんぜん来ない

間に合わないよ、で、かなに「すみません、送ってください」と頼んで階段を降りたら、下から登ってくるうちの学生が。「道が混んでて8時に出たのに30分かかりました」って、いや、そこ「8時に迎えに来て」って言ったのが「8時に迎えに出る」になっているところが、沖縄なんだよな。

まぁ、僕も、そんな感じで、いまだに遅刻魔なわけですが。

そこそこお金取られたので、ちょっと厳しい。学生の分がな。

そして、明日は OSC Okinawa です。そっちも、よろしく。一応、うちの学生のcmakeのセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。

Tuesday, 13 June 2017

Prolog とシーケント代数

去年も今頃授業でやっていたみたいです。関数型言語と同じで、

*  プログラム中での変数の論理的関係が理解しやすいように記述する

ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。

Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。

でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。


Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'

これだけだものな。

実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。

Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。

アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。