2012年09月

あー，彼岸花の時期は終わったかぁ．コスモスもそろそろ微妙かぁ？　紅葉前線はどこだぁ？

閑話休題．

モン・サン・ミッシェル行きのツアーが７月から９月の期間限定だった orz　楽しようと思ったけど失敗．ちゃんと計画を練るか．

閑話休題．

1年前に書いた下記の Haskell コードが読めなくなっている．修行が足らん．

fib((-1+)->n@((-1+)->m))|m<0=1|((,,fib n)m->(fib->x,_,y))<-()=x+y

閑話休題．

国際電話のタイムラグを体験．やっぱ微妙に遅れるね．

今日は満月だったのか？　とか考えつつ６時半頃に近場のトラムの駅へてくてく．

７時過ぎに LES AUBRAIS 駅に到着．パリ行の Intercites の切符を買って７時半ちょっと前に電車出発．

８時１５分くらいにオステルリッツ駅到着→メトロ５でバスティーユ駅に→メトロ１でルーブル美術館．残念ながら駅から地下に抜ける通路の扉が閉まっていたので8:45くらいに地上からピラミッドに並んだ．最初の折れ曲がりの手前には並べたけれど前回よりも前に並んでいる人の数がだいぶ多い．Intercites があと20分くらい早いといいのだけど，一本前は一時間以上前なので微妙．

そしてまたニケへ直行．でも既に人が……　スタートダッシュが足りなかった．

混んでるところを遠巻きに見るシリーズ：

なんとなく朝日の入り具合的に室内が金色に輝いてるように見えたのだけどうまく撮れない罠．あれこれしているうちに団体に占拠されてチャンスを逃した……

よくわからない工事中？　

お帰りは地下からで．セキュリティチェックがボトルネックだよね……　そのあとのチケット購入は自動券売機が意外と空いている印象．

人が多すぎてやる気なくしたので今回は２時間半ほど見て回って終了．久々にアジア系の人を沢山見た気がする．つか，列に並んでた前のグループ日本人だったし．

閑話休題．

せっかくパリに出てきたし＆レンズの焦点距離が足らんしということで，Eマウントの望遠レンズを見に Chatelet - Les Halles 駅のところのショッピングセンターにある Fnac に行ってみたんだけど……　Sony E 55-210mm F4.5-6.3 の値段が 349ユーロとかで kakaku.com の 30010円よりだいぶ高いという結果．悩ましいので購入は見送った．もうちょっと旅程が単純だったらレンズも沢山持ってこれたんだけどなぁ．

閑話休題．

今日の予算：ルーブル美術館入館料 11ユーロ，パリ・オルレアン往復 19.50ユーロx2，パリ市内のメトロ移動 1.7ユーロx3，合計で 55.1ユーロ（オルレアンのトラムは去年の10回券のあまり2回分を使ったのでカウント無し）．まあ，ユーロ安くなったしリーズナブルなお値段で遊んできた気分．

先週月曜の分の代休？　とりあえず新婚さんの新婚旅行にお邪魔してワイナリー２軒を見学して一緒に昼食という一日．

ワイナリーはオルレアンの中心から１５キロ弱のところ？　とりあえず詳細気にせず白いワンうまかた．おばぁちゃん良い人．ガメだったかのぶどうを食べたのだけどふつうに美味しいぶどうだった．渋い赤ワインにするのがもったいない？

お昼は Le Lift (www.restaurant-le-lift.com) というところで．Google map だと変なところに案内されて迷う事になるが，ウェブサイトの地図を見れば迷わない．トラムのA線が走っている橋から川沿い（中心部側）を東に向かって少し行ったところの左側にある．つか，レストランが屋上にあって駐車場はその建物の地下という構造（駐車場メモ：駐車券とって入場，駐車場に向かう階段を降りてく途中の地下１回の踊り場の精算機に駐車券入れて精算，精算後の駐車券を出口ゲートに突っ込む，というながれ）．そんなに畏まってないので行きやすい雰囲気．前菜・メイン・デザートで３３ユーロ．普段の昼食の４倍程度．

帰りの便を加算するとプレミア資格用のマイル数が 49000くらいになるらしい．３ヶ月弱に１回の周期でアメリカないしヨーロッパに飛べばそうなるか．

沖縄往復とかやってみてもいいかもしれない．

Android のバックグラウンドデータとか自動同期を止めただけではソフトウェアの更新とかは止まらないのね．そのせいなのか全然通信した記憶が無いのに第一のリミットいっぱいまで使われていたっぽい日が多数……　これまでの旅でも結構無駄が発生していたということか．

普段は音声通話しないのでパケホでトータル６千円なのだけど，今月は少なくとも３万超えでそれの５倍．約半年分と考えると高いかなぁ．

