融合変換による最適化の
理論的基盤と正当性
酒井政裕
慶應義塾大学大学院
政策・メディア研究科修士課程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] の利用?
途中の過程では弱い等号を用いる
最終的には条件付の等式に
目的
正当性を理論的に保障
融合変換をより安全に広い範囲で使用可能に
安全で強力な最適化技術の実現
信頼性と性能の両立を
また、その過程で融合変換についてよりよく理
解したい
それによって、より高度な融合変換を
詳しくは目下研究中
まとめ
プログラム変換の一つとしての融合変換
融合変換の簡単な例と理論
私のアプローチ
© Copyright 2024 ExpyDoc
