No Such Blog or Diary

今回の旅程では４回飛行機に乗った．その内３回は隣の席が空いててエコノミーなのに快適モード．一番後ろ当たりは勝ちが多い．最初の飛行機がコードシェア便で席を撮り忘れていたのは痛かった…

さて，出張中に届いたマシンのセットアップも終わったし，そろそろ帰るか．

とりあえず Robin Milner 1時間．

次いでメドレーセッション．最初は GPU で 0CFA という面白話．preprint version の紹介を研究室輪講で聞いていたので，著者らの考えを確認するのが目的．とりあえず 0CFA 以外の計算に使えるという意識を持っているようで安心．とはいえ具体的に何に使えるかは述べてなかったが…　結局のところ集合上の不動点演算系は何でもできるんじゃないのとは思いつつも具体的なアプリケーションは思いつかない．とにもかくにも sparse matrix 万歳．ELL form 万歳．GPU上で効果的に実行できる面白い計算パタンを示したという点が最も価値ありと思う．次は quantum computation の bisimulation の話．ぶっちゃけ量子計算自体に誰もついて行ってない気がしたのだけど…　量子テレポーテーションのプログラムですらスライド見ただけでは時間が短すぎてわからず．幸いなことに Wikipedia にある quantum teleportation の説明を見てプログラムだけは理解できたのだけど，それ以外の部分はよくわからずのまま．まあ，量子計算自体がまだまだ新しいから道具の準備もまだまだなんだねという感想．そしてこのセッションの最後は DPJ (Deterministic Parallel Java) に入れた安全な non-determinism の話．DPJ は deterministic-by-default というコンセプトで，基本的に入力に対して出力が一意に決まる．でも効率悪いことがあるから明示的に non-deterministic な事してもいいよね，という話．このセッションは全くもっててんでバラバラな内容で面白かった．

以下略．

お昼はまた Whole Foods Market で．今日は詰め込み過ぎた…

午後１の Synthesis セッションの最初のが面白かった，というか便利なので欲しい．スプレッドシート上の文字列の変換操作を，いくつか例示してやるだけで他のは勝手にやってくれる（そういうプログラムを内部で合成している）．間違った部分もインタラクティブに修正してやると，同じような修正のかかりそうな部分をやっぱり勝手に直してくれる．これが Excel に標準で入っていれば…　世の中の事務処理が物凄く高速化されるんじゃなかろうか？　中身的には，入力文字列の部分列と定数文字列の組み合わせでできる文字列を出力するプログラムを合成する．部分列は開始インデックスと終了インデックスで表され，インデックスは２つの正規表現（インデックスから左にマッチする正規表現と右の正規表現）と何番目のマッチかの整数で表す．リーズナブルなプログラムを出すのに具体的にどうやっているのかは分からないけれど，なるべく小さくかつ定数文字列を少なくという方向でチューンされているらしい．今回のは syntactic な変換（部分文字列の再構成）のみだけど，semantic な変換（日付から曜日を出すとか，数を足すとか）もできる研究が進んでいるらしい．Excelとかを日々使うような人たちこそがプログラム合成を必要としている人々の大部分なわけで，その意味において非常に有用な結果だと思う．というか，コマンドライン上で生活する人間としては sed のプログラムを自動生成してほしい…　（過去何度か考えたけどあまりに面倒なので放棄され続けている…）

他略．

とりあえず，会場がダメすぎて困る．椅子しかない，ものすごく密集している，質問にマイクの位置まで出るのすら大変，そもそも人が邪魔でスクリーンの下半分が完全に見えない．ACMの会議の発表はあとでオンラインでビデオが見れるので，この会場だったらビデオで見るだけでも十分，というかビデオのほうがスクリーンをちゃんと見れる分より良いのではなかろうか？