とりあえずデータ通信の大本を切っておけば大丈夫なのだろうか？　

とりあえず，すでにある仮定から導かれる複数の結論を同時に使いたい時にどうすればいいのかとかで小一時間悩む．apply すると元のが消えちゃうし……　とかやってた．面倒になって最終的に assert で必要なものを全部突っ込めばいいやという結論に達した．もしくは replace 使いまくって後回しにするとか．あとは仮定に conjunction が入っているときにその一方だけが使いたいんだよとかいう時には destruct H as [H1 H2] とか叫べばいいと学習．そしてペアの等式から要素の等式を得る方法がわからず，それをやるためだけの証明を別途自前で用意するとかいうアホらしさ．まだまだ色々と経験が足りん．

そして書き換え位置を特定する方法が未だにわからない．

リスト l の n 番目の要素を取ってくる関数 nth n l を定義するのに (n < length l) をつけときゃデフォルト値とか使わずトータルな関数定義できるよね，とかいう勢いで関数本体を書いてみようと思ったのだけどどう書いていいのかわからなかったという．結局，定義の頭に Program ってつけといてよくわからんところに _ （アンダースコア）置いといて，あとで proof obligation を始末する，という方法で定義できることを教えたもらったのでそれで済ませたのだけど……　定義された関数が読めん．そして定義された関数に関する性質の証明も訳わからん項が出てきて混乱する（再帰先で n < length l が保たれることを示すためにこの型を持つ読めない項が作られるので式の見た目がごちゃごちゃ）．依存型とか使いこなせない気がする．

丸一日寝てた．お陰で体調もあと一晩寝れば通常運転くらいに回復．とりあえず予想以上に寝不足と冷えすぎが堪えたっぽい．今日は気温も高くて幸い．

さて，防寒対策を練っておくか．

なんの予定もない週末とか結構久しぶりな気がするなぁ……　とか言いつつ論文の印刷に大学まで出て来たり．つか，でかいディスプレイを使うには必然的に大学に出てこないとならん．

それはよいとして，頭がいたいレベルで風邪引いてるので冬眠しよう．

予想よりも寒いのでやばそうだなと思っていたら喉と鼻がやられた．とりあえず週末は寝て過ごすか．

閑話休題．

Don't disturb 無視して突っ込んで来ないで欲しいんだけど……　ちょいと移動すっか．

普通に関数型言語として使うのは問題ないけれど依存型で変なことしようかなと思い始めるあたりでごちゃごちゃと……　Prop と bool の違いではまりまくるとか．どこに気をつけるべきなのかがはっきり見えないので修行あるのみ？

Coq 8.4 用のはバグってる？　生成される関数の本体であるラムダ式が型引数を通常の引数と同様に受け取ろうとしているような気が……　関数の型が合わないという文句を言われる．どうやら Haskell を吐いても Ocaml を吐いてもおかしいらしい．

とりあえず 8.3p12 用で我慢するか……　別の部分が 8.4 の機能を使っている気がしなくもないのだけど大丈夫かな？

つか，１日に２回も coq をコンパイルすることになるとは．

Coq を入れて proof general 入れてごにょごにょ．結構メンドイなぁ．証明の仕方がわかっても具体的に Coq をそのとおりに動かすのが慣れてないので手間かかる．うーん．

無事にお仕事その一は終了したが，お昼とかに周りの連中の会話を聞いていたのだけど全くフランス語がわからない．赤ん坊とかどうやって言語獲得してんだ？　とりあえず第二外国語はドイツ語だったし，フランス語とか基本の単語もわからない．出口が Sortie だとか駅が Gare だとか確定が Valider だとか程度の名詞がいくつか分かる程度の能力．

うーん，悲しいのでちょいとフランス語をお勉強しよう．

閑話休題．

時差ボケがまだ……

オルレアンへ移動した．RERのBが改装中につきシャルル・ド・ゴール国際空港から５駅ぐらいが使えないという罠にハマった以外は平和だった（バスで B のもう一方の端まで輸送中）．

さて，明日は仕事だ．寝るか．

ホテルの予約１日分間違ってたので面倒という罠．ま，いいか．

明日は早いので空港近くに移動．

荷物をぎりぎりの重さに仕上げてきているのでちょっと投げ捨てたい気分．適当に買った吊りばかりが意外と便利（超過料金払うギリギリの線を狙うのに）．

閑話休題．

ようやく scala のインタプリタの動作の感覚がつかめてきた．コンパイルできてもインタプリタでロードできないファイルが有るとかやめて欲しいんだけど．とりあえずデモるにはインタプリタのほうが楽なのでソースをゴニョゴニョ修正．インタプリタで読み込むと，頭から順に処理してくれるのでファイルの後ろのほうで定義しているものを頭のほうで使うと文句を言われるっぽい．本当にそうなのか知らんがとりあえず定義の順を直したら通った．

