2011年01月

数年前に実験で使った紙テープといくつかの資料が見つからない．研究室を一通り探し滝になっているけど見つからない．

代わりと言ってはなんだけど，目的とは違う40年前の大量の紙テープが発掘された．テープに書かれているメモを見ると何やら成績のデータか何からしきものもあったが…　現在のところテープリーダがないので何とも．一定のテンションをかけてテープを巻き取れる機械さえあれば穴の読み込み自体はwebカメラで十分できるのだけど．

当時の実験担当者が数日後に来るのでその時にまた探す．

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

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

とりあえず 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円とかで売ってるし．

今日は主にツールと並列と．

最初の Particle systems 記述用のライブラリ in SML3d を作ったぜという話は…　使えそうだけど実際問題としてどの程度実用なのかよくわからず．とりあえず particle-particle interaction はまだできないらしい．世の中でパーティクル間の相互作用ってどれくらい必要になっているのか知らんけど，それを GPU でどうやってうまくやるんだろうとかいう興味はある．それはさておき，3Dグラフィックスには宣言的なアプローチが必要だというのは大いに納得．命令的に3Dやるのは面倒すぎて過去何度やる気が無くなったことか．まあ，パフォーマンスが気になるところではあるけれど．次の Xpath クエリを functional logic な言語 TOY に実装したぜ(XPath = non-deterministic higher-order expression で)の話は…　forward-axes の実装は普通なのでさておき，reverse-axes の filter への変換が高階マッチングでダイナミックにできてしまうという点に感動した．ついでに XPath のデバッグに現在の XPath にマッチするインスタンスを生成させりゃいいとかいう考え方も論理型言語ならではだなぁと感心．Curry でも勉強しようかね．そんで3つ目の話は strictness を排除してメモリ効率を上げましょうという話で…　strict にして効率を上げようという普通の考え方と逆を行く結果で興味深い．不必要に評価しなければメモリを無駄に消費しないで済むよねと言われれば確かにその通りな気もするけれど，最適な strict 具合を見極めるのも大変そうだなぁ．

で，午後１は並列．とりあえず F♯ に async 入れたよ（というか，既存言語に容易に機能追加する方法論？）という話で…　英語が速すぎて…　実際のところ数年前にテクレポか何かで出ていた話をちゃんと学会で話しましたよという宣伝でしかなかったような．んで，その次は HPC のために通信を明示的に書きましょう，でも宣言的に，という話．ぶっちゃけ何処が宣言的なのかとかいう疑問というかただのマクロの展開じゃんというツッコミが Launchbury から飛んでいたのだけど…　代数規則とかは無いんかいという．ぶっちゃけ使い物になるのかどうかわからない．そして3つ目でまたF＃に戻って，こんどは reactive programming 用の拡張を入れたよと．まあ自然．Manticore の pcase と同じ．

どうでもいいけど並列系の人間はしゃべる時間も勿体ないくらいにせっかちなのかね？　3件中2件が喋るの速かった．特に2件目とか無駄に時間が余ってたんだけど…

以下略．

朝一でレジストレーションしてPADL'11で話を聞く．

初っ端の招待公演は Core i7 の formal verification の話．どうやら Pentium Pro のころから FV をやっていたらしい．仕様とか検証器とかをlazyなMLで書いてるとかいう話で，まあ手続型言語で仕様書くとか検証に関する無駄な計算を省かせるとかはしたくないから遅延評価な関数型言語でやるのは筋が良いねという．質問でロジック言語でいいんじゃねーのとか出てたけど，そこらへんは歴史的事情と現場的事情があるのでしょう．

