融合変換による最適化の
理論的基盤と正当性
酒井政裕
慶應義塾大学大学院
政策・メディア研究科修士課程2年
自己紹介
 2001年 慶應義塾大学総合政策学部入学
 2005年 同卒業
 2005年慶應義塾大学大学院 政策・メディア
研究科 入学、現在在学中
 萩野達也研究室所属
自己紹介: 活動
 Haskell
 Lightweight Language Weekend 2004
 Lightweight Language Day and Night
2005
 日経ソフトウェア6月号「Haskellによる関数プロ
グラミング入門」
 Ruby-GNOME2
研究的興味
関数型言語の最適化
プログラム変換、特に融合変換の
理論的基盤とアルゴリズム
研究の背景
 ソフトウェアの不具合が社会問題化するケー
スが増加
 ソフトウェアが必要とされる領域の広がり
 ソフトウェアの高機能化・多機能化にともなう
複雑化
 ソフトウェアの信頼性が重要に
 様々なレベルの方法が必要
 工学的な品質管理, etc
 分かり易い自明なコードも重要
研究の背景 (2)
 分かり易い自明なコードは重要
 しかし性能のよいコードは複雑で分かり難い
 信頼性と効率の両立は難しい
研究の目的
 高度な最適化技術の実現
 強力な最適化
 しっかりとした理論的な基盤
 信頼性を損なわない
 信頼性と効率の両立
位置づけ
応用
信頼性の高いソフトウェア
高性能なソフトウェア
プログラム変換
ソフトウェア検証
プログラム意味論
コンピュータサイエンス
基礎
数理論理学
位置づけ
信頼性の高いソフトウェア
高性能なソフトウェア
応用
融合変換
等
プログラム変換
ソフトウェア検証
プログラム意味論
コンピュータサイエンス
領域理論
型理論
各種意味論
基礎
ロジック
圏論
離散数学
数理論理学
形式的証明
モデル検査
テスト等
最適化
 概念を素直に表現した単純なプログラム
 分かりやすい
 モジュラリティーが高く、扱いやすい
 しかし、性能が悪いことがしばしば
 最適化が必要
 コンパイラによる最適化
 ハンドチューニング
ハンドチューニングの問題
 その過程でバグが混入する可能性
 結果のプログラムは
 複雑で保守が困難
 モジュラリティーが低く再利用が困難
 信頼性を損なう
 最適化のための別アプローチが必要!
プログラム変換
 数学的(代数的)な性質を用いる最適化
 例)
a×3 + a×2
= { 分配則 }
a×(3+2)
= { calculation }
a×5
 同じ意味で性能のよいプログラムへ変換
 オーダが変わるような場合も
融合変換
 プログラム変換の一種
 複数のパスからなるプログラム
 わかりやすいが
 中間データが存在し、効率が悪い
 これを単一のパスに変換
融合変換の例
 add(vector A, vector B) {
vector tmp;
for (int i = 0; i < A.size; i++)
tmp[i] = A[i] + B[i];
return tmp;
}
 add(add(A,B), C);
 二回ループを回す必要
融合変換の例
 add3(vector A, vector B, vector C) {
vector tmp;
for (int i = 0; i < A.size; i++)
tmp[i] = A[i] + B[i] + C[i];
return tmp;
}
 add3(A,B,C);
効率向上
 一回のループですむ
融合変換 (2)
 中間データ構造を生成しないことによる、空間
効率の向上
 これまで離れていたコードが接することにより、
更なる最適化が適用可能に
 主に関数型言語で用いられる
関数型言語
 数学的な関数に基づいた言語
 (原則的に)副作用がない
 等しい式は自由に置き換えが可能
 数学的な取り扱いが容易
 例: Haskell, ML, Lisp
なぜ関数型言語か?
 数学的に厳密な議論をしたい
 現状の一般的な命令型言語では難しい
 代数的性質が簡単に利用できる
 命令型言語では特別な解析が必要
 そこで、とりあえず関数型言語に特化
融合変換の理論
 圏論
 データ型と帰納的定義
 一意性による等式の導出
 融合変換の難しさ
圏論
 対象と射(矢印)による抽象化
 プログラムを扱うのに便利な概念を提供
対象 射
 等式を図式で表現