閑話休題．

来週の月曜って日本だと休日なのか……　月曜に海外でお仕事した場合って休日出勤扱いなのか？　よくわからん．

つまりはそういうことであったと．記憶力がない．

閑話休題．

Monoid とか関係なく図形のライブラリ作りましたな気が……　というか，Monoid がどう嬉しいんかが全くわからん．タイトルだけ見て期待していたのだけどビミョーな気分を味わった．

閑話休題．

PCの充電を忘れていた → ACアダプタを取ってきた → コネクタ忘れてコンセントに刺さらない罠．タコ足配線で大本しかコネクタかましてないので忘れてた．

閑話休題．

ペットボトルとかの回収システムが楽しい．中でくるくる回ってスキャンされるのでボトルを潰しちゃダメなのがちょっと難点だけど．

.forward にパイプでコマンド書いときゃ受信時にコマンドが実行されるんだっけ？　

あー，実行って誰がしてるんだ？　sendmail なのか？

ん？　/etc/aliases に書いときゃアカウントの実態がなくてもいいのか．

Delite の上のDSLの数が思ってたより多くて驚いた．分散バージョンがほしいね．

土砂降り．

トランポリン転がってった！

暗号化したままの計算は知ってたけど，秘密分散したままの計算とかも考えられてるのね．圧縮したまま計算とか暗号化したまま計算とか，○○したまま計算って「ダイアグラムがコミュートなんですよ」な世界なわけだな．

うーん……　ADP速くしましたなのか？　そして python が強い世界なのよと．……同じインデント駆動のシンタックスな Haskell が売れる基盤はできている？

そして並列は先が読めてしまう内容なので面白くなく……　発表時間が短いから突っ込んだ話もできず表面だけだど当たり前だよねになってるきがする．まあ，並列型の会議ではないし．

閑話休題．

停電明けのサーバ達が普通に動いてくれてて素晴らしい．ついでだからとアップデートをかけたら機能がうまく働かなくなったりもしたが……　時間がたったら直った．正常になってくれるのは良いのだけど原因不明なのはよろしくない．

そして新しいメールホスティングのシステムにはかゆいところに手が届く機能がついていることを発見．とりあえずテキトウに利用してみることにした．

文脈に依存しない参照透明なプログラムって扱いやすくてうれしいんだけど，参照透明な人間がいたとしたら意図が通じなくて残念だよね．

寒いコペンハーゲンにおいて会場が屋外より寒くて震えが……　泊まっているホテルは汗を書くほどに暑いのだけど，空調の入れ具合の感覚がよくわからない．

んで，気づいてなかったけど１件２０分発表とかいうスケジュールなのね．質疑も入れるとだいぶ短い気がするのだけど，最近の傾向なのでしかたがないのか．マルチトラックになるよかマシではあるけれど，論文採択しすぎじゃね？　そもそも今年は投稿件数少なかったんじゃ……　査読プロセスというか採録決定プロセスに新しい試みを入れたことの是非もよくわからんな．

SAT とか SMT とか直接使うと面倒だからプログラムの上で変数に存在量化子を付ける程度で言語システムがソルバを適宜ぶん回して結果を変数に入れてくれるとかいう仕組みは便利よね．というか，これらのソルバを存在量化子をプログラミング言語に入れることで簡単に利用できるようにしましょうというアイデアが頭いいなぁと思った今日この頃．

make だとうまく扱えない動的な依存関係（ソースコードを動的に生成するとかして依存関係が動的にできる）を簡単に使えるビルドシステム shake とかかっこいい．その他にも色々とプログラム開発の上で欲しい機能がついていると．うーん……　すごくいいツールだと思うんだが，言語が Haskell ってのが普及を妨げるような？　色々と高速化を頑張っていて，コンパイルとリンクって集中的に使う機能が CPU と I/O とに分かれているからインターリーブしてやって方が並列性が上がるよねとかは特に印象に残った．make が出来た頃とはけっこう計算機事情が異なってきているので，新しい効率的な「定番の」ビルドシステムってのも欲しいよね．つか，make って34歳とかなのか．

First International Workshop on Cross-model Language Design and Implementation とかいう初回なので良く分からないワークショップに invited talks 目当てで突っ込んでみた．

とりあえず DBPL とかの流れなのか．データベースというか巨大データというかに言語的な？　混沌としそうな勢い．

Invited talks は両方とも面白くこれらだけでも十分元がとれた気がする．半環だよねと文殊の知恵だよねと．

閑話休題．

身近にお財布盗まれた事件発生でコペンハーゲンもコエェなぁと思う今日この頃（空港の駅だったらしいけど）．数人の連携に狙われたらアウトだよねぇ……　とりあえず，お金持ってないように装っておけば狙われずにすむか？