次いで，メッセージパッシングとかネットワークの話．Erlang で，お前にはメッセージが絶対来ないよとか，お前のメッセージは絶対に受け取ってもらえないよとか，そういうメッセージのやり取りの不備を静的に解析する話．大半の発表スライドが「スライド一枚に説明したいことを連想する画像一枚」とかいう構成だったのが印象的．しゃべっていた内容は納得．パイ計算などとの関連や，セッションタイプとかとの関係があるのかないのか良くわからなかった．その次はチャネルを使ったプロセス通信なプログラムを簡単に書くコンビネータライブラリの話で，type class 使いまくると綺麗に書けるとという話．とりあえず type class を使ったプログラムは細かいことを考えなければ読みやすいのだけど，細かいことを考え出すと「この部分式の型はこれだからこのインスタンスの関数が実行されて…」とか追わなければならないので理解が大変な気がしなくもない．最後のはProbLog (Probabilistic extension of Prolog) でモバイルアドホックネットワークのプロトコルの解析を解析的にやるとか．新に解析的なのかどうかはさておき，ProbLogはプログラムに対して何かの確率をうまく計算してくれるらしい．シミュレーションとは違うのだよシミュレーションとは，と言っていたけれど，ProbLogでやってることって確率モデル（プログラム）のシミュレーションなんじゃないかなぁとか思ってみたり．まあ，よくわからん．

以下略．

オースティン到着．空港から街中までのバスが1ドルとか素晴らしすぎる．街中のバス全部が1回乗車1ドルで，一日パスでも2ドルとか．東京のバスも半額になってほしいなぁ．

さて，今日はもうレジストレーションに行ってもしょうがないので明日の朝に行くことにする．さっさと寝ないと風邪ひきそう．

だから目的地は寒くなくてもシカゴは寒いんだって！　飛行機が雪を巻き上げながら突き進んでいくし！　前回も同じようなことを思いつつ，完全に忘れてた．学習しない．

そして入国審査は例のごとく1時間かかった．こちらは学習したので乗継までの時間に余裕を持っておいた．とはいえ4時間は開けすぎだったかもしれない．

閑話休題．

PSPのUSB充電はいつでも出来るわけじゃないのね…　

明日からのお出かけの準備．まあ，いつも持ち歩いているセットに着替え付け足すだけだけど．

ああ，パスポートを忘れてはいかん．

そして飛行機で暇なので長めの論文を印刷して持っていこう．ついでに死者の宮殿の攻略情報を印刷して持ってくか．

修論生がTeXを全く使えなくて驚くばかり．過去二回の学科輪講の資料をどうやって作っていたのだろうとかいう疑問も湧いてくるのだけど…　Wordで処理してたのかね．Wordだと参照の処理とか面倒そうだし，表記法をマクロで抽象化しておいてあとで気に入らなくなったら一斉に修正とかいう技も使えなさそうだし，論文書くのにWordって使いやすいのかね？　よくわからん．科研の申請でさえ参照とか面倒だからTeXで用意してからWordに貼りつけだし．

とりあえず参照番号直打ちだけは最終的に無くさせたい所存．番号振るのはTeXのお仕事だし．"mathematical" とか入っている専攻出身でTeX使えないとかありえないし．

アンケートの集計やイベントへの参加登録等のための回答入力ページが簡単に作れつつ，入力されたデータが勝手にスプレッドシートに記録されてくれるとか便利すぎる．

でだ，大体の使い方は分かったのだけど，スプレッドシートの列の入れ替えの仕方が分からないという状況．フォームにアイテムを追加した順で列が並んでいるのだけど，フォームの上でアイテムを移動してもスプレッドシートの列が移動してくれないっぽい．別に列の順番なんか集計上は全然問題ないのだけど，何となく気持ち悪い．

もう少し Google Docs のお勉強をしなければならない様だ．

２つのテキストファイルに書かれたレコード達を指定したフィールドで（いわゆる RDB の）join するコマンドが欲しい．

まあ，そのものなコマンド join が unix にはあったりするのだけれど，もう少し柔軟性が欲しいなぁと．例えば join はキーとするフィールドが二つのファイルで同じ順序にソートされてなければならない．けれど，しばしばキーでソートし直すとかしたくない時がある．まあ，前処理で行番号を新たなフィールドとして追加した上でキーでソートして，join が終わったら行番号でソートし直すとかすりゃ元の順番壊さずに済むのだけど．ちょっと手間．

