便乗値上げ

そもそも、今の若い人って、物が値上がりしていた時代を知らないんじゃなかろうか。給料も一緒に上がっていたりしたけど。

バス代が上がるのだけど、

　　回数券は、値上げ分を追加して払え

だそうです。小銭数えるのが面倒だから回数券にしてるのに。3%なはずだが、180円が190円なので、ちょっと便乗値上げされてる。こういう追加で払うのが多いらしい。小銭が大活躍だな。

そういうわけなので、バスの回数券は前もってたくさん買ってもあまりうれしくはないらしい。

便乗値上げで儲かった分がどうなるのかは知らないけど。

バスは、しばらく前に消費税とは関係なく値上げしてたな。モノレールも、いつの間にか値上げしてた。そういえばヤマト運輸が値上げとかの話も。

消費税が上がる時に、何もしないと不況になるってのが経験則だけど、今回は少しは何かしてくれるんでしょうか… 最低賃金は消費税分上げろとは思うけど。

蒼穹のファフナー

Left and right と Heaven and earth を見ました。お腹の調子は様子見中。

昼間から暗いアニメ見るなと怒られたりしたけど、まぁ、ファフナーは、そういうアニメなので。Left and right は救いのない話だけど「冷静に対処したんだな」とか、そんな風に思われるのは悪くないなと思いました。

Heaven and earth の方は少し詰め込みすぎで状況が良くわからず。あまり好きではない方向だけど仕方ないかな。来年の蒼穹のファフナーEXODUSの予習にはなったかも。

でも、本編の方、既に忘れているかも。レムみたいな、まったくコミュニケーションできない宇宙人という設定が面白かったんですが…

図を書いて証明する

お腹の調子がいまだにだめなので、今日は一日おとなしくしていることに。

なんとなく、Agda の System T のペアノ算術をいじってました。2の次は3ってのを S (2) = 3 とか書いて、0 と S (と再帰)で全部整数の計算ができるってやつですね。最初に見たのは高校の頃だったはずで、その時も簡単な演習はやったはず。

でも、Agda で書くと結構長い。まぁ、そんなものなんだけど。

　　(S(j)k)l = (jk + k)l = (jk)l + kl = j(kl) + kl = (S(j))(kl)

とかやるんだけど、ながいです。

そういえば、掛け算の交換法則(xy = yx) とか分配法則て図で説明してなかったっけ?

でも、xy = yx って、図で説明すると結局、x軸とy軸を入れ替えても面積は同じってのを使っているので、証明にはないな。

分配法則 (x+y)z = xy + yz も「足しても面積は変わらない」ってのを使っているので、あまり証明になってない。

そういえばピタゴラスの定理を図で証明するってのも、そうだったっけ。と思ったのだった。

西洋人は図形の認識が苦手て、全部、文字で論文を書くなんてもあったか。

VMWare Fusion 6

ずーっと、4 を使っていたんですが、何故か、

設定パネルが立ち上がらない

という状況に。機能的には4で十分なんだけど、まぁ、

Windows 税だから

と思って6に上げて見ました。upgrade で49$か。ライセンスを持っていれば、アカウントから、それを選択して終わり。それで治りました。なんだったんだ。

見かけは、少しUIが変わったかな。ちょっと、遅くなった気もする。

お腹の調子はは戻らないまま、

第4回地域間インタークラウドワークショップ
http://ricc.itrc.net/events/201403-workshop

の飲み会に行ってきました。飲み食いは問題ないです。iSCSI ではなく NFS でやる、その方が速いみたいな話を聞いて来ました。

System F

日曜日までお腹下して家でお休みしてました。カンボジアでなんかくらったらしいです。でも、もう治った(気がする)。胃腸の弱い僕だが、これくらいですんでよかった。白湯で乗り切りました。(いつものことだが)

System F は、いつもの難しい話ですが。といっても、System T みたいに、再帰で自然数やリストの計算をするみたいな話で簡単って言えば簡単。電卓っぽい。

System F は、二階の型付きλ式にエンコードしていくのですが、これが、

C++ の template
Java の Generic

とかと、そっくり。True / False とかは、Smalltalk 方式で、True にブロックを投げると eval ってくれるみたいな感じです。

Prolog の unification だけで、再帰抜きにプログラミングしていくみたい、と言っても誰もわからないか。λをfunctorで書いて eval を書くあれです。

そんな感じで、シェムリアップにいる間に、ほとんど Agda で書いちゃったんですが、結構、癖があるな。論文には「これで何でも書ける」的に書いてありますが、関数の組み合わせとかに制約が多くて大変そう。

まぁ、でも、だいたいの感じはわかりました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/45130bd669ca/system-f.agda

戻って来ました

アンコールワットと言っても学術調査とかじゃなくて観光だからね。でも写真は 7GB 撮ったらしいです。

遺跡の修復や発見はゆっくり進んでいるようですが、日本の援助によるものもあるらしい。それがカンボジアの観光収入につながるのは悪い話ではないよね。でも現地の人は「道路の拡幅で木が切られて木陰が減った」とか言ってました。どこでも、そんなものではある。この季節は木陰は涼しくて、ハンモックをたくさん見ました。