閑話休題．

今日は日曜日だったのか．ホテルの朝飯の時間を間違えた．そしてスーパーに行ったら閉まってた罠．

閑話休題．

ホテルの部屋がコンパクトすぎて毎日どこかしらの出っ張りに頭をぶつけている．もうちょっと突飛な突起のない部屋の構造にならんものか？

３大がっかりのひとつらしいのだけど，何にがっかりすればいいのか分からないことにがっかりするくらい？　大事にされているのでとても綺麗だなぁという印象．そして足は結構普通の足なのね．

ぶっちゃけ観光客が多すぎることが一番残念？　バスが引っ切り無しにやって来てたし．観光客で賑わっていなければ人魚姫のがっかり具合が理解できたのかもしれない．

そして中国語の新聞を買えと声をかけられる罠．読めません．

閑話休題．

その他，よくわからないけれど近くにあった像たち．

中央駅付近のホテルから人魚像をちょっと過ぎたあたりまで行って返ってきて１０キロ程度の散策．スーパーも沢山発見．水２Lで8DKK（容器代3DKK含み）なので16円/DKKでも128円だからそんなに高くない（容器回収に出せば80円だし）．そして細いにんじんがひと袋250g（１２本くらい）入りで２袋15DKKとかでおやつにちょうどいい．

成田からミュンヘン経由でコペンハーゲンへ飛ぶというルートのミュンヘン→コペンハーゲンがストライキ中のルフトハンザ便だったけど，幸いなことに，結局その便はキャンセルされなかったので無事にコペンハーゲンに着けた．

とりあえず沢山キャンセルの図．

ストライキのせいなのかどうかしらんけど，とりあえずミュンヘン空港は乗り換えがとてもスムーズだった．入国審査も保安検査場もほとんど行列で待たずに通過できた．

閑話休題．

ミュンヘンのゲートでコーヒーとかホットチョコとか無料でサービスされとるのに気づいた．ルフトハンザはサービスいいと思うんだけど，ストライキが起きるとか従業員の待遇はよろしくないのかね？　

閑話休題．

海外ローミングで高い金払ってパケット通信しているときに受信する迷惑メールほどむかつくものはない．とくに基地外から送られてくる意味不明な迷惑なメールが25通とかみるとパケット代の請求を本気で考えようかと思う．

閑話休題．

デンマークのリーズナブルなホテルを確保しておいたのだけど，その部屋のコンパクトさに感動した．２段ベッドになっているのに横幅が１mない．寝相の悪い人は絶対に落ちるレベル．面白い．

定期健康診断の期間がちょうど長期の出張と重なっているので今日の午前に別キャンパスに行って受診するしか無いという罠．いつもとちらほら勝手が違ったのだけど，開始時刻前の待ち行列に番号札を配ってロビーで座って待てる状況を作るという点はいつものところも見習って欲しいなぁと思った．いつも３階までの階段を登って立って待つ行列とかになってるから……

さて，色々と計画の詳細を詰めねば．

櫻室町のリキュール．生姜と唐辛子でどちらも飲んだ後に体が熱い．そして唐辛子梅酒はほんとうに辛い．

これ飲んで寝れば風邪とか治りそうな勢い．

パスポートと日本の運転免許と2400円（発行手数料）と700円（写真用）を持って神田の免許更新センターへ行ったら１５分もかからずに作れた．とりあえず二輪と普通の四輪に乗れるらしい．

軽井沢から練馬までは順調に帰ってこれたが，そこから赤羽まで30分もかかったうえにまた土砂降りをくらいジーパンとジャケットが浸水．あと10分早ければ土砂降りを回避できたろうに……　渋滞が悪い．

閑話休題．

雨のせいか東京も暑くないっぽい．

Irith Pomeranz と Sudhakar M. Reddy の共著論文数が 409 であることを発見．Densest subgraph の近似アルゴリズムの実装のテストに DBLP のデータベースを使ってみたら（著者を頂点に共著関係を辺にした），この二人だけからなる subgraph がもっとも dense (エッジ本数/頂点数が最大) が結果として得られたので知ったという事実．とりあえず，驚きの共著数．他にも，互いに共著論文数が３０～６０本とかいう６人組とかも見つかった．

そして Irith Pomeranz 自身は毎月２本というペースで論文を生成している．これも驚きの論文執筆数．

そしたらバケツをひっくり返したような土砂降りをくらって下着までずぶ濡れ．草津の道の駅で土産を買い，さて大津へ下るかと R292 を進み始めて数分もしないうちにやられた．道路に小さな川ができる勢いの大雨の中カーブだらけの坂道を単車で下るとか神経使いまくりで疲れた．ついでに１８度とかいう気温の中を濡れたメッシュジャケットで走り抜けるってのも冷えすぎて体力的にきつかった……