[Paper, ICFP09] ICFP09 papers: review4

by syoyo

[Paper, ICFP09] ICFP09 papers: review3
の続きです.

Biorthogonality, Step-Indexing and Compiler Correctness

再帰のある単純型付き関数言語(simply typed functional language)と、SECD マシン の派生としての低レベルプログラムの操作挙動(operational behavior)との論理的な関連を定義します.
双直交性(biorthogonality)と step-indexing を用いて定義される「関連」は、数学的で領域理論的(domain-theoretic)な関数を実装するための低レベルコードの一部とは何を意味するのかを捉え、また単純なコンパイラの正しさを証明するために使われます. 成果は Coq 証明支援により形式化されています.

コメント: んー、抽象的でよくわかりませんが、コンパイラの検証にも使える手法なのかな.

Causal Commutative Arrows and Their Optimization

アロー(Arrow)は抽象計算(abstract computation)の一般的な形式です.
モナド(monad)よりも汎用的で、より広く応用が効き、特に抽象信号処理やデータフロー計算をうまく抽象化します.
最も特筆すべきものとして、アローは Yampa とよばれるドメイン固有言語の基礎を構成しています. Yampa はいろいろな具体的なアプリケーション、アニメーション、ロボティクス、サウンド合成、制御システム、グラフィカルユーザインターフェイスに使われています.

我々の主要な興味は、Yampa により表現される抽象計算のクラスのをよりよく理解することです.
しかしながら、アローはこれを精度よく行うには十分に具体的ではありません.
この状況を改善するために、平行計算(concurrent computations)の非干渉な性質の一種を表現する、可換アロー(commutative arrows)という概念を導入します.
また、 init 操作を追加し、そしてアロー効果のカジュアルな性質を表現するきわめて重要な法則を確認します.
我々は本提案により導出される計算モデルをカジュアル可換アロー(casual commutative arrows)と呼ぶことにします.

この計算のクラスをより詳しく調べるために、我々はカジュアル可換アロー(casual commutative arrows, CCA)と呼ばれる単純型付きラムダ計算の拡張を定義し、その性質を調べます.
我々の主要な寄与は、カジュアル可換標準形(casual commutative normal form, CCNF)とよばれる CCA の標準形の検証です.
terminating normalization procedure を定義することにより、アローの既存の実装に対してパフォーマンスの劇的な改善となる最適化戦略を発案しました.
このテクニックは Haskell で実装してあり、我々のアプローチの効果を検証するベンチマークを実施しました.
ストリーム融合(stream fusion)と組み合わせたとき、全体的な手法は 100 倍以上のスピードアップを実現します.

コメント: 信号処理をうまく(関数型言語で)抽象化するそうなので、シェーディング言語とかに使えそう. しかもそれを高速に処理できるらしい. まずはアロー、 Yampa を調べることからですね.

… のこり 24 papers ほどです.

Advertisements