集合
関数
位相
空間
群
連続関数
型
プログラム
準同型
データ型と帰納的定義: 自然数を例に
 以下のような再帰的定
義で関数 h: N->X が
一意に決まる
 h(0) = f
 h(s(n)) = g(h(n))
 圏論での書き方
 h∘0 = f
 h∘s = g∘h
 この h を fold(f,g)
と表す。
 一意に決まることが N
の本質
帰納的定義の例
 2倍する関数
double : N -> N
double(0)
=0
double(s(n)) = s(s(double(n))
 fold で表現
double = fold(0, s∘s)
double ∘ double の融合
 doubleは以下を満たす
double ∘ 0 = 0
double ∘ s ∘ s
= s∘s∘s∘s ∘ double
 よって
double∘double ∘ 0 = 0
double∘double ∘ s
= s∘s∘s∘s∘double∘double
double ∘ double の融合
 double∘double ∘ 0 = 0
double∘double ∘ s
= s∘s∘s∘s∘double∘double
 fold(0,s∘s∘s∘s) も
同じ等式を満たす
 一意性より
double ∘ double
= fold(0,s∘s∘s∘s)
double ∘ double の融合
 double∘double ∘ 0 = 0
double∘double ∘ s
= s∘s∘s∘s∘double.double
 融合できた!!
fold(0,s∘s∘s∘s) も
同じ等式を満たす
 一意性より
double ∘ double
= fold(0,s∘s∘s∘s)
融合変換の規則
 一般に h:X->Yが
h ∘ g = g’ ∘ h
h ∘ f = f’
を満たすならば
h ∘ fold(f,g)
= fold(f’,g’)
融合の難しさ
 h ∘ fold(f,g) = fold(f’,g’)
 f’, g’ をどう発見するか?
 関数は fold(f,g) の形をしていないかも
 対策
 Shortcut 融合変換
 関数を融合しやすい形で定義しておく
 Warm Fusion
 一般の再帰的定義から fold/build を導出
融合変換の実装例
 Haskellの処理系GHC
 short-cut 融合変換
 10クイーンで43%, 大規模ベンチマークで平均
3%の実行時間改善
 尾上 能之 『融合変換による関数プログラム
の最適化』 [Onoue’99]
 再帰的定義からHylomorphismという形式を導
出し、Hylo-Cata fusion という規則によって融
合を行う
 GHCに実装したが取り込まれてはいない
尾上らの手法の問題
 Hylo-Cata のみを扱いその双対の HyloAna を扱っていない
 Hylomorphism と Free theorems を組み
合わせることの正当性の問題
正当性の問題
 Hylomorphism
 余帰納的な関数でデータを生成し、帰納的な関数でデータを
消費する関数
 帰納的データ型と余帰納的データ型の一致が必要
μX. F(X) = νX. F(X) … (A)
 Free Theorems
 型を関係として解釈することによって証明される
 パラメトリシティに基づく … (B)
 AとBは厳密には矛盾!!
なぜ矛盾するか
 ラムダ計算に基づく体系では以下が同値
 帰納的データ型と余帰納的データ型が一致
 すべての型Aに不動点コンビネータ
fixA: (A -> A) -> A が存在
 パラメトリシティより、直和 A+B を表現可能
∀C. (A->C) -> (B->C) -> C
 ラムダ計算(= Cartesian Closed Category)
では直和と不動点コンビネータは矛盾
 正確には退化したモデルしか存在しない
何が困るのか
 正当性は微妙なのは気持ち悪い
 本来成り立っていない等式に基づいた最適化
が行われてしまう可能性
 アドホックに正当性を保障することは可能だが、
一般的な保障が欲しい
私のアプローチ
 形式的な意味論を用いた正当化
 今考えているアイディア
 Moral equality [Danielsson’06] の利用?
 途中の過程では弱い等号を用いる
 最終的には条件付の等式に
目的




正当性を理論的に保障
融合変換をより安全に広い範囲で使用可能に
安全で強力な最適化技術の実現
信頼性と性能の両立を
 また、その過程で融合変換についてよりよく理
解したい
 それによって、より高度な融合変換を
詳しくは目下研究中
まとめ
 プログラム変換の一つとしての融合変換
 融合変換の簡単な例と理論
 私のアプローチ
ダウンロード

interview2 - 酒井 政裕 (SAKAI Masahiro)