なーんてこと思ったり思わなかったりで，結局いつも while read line; do ... sed -i -e ...; done とかやって総当りで書き換えしまくるのだけど，なんかもう少しスマートにやりたいなぁと．

先々週末くらいから調子悪かったのをようやく業者に連絡して修理してもらった．なにやらトナーカートリッジと本体との間のトナー輸送路にズレが生じで詰まってたのが原因らしかった．トナーが詰まって輸送できないのに頑張ってトナーを送ろうとしてギアが飛んでたみたい．

とりあえず輪講用の大量印刷前に修理が終わって良かった．

先週，研究室の電話が通じなくなった．電話がないと色々不便だということで，先週のうちに修理の依頼を出し，先週のうちに修理の業者が研究室に来た．が，私は不在だったので，業者がまた月曜に来ると学生に伝言を残して去っていった．

で，今日の夕方に業者が来た．とりあえず私が状況説明を始めたてみたのだけど，このとき確認したら電話が普通に使えた．修理を呼んだ時に限って問題の現象が起きないとかいう最悪のケースか！とか思って，私は必死になって問題の現象（断線）を説明．

が，私が一通説明したあとに，業者の人曰く「先週直したんですよ、それ…」　じゃあ，何のためにあんた来たの？　修理のためではなくて直ったことの確認のためってこと？　んなことワシなんも聞いとらんのだけど．

なんだろう，先に一言「直ったことの確認に来ました」と言ってくれればいいのに．伝言残した人も今日来た人も最初に何も言ってくれないんだもの．効率悪すぎ．情報の伝達の確認をちゃんとしろよ．新居の不動産屋といい，今回の電話修理といい，そこら辺をお座なりにしている連中に最近しばしば遭遇する気がする．

そういや補助錠の取付に鍵屋が昨日やっときた．鍵屋自体は対応が速いはずなので，不動産屋の動きが鈍かったと思っておこう．そして錠が３つも付いてるドアってのも異様な雰囲気を醸し出すなぁ…

海から昇る日の出が見たいなぁと思って九十九里浜の九十九里ビーチタワーへ行ってみたのだけど，残念ながら海の上に雲があって日の出が見られなかった．

さらに悪いことに，突然ものすごく雪が降ってきた．出かける前にチェックした天気予報で晴れだったのに…　前も良く見えないし体に積もるし滑りそうだし．雪が降りそうなくらいに寒い時にはバイク乗らないのが正解なのかもしれない．

先週に引き続きまたもや死ぬほど寒かった．家についてもまだ若干の雪がジャケットに残ってたし．早く暖かくならないかな…

東西の方向からみると太く見える気がするのだけどどうなのだろうか？

宝永山が真ん中に来る裾野からの見え方に慣れてるせいか，山中湖辺りから見ると太った感じに見えて違和感がある．ただ単に富士山に近い地点から眺めるからなのだろうか？

Skype にグループビデオ通話機能が付いてたのね，去年の中頃から．誰か一人でもSkype Premium (1000円弱／月) を購入していれば使えると．

Polycom も微妙に不安定になってきたので Skype 使うってのもありだなぁ，と思った今日この頃．

でもグループビデオに対応したSkype5.0はLinuxにない気がする…　まあ，VMware + Windows 7 とかを用意してその中で使えば問題ないか．

論文の締切り．31ページのテクレポを15ページに縮めたのをさらに圧縮して10ページ．なんのこっちゃ．

テクレポ発行の締切り．最後の修正と印刷と冊子作りと配布と…　奇しくも2年連続で第01号が31ページとかいうオチ．

ワークショプでの発表．内容が多すぎて予定通り後半はスキップ．というか，予定になかったことをしゃべろうとして英文が出てこないとかで微妙に伸びるよね．そして最後の片付け担当．

あー，ねみぃ．

つまり，ディスカッションするかどうかすら自由であると．

とりあえず論文始末しないと．

それにしてもタクシー高いなぁ．荷物が多いときには便利なのだけど．

