22:27 10/10/06
ICFP 2010
International Conference on Functional Programming に行ってきました。 Haskell や OCaml や Scheme や Erlang 等々「関数型プログラミング言語」の研究の国際会議です。 延々と twitter で実況つぶやきしてたのを ICFP 2010 実況など にまとめましたので、どんな発表があったのか興味のある方は、そちらをどうぞ。
自分にとって特に面白かった！というベスト３は、この三つかなあ。
- VeriML: typed computation of logical terms inside a language with effects
-
「証明を書けるプログラミング言語」は素晴らしいのですけども、
そんなに大変でないように思える証明でも、書くと、想像以上に長くなってしまう傾向があります。
あなぷるやってるとよく感じます。
polymorphismやモジュールや高階関数などなど、
今時の「プログラミング言語」の持ってる抽象化機構は一通り備えた「言語」で書いているにも関わらず、長い。
なぜだろうか。
…という問題への挑戦。 結論としては、証明記述言語をさらに洗練させる、という方向には行かない。 この業界で"tactic"と呼ばれる、REPLで対話的に書く証明を探してくるコマンド、 これを実装する環境を強化するべきだ、という方向を提案する。 Coqで言うと「Gallinaはいい、とにかくLtacがショボいのを何とかすべきだ」。 というわけで VeriML というtactic記述言語を提案。 実はこの言語自体はまだ全然チェックしてないんですけど、この方向に対する提言は、 私にはかなり目から鱗でした＆説得されました。 - Type Inference in Context
- 型推論のアルゴリズムの、綺麗な整頓。 これまで型推論できなかったものができるようになったとかではなく、 「型推論とはそもそも何をやってるのか」ちょっと考え直してみた、というもの。 わかりやすかったです。この方針に忠実な実装を一度やっておきたいな。
- What Tic-Tac-Toe, the Tychonoff Theorem, and the Double-Negation Shift have in common
-
平均値の定理：∫f = f(c)："区間全体の平均値と同じ値を瞬間的に取る特定の一点が必ず存在する"
や、
最大値・最小値の定理："区間全体の最大値/最小値を取る特定の一点が必ず存在する"
や、
Drinker Paradox：日本語で上手く書けないのだけど、
"酒場には常に必ず、(その人が呑んでる⇒酒場の全員が呑んでる) が成り立つような特定の一人が存在する"。
というように、ある範囲全体について語る「平均、最大、全員」といった概念に対して、 なぜか、それと対になる特定の一点が必ずどこかに存在せざるを得ない、という現象がしばしば発生します。 これ、プログラミングにも活用できるぜ、というお話。 「全体」という扱いにくいものへの言及を一度特定の「個体」に移し直して、 そこでなんかの演算を加えてから元に戻ると、なにか「全体」に対する演算になっている、的な。 位相の言葉で数学的に説明しなおしてみたり、「○×ゲームの最適プレイ手順を求める」という Haskell プログラムをこれで書いたりしてました。 計算効率はすごく悪そうなので、少なくとも現時点では遊びに近いですけど、こういう考え方があるんだなあ、 という展開が面白かったです。
基本的に、こう、「その発想はなかった」という、 明日から自分のものの見方が変わるなーと思ったものをピックアップしています。 コンピュータ科学の研究史的に重要なコーナーストーンになりそうとか、今ホットな話題が、とかは全然よくわからないもので…。
VLDB 2010
さらにそのちょっと前に International Conference on Very Large Data Bases というのに行ってました。
シンガポール。F1レースの直前だったそうで、観客席などが作られてました。 nishioさんに教えてもらった チキンライス が美味しかったです。
リンク先の "Proceedings and presentations are available for download:" 以下から、 オフィシャルに全論文が公開されてます。マイ面白かったベスト３は：
- Avalanche-Safe LINQ Compilation
- LINQ のクエリ式を SQL にコンパイルするときに、できるだけまとまった SQL にして飛ばす、などなどエンジン。 間違っても、途中式で返ってきたrowの数に比例する回数SQLを飛ばしたりするような事態が起きないようにする。 これって実装ダウンロードできるのかな？
- Hadoop++: Making a Yellow Elephant Run Like a Cheetah (Without It Even Noticing)
- このチームの人達全員おそろいの Hadoop++ Tシャツ着て、気合い入ってました。 名前の通り Hadoop をハックして象をチーターに！ Hadoop本体の実装には一切手を加えずに、フックメソッドを上手く使うことで、 検索インデックスやなんやかんや従来DBの技法をM-Rの過程に薄切りして混ぜ込んで忍び込んでいる。
- Destabilizers and independence of XML updates
- 内容としては、元DBに変更を加えたときに別に作ってあるビューをupdateする必要があるかどうか判定、 といったものなんですけど、これは、実装テクニックに感心。 「判定問題を見たらSMTソルバに渡せる形に変換して頑張る」というのも定番中の定番ですし 「木構造をRDBで高速に扱うのに、木構造を数値の区間にエンコード」というのも定番中の定番ですけど、 合わせ技で「この区間エンコードを方式を使えば既に木の話が自然数の話に落ちてるから簡単にSMTに持ってけるじゃん！」 という発想をしたことがなかった。なるほど。
あとは、 趣味アルゴリズマー的には、 色んな形のインデックス作る話はどれも聞いてて楽しいですね。 "Shortest Path Computation on Air Indexes" （最短路計算しやすいような形で、 グラフのデータを繰り返し電波放送するのに適した表現はどんなのか）や、 "Approximate Joins for XML Using g-String" (XSym) （ツリーとツリーの類似度計算を真剣にやるとコストデカいけど、 n-gram (のツリー版概念) を横に並べた文字列の類似度計算でだいたい何となく精度出るんじゃないの？？） 辺り。