ホテルのネットの環境は割と良かったのですが、ネットはあまり見ませんでした。そのために行ってるわけだし。

ホテルのプールは真ん中は水深2mぐらいあって気持ちが良かった。と言っても一回しか泳がなかったけど。遺跡の登り降りの後で泳ぐ気にはなかなかなれない...

一緒に来た日本人は卒業旅行な人たちとか、60歳のお祝いでお金出してもらったけど旦那は置いてきましたなご婦人とかでした。いや、中国人が多かった。

学生は別にどんな旅行でも良いですが、

エスニックは食べられません。辛いものだめです。

なら、なんのためにカンボジアに来たんだよ〜　ちゃんと、耐性付けてから来いとは思いました。代々木のアンコールワットに近い料理も食べられました。(ま、お腹はゆるくなったが) というわけで、食事も良かったです。

週末は寝ていることになるはず...

そんなわけで

何故か、カンボジアにいるわけですが、

Wifi がつながれば、別にどこでもやることは同じ

ではあるよね。3/20 には戻るはずです。それまでは、音信不通です。アンコールワット見る以外は寝てると思います。

LSI デザインコンテスト

ここ数年さぼっていたのですが、ちょっと覗いてみました。最近の課題は、ハードウェアソフトウェア協調合成らしい。

http://www.lsi-contest.com

ハードウェアも興味はあったんだけど、ほとんど触ってない。FPGAやっているグループが、そばにいるので、それはもったいない気もする。

ハードウェアの方が定型的な処理は絶対的に速いんだけど、それは、もちろん十分な並列度がある場合。、画像処理やFFTを含む信号処理では、当然のように期待できるわけですが…

実際のアプリケーションだと、それが以外の部分が多くて、そこにはあまり並列度がなかったりする。なので、大きなアプリケーションをハードウェアにマップするのは、結構、難しいらしい。

並列計算機は、ハードウェアとCPUの中間みたいなところがある。今の Intel64 アーキテクチャは偶然の積み重ねでできてきたところもあって、ハードウェア屋さんから見ると「なんで、この命令ないの?」的なものが結構あるみたい。そこがはまえれば、HWSW協調合成も面白いと思うな。

いきなり Linux につながる合成ツールとかもあるのね。面白い。

OS研究会 5/14,15 沖縄船員会館

船員会館はぼろいんですが、泊港なので面白いとは思います。

http://www.okisen.or.jp

ぜひ、いらしてください。めーんそーれ。

懇親会は、この辺りだと、海のちんぼーら辺り? まぁ、どこでも困りませんね。立食パーティも可能らしい。この辺りはあやしい飲み屋さん街なので、気を付けて欲しいです。

日程で少しミスしてしまってすみません。

船員会館、プロジェクタ、スクリーンなしですか? まぁ、持ち込めば良いだけですが…　ネットはあるらしい。プロジェクタはともかく、スクリーンは置いて欲しいかなぁ。

5月には Open Source Conference も。頑張ります。

Coherence Space

まだ、Proofs and Types 読んでます。89年の本だから、もう古典なんだよな。何回か読んだけど、Coherence Space の所で挫折してた。今なら理由はわかる。

　　ちゃんと計算しろ

ってことね。証明を追っただけでは足りなくて、実際に集合を作ってみないと。Coherence Space は有限近似、つまり、有限集合だけで話が済むので、実は楽勝でした。 Φ(空集合)が未定義データを表していて、値が決まっていくと、それを∪で足していく感じですね(directed union)。これが、なんでわからなかったのか今では不思議。

もっとも、Stable Function の所で、pull back と filtered limit が保存するとか圏論の言葉で書かれているがするするわかるのは圏論復習したからだな。 Coherence Space を limit のある圏の自己関手として定義して、Stable Function を自然変換と考えれば Agda に載せられると思ったけど、できるかどうかは。

while program とか fixed point semantics とかの方がわかりやすかったんだけど、あれも、やっぱり問題解いていたからだろうな〜　

というわけで、今回は Sysetm F まで読めるようです。しかし、この手の理論は役には立たないのだが。もっとも、System F は Java のGeneric のような型変数の理論だから、珍しく役に立った方ですね。

、OSC2014沖縄 5月24日

え、ちょっと早すぎませんか?

4月7日(月)：募集締切（空きがあればその後も引き続き受付可）
5月24日(土)：当日　会場への荷物運搬

http://www.ospn.jp/osc2014-okinawa/

えーと、何、出展するか考えないと。とりあえず、申し込んでから考えるか。

去年は7/6だったんだ。

http://seeker-s-eye.blogspot.jp/2013/07/osc-okinawa.html

この時は Haskell ネタでしたが、今年はどうしようかな。

この辺りは沖縄は梅雨の最中ですね。

たどり着いたら、いつも雨降り

昨日は良く雨が降って。まぁ、僕は、

　　出かけると、土砂降りになる
バスに乗ると晴れる
降りるタイミングで土砂降り

ってなのが良くある。昨日も、飯でも食うかと大学を出たらばりばり降って、Mou が入れなかったのでガストまで歩くという羽目に。

でも、