明後日締切りの会議に論文投げてみようかとか突然思い立った．スペース足りないのが難点なのだけどバッサリ切ってやれば何とかなりそうな気はする．とりあえずイントロをさらにやさしく書き直す方向で．

近場の浅草で開催．デンマークから強力な連中がゾロゾロやってくるという．

そして今回ホテル側に用意してもらった（レンタル）プロジェクタも例に漏れず光束が少なすぎて暗いのなんの．なにやらより強力なプロジェクタも無いことはないらしいが数日間のレンタル料で新品が買えてしまうお値段．しょうがないので強力なプロジェクタを取りに大学まで往復した．近場でよかった．

今度のPPLは北海道なので，電車じゃ疲れるから飛行機で行く．とりあえずスーパー旅割で予算消費を抑えようと思い年末にさっさと航空券を買おうとしたら，実は２ヶ月前にならないと購入できないオチが待っていた．予約は出来るのだけど．

ということで，２ヶ月前になったのでさっさと購入．忘れた頃にやってくる３日間で支払いをしなければいけないとか微妙に危険度高いなぁ．

日の出前にバイクで南房総に出かけたら痛かった．主に指的な意味で．

まあ，高速走ったら寒すぎるのは分かっていたのだけど，正直南房総の一般道を舐めすぎていた．微妙に高度が上がって寒くなる上に信号にも引っかからないので走り続けて冷える一方．途中でかなりやばい感じに手が痛くなってきたので一般道なのに自販機で一休憩とか．やっぱ冬場はバイクだと色々きつい．

エンジンの熱をフレキシブルなヒートパイプで手元に持ってくるとかできるとありがたいかも？

閑話休題．

水仙ロードを目的に出かけたのだけど，途中でハイキングコース（コンクリート舗装な山道）にバイクで迷い込んだ．日の出前に．山超えたら確かに水仙ロードに出られたのだけど，ぶっちゃけもう少し気の利いた案内が欲しかった気がする…

でもまあ，山の上できれいな日の出が見られたので良しとしよう．ぶっちゃけ寒すぎて気の利いたものが撮れてないのだけど．

さて，来週辺りには宝登山のロウバイが見頃になるかね？

プリンターが文句を吐くだけでまともに反応しくれない．

電話線が断線して電話が通じない．

新年早々面倒事が多いなぁ．とりあえず来週はイベントがあるので正常に戻るのは再来週かなぁ．

ギリギリ予想範囲内ではあるけれど色々と準備期間が短くなるなぁ…　あーめんどい．

よくよく考えるとただの数学の論文な気がしてきたぞ…　関数型言語のプログラムなんて数式でしかない．誰が読むんだこれ？

これまでは研究室が近かったので家にプリンタなくても不自由しなかったのだけど，片道３０分になると時間効率が悪いので家にプリンタが欲しくなってきた．

Linuxから面倒なく使える両面印刷ユニット付きのモノクロレーザープリンタっていくらぐらいだろう？　brother のプリンタならLinuxでも設定楽だから２万円強くらいかね．

雑煮用と謳って大量に安く売っていた．きっとクリスマスで消費しきれなかったヤツらに違いない．調度良いのでネギシチューの具になった．

東京に戻ってきた．在来線使用．高速の渋滞情報とか見てるとバイクで帰らなくて正解だった気がする．

サイズが・・・

ところでお餅にみかん乗せるのってなんでだろう？

初詣に三嶋大社行って，そこから初日の出などを拝みに富士山一周．大社は朝４時とかが空いてて楽．

初日の出直前の富士山．日の出は逆方向だけど．

山中湖での富士山と日の出．ぶっちゃけ日の出と富士山が同時に見えるのは富士宮のほうなので思いっきり微妙な位置で日の出を見た気もしなくない．

ということで，富士山と日の出を同じ画に収めるべく忍野八海．朝早かったのに意外と多めの人とすれ違った．

そして道端には雪．向こうのお山にも雪．バイクではあまり積極的に来たくはない．