んで，招待公演は certified compiler の話で…　確かに飛行機のプログラムにもコンパイラが関与していると思うと certified compiler がないと怖すぎて飛行機乗れないなぁと．とはいえ，飛行機の制御とかは floating point 使っているわけで，そいつの検証とか大変だよねと．常識的に考えて合っているだろう前提条件が floating point だと正しくないことが多々ある（結合性とか，同値判定とか）のでなんとも．いっそのこと制御機を綺麗な構造の体の上に構築すればいいんじゃねとか思ったりするのだけど，そういったものは理論的にもあるのだろうか？　それはさておき，肝心の検証器自体の検証をどうやるのかとか考え出すと非常に悩ましい気になるのだけど，そこらへんどうなっているのやら．何を信じていいのかわからない気もしなくはない．verified mix とかあれば verified compiler は verified interpreter から作れるんじゃね？

そしてテクニカルセッションは今年から2並列なので…　とりあえず Semi-Automated Verification へ．んで，concurrent C の certified compiler という CompCertTSO (TSO = Total Store Ordering) の話が最初．細かいことはわからんが，そもそも certified compiler は逐次でさえ面倒なので，concurrent 用の証明を簡単にするために言語のセマンティクスとメモリのセマンティクスを分けたとかなんとか．確かに，Sequentially Consistent でないことが起こる（最初 0 で初期化された x と y に対し，２つのスレッドが それぞれ mov x 1 と mov y 2 をし，そして其々が mov ax y と mox bx x とやると，ax も bx も 0 ってことがしばしばある．バッファのせいで．）って時点でどんだけ面倒なんだよと．計算機のセマンティクスは x86-TSO という去年あたりに発表されたもの．次いで，c++0xのconcurrentの検証で，実際いくつかの問題を見つけたりしたそうな．これも x86-TSO のセマンティクスを使っている．そしてC/C++言語の検証セッションの最後は，C++のオブジェクトレイアウトの検証．多重継承時のオブジェクトレイアウトのアルゴリズムとかのをちゃんと検証したと．確かにこれも面倒な話だね…　なんとなく実用的な言語の検証は力技で押し切れる体力がないと駄目だなぁという印象．

以下略．

ホテルに Wi-Fi があるかなと探してみたら（PCは有線接続できるがiPodは無線が必要なので），COA_MESH とかいう SSID のネットワークが無料で使えることを見つけた．調べてみると City of Austin - The City of Austin is deploying a Wireless Mesh Wi-Fi Network とかいうことで，オースティン市が提供しているらしい．

行政が屋外でも使えるワイヤレスネットワークを提供してくれるってのはいろいろと便利でいいなぁと．一応，最初にネットワークにつなげると「ブラウジングとメール以外に使わないでね」とかあるけれど，これらを使わせてもらえるだけでありがたい．市民税とかで強制的に使用料を取られると思うと微妙だけれど．

でもまあ，まだまだメッシュが限定的なので欲しいところで繋がらないという罠が待っていたりする．ちょうど泊まっているホテルはメッシュ内なので接続可能だが，会議の開かれているホテルはメッシュ外なので繋がらなかった．外を歩きながら google map 使おうと思ったら繋がらなかったとかも．

風邪引くのも嫌なのでスーパーマーケットで新鮮な食糧をゲット．ホテルから歩いて15分の Whole Foods Market というお店．なにやら Austin 発祥の巨大なチェーンでかつ有機栽培に拘った有名なお店らしい．日本語のウィキペディアにも載ってるっぽいし．

んで，総菜コーナーでサラダやらなんやらを好きなように容器に詰めてお持ち帰り．野菜のあまりないホテルの食事とかもう嫌だ．お値段も$7.99/1lbなので換算して100g145円程度とオリジン弁当よか安いし．惣菜以外にも色々とものすごく何でもあるので不健康な食事もいくらでも可能．普通に鳥の丸焼きが紙袋入りでドカドカおかれていたのはアメリカっぽいというかなんというか．

Bostonに行ったときには Trader Joe's にお世話になったけど，近くに大きなスーパーがあるって便利だなぁ．というか，海外行ったら現地のスーパーで現地の食糧を調達して食べるってのが半ばパターン化している気がする．お金の節約＆体へのダメージ減少というメリットは捨てがたい．今回の Whole Foods Market は若干お値段高めっぽいのでなんともだけど．

そういや Whole Foods Market の（エコ）バッグとか土産になるのかね？　Google の suggestions に出てくるし楽天で800円とかで売ってるし．