張り子の虎ではありません

ので、大丈夫です。ちゃんとレインコート着てきたしな。

ただ、靴と鞄は、革だから、普段から、ちゃんと油塗っとかないとな。今の鞄の代替が、なかなか見つからなくて。修理という手もあるが...

特に blog のねたのない日

ま、そういう日も良いよね。

撮った写真からネタを探したり(食べ物は鉄板ネタ)、研究ネタとか、PCメンテネタとか探します。

そういえば、

ネットニュースが落ちてる
MailMan を使う

ってな仕事が降ってきていて、どっちも、微妙に動かない。いろいろ Firewall とか入れられてるからなぁ。

宮城隼夫先生最終講義

琉大に来る時に、翁長先生と宮城先生に東京駅に呼び出されて面接されたのを思い出します。「給料の話はしませんでしたが、安いです」みたいな話があったような、なかったような。本当に来るの? みたいな面接だったみたいです。

リヤプノフ関数は学部で習ったので知ってます。宮城先生らしくわかりやすい説明で良い最終講義でした。「ロシアの偉い先生とたまたま隣になった」いや、宮城先生、人生に偶然はないのですよ。いや、若い頃に、ちゃんとたくさん論文書くのは重要だと思いました。

翁長先生を久しぶりに見ましたが、まぁ、変わらないですね〜 お元気そうで何よりです。

Proofs and Types

学生と一緒に読みなおしてます。

ゲンツェンのシーケント代数の辺りから「あれ? こんなこと書いてあったかな」みたいなのが。一度、読んでるはずなんだけどな〜 こんなに Linear logic の話書いてあったっけ。

ちゃんと、ホワイトボードで計算やらせるからだな。そうそう、手で計算してみるまでは、何言ってるのかわからないものさ。

結構、飛ばしながらゲーデルのSystem Tまで来たんですが、最後に、

R は、It で定義できる

とか、さらっと書いてある。R も It も再帰を表す関数なんだけど、R は U -> Int -> U を使って次に行くのに対して、It は U -> U しかない。

f(n+1) = g(n, f(n))

と、

f(n+1) = g(f(n))

の違いみたいなものらしです。で、pair を使って、

<n+1, f (n+1)> = g(<n, f(n)>)

みたいにすれば良いってな話らしい。

これが結構面倒。で、Agda で、System T を書き始めたら、あっというまに数時間経ってました。玉手箱か Agda は。

うちに戻ってから、さらに、4時間ぐらいで証明できました。でも、System T と Agda の相性が良いというのはわかりました。

今回は System F まで、行きつけるのだろうか。

Proofs and Types (Cambridge Tracts in Theoretical Computer Science) by Jean-Yves Girard et al.
http://amzn.com/0521371813

宜野湾市役所から琉大

なんと、宜野湾市役所から歩いて、高速バスに乗れとグーグルマップが言うので。

坂をまっすぐ行くと近いんですが、そんな道あるわけもなく。バス停一つ。160円だそうです。

割と、高速バス本数あるのね。

http://buta.nahabus.jp/ryukyubuskotsu/busstop_show.asp?busstop=1592%20%2001

でも、階段作ってくれれば、そこを昇り降りします。

パスポートはできたら葉書を持ってとかではなくて、決まった日時にとりに行くだけでした。宜野湾市役所で取れるのは便利。ICチップで、分厚くなってました。

学科のブレード

使いこなすのに2年とは言わないが1年はかかるという。毎年、いろいろ変わるかならな〜

VM使わずに160台と言ったら、実はVMで運用されてメモリが足りなくて泣くとか。

VM中心に運用したら「マシンのメモリ全部使いたい」とか言われて、そこだけ一台切り出しとか。

稼働率はと言ったら「測ってない」みたいな話が。え? cacti は? VM単位? え、ブレード単位で良いんじゃないの? まぁ、いろいろ行き違いがあるな〜　クラウドにすれば稼働率はミエミエになるでしょうけど。(どうせ、そんなに高いはずない)

次期システムは KVM で組みたいとは思ってますが、なかなか難しいね。オンプレミスとかいう言葉も出てるけど、まずは、ローカルとクラウドの使い分けをちゃんとしたい。

今朝の地震

ゴーってのが長かったんですが、あまり揺れは激しくなく。それが少し時間を開けて二度。数時間後に、もう一つ。そんな感じでした。

沖縄は地震は少ないんですが、地球上どこでも地震から安全なところはないので。NYみたいに岩盤の上に乗っているとかならともかく。震源が近いのは珍しい。

本棚を止めると本が落ちる。でもゆれば幅が大きいとどうせだめ。でも、今回は落ちませんでした。実家の本は結構落ちて、母が片付けてくれたらしい。すみませんです。

喉かれた

二日続きの宴会で、酔っ払って大きな声で話しまくったので、声が枯れました。それだけ楽しかったということか。宴会での挨拶は、

お疲れ様

ではなく、

夜はまだこれから！

ということで。

でも、なんか舌も噛んだ。みんな無事に帰れたのだろうか(両日とも)。

う、また舌噛んだ。痛いです。でも、イベントは来週はあまりない。ゆっくり勉強できるね。