学位論文要旨



No 112232
著者(漢字) 胡,振江
著者(英字) Hu,Zhen-Jiang
著者(カナ) コ,シンコウ
標題(和) 構成的手法による関数プログラムの最適化
標題(洋) A Calculational Approach to Optimizing Functional Programs
報告番号 112232
報告番号 甲12232
学位授与日 1996.09.30
学位種別 課程博士
学位種類 博士(工学)
学位記番号 博工第3775号
研究科 工学系研究科
専攻 情報工学専攻
論文審査委員 主査: 東京大学 教授 武市,正人
 東京大学 教授 田中,英彦
 東京大学 教授 井上,博允
 東京大学 教授 杉原,厚吉
 東京大学 助教授 寺田,実
 東京大学 講師 松岡,聡
 東京大学 教授 萩谷,昌己
内容要旨

 中国では,「魚和熊掌不可同時兼得」という諺がよく知られている.これは二つの貴重品を同時に手に入れることはできないという意味である.関数プログラミングにも同じことが言える.関数プログラムの開発においては,機能は小さい多数の関数を部品として組み合わせて,全体として大きなプログラムに組み上げていくというプログラミングが行なわれる.ひとつひとつの小さい関数は極めて汎用性に富む有用な部品で,これらを組み合わせた全体はモジュラー性をもち簡潔であるが,そのままでは必ずしも実行効率のよいプログラムになるとは言えない.その大きな原因としては,

 ・部品となる関数間で多数の中間データ構造が受け渡されること

 ・同一のデータ構造中を各部品関数が別個に廻ることがあること

 の二つを挙げることができる.本論文では主としてこの二つの問題に焦点を当て,処理対象とする大きなプログラムを,計算結果には現れない中間データ構造を生成することなく,同一のデータ構造を重複して廻らないプログラムに前処理によって変換し,構成的アルゴリズム論に基づいて実行効率を改善するための方法論を提案した.

 本論文は構成的アルゴリズム論に基盤をおく。構成的アルゴリズム論(Constructive Algorithmics)とは、80年代後期に提案されたプログラムの計算法(calculus)であり、プログラムを変換するための規則を組織的に構築するための理論である.この手法では、プログラムをカテゴリ理論の枠組でとらえ,小数の強力な定理を用いてプログラムを構成的に変換していくことができる.ここで重要なのは,catamorphismと呼ばれる概念である.catamorphismとは,再帰的なデータ構造から別の再帰的な構造への「準同型」の形をした関数を指す.さらにcatamorphismとはカテゴリ的に「相対」の関係にあるanamorphismや,catamorphismとanamorphismとの合成によって表現されるhylomorphismが,プログラムの最適化において一番有用な部品として中心的な役割を果たすことがわかった.本論文は,まず第一に一般的な再帰定義をhylomorphismで表現するためのアルゴリズムを提案した.その結果,関数プログラムの最適化は一般的な再帰関数の代わりにhylomorphism上で議論すればよい.次に,本論文は構成的アルゴリズム論に基づいてプログラムを最適化するために

 ・プログラムの融合(fusion)の計算操作

 ・プログラムの組(tupling)の計算操作

 ・プログラムの副作用(side effect)の計算操作

 ・プログラムの並列化(parallelization)の計算操作

 に関して重要な定理及び変換アルゴリズムを与えた.これらの定理とアルゴリズムを系統的に適用することによって,効率のよい逐次または並列の関数プログラムを導くことができる.

 本論文の進展によって、効率の良いプログラムを導出するための方法論が確立されることが期待される。これにより,通常のプログラミング言語で書かれたプログラムを,機械的な処理によって並列に実行し効率を高めることが可能になる.このことは、将来のソフトウェア開発、特にコンパイラの構築において大きな意義を持つ。

審査要旨

 計算機プログラミングにおいては、解くべき問題に対する計算処理の明解な記述とその処理を実現するプログラムの効率的な実行という要求がある。処理を明解に記述したプログラムは問題の理解に役立ち、計算処理の正当性の証明にも有用であるが、実行する際には必ずしも効率的ではない。従来より、このような相反する要求を調和させるべく、明解な記述をもとに、效率のよいプログラムを導出する試みがなされてきている。これらの多くは、蓄積された事例に照らしてプログラムを改良したり、発見的な手法によってプログラムを変換しようとするものである。これに対して、プログラムを対象とした理論に基づき、数学的に等価性が保証される規則にしたがう変換によってプログラムを最適化する方法も考えられる。

 本論文は、このような背景のもとで構成的手法に基づくプログラムの変換について研究したもので、「構成的手法による関数プログラムの最適化(A Calculational Approach to Optimizing Functional Programs)」と題し、英文で書かれ、9章よりなる。

 第1章Introductionでは、本研究の背景と成果を要約するとともに、本論文の構成を述べている。

 第2章Preliminariesでは、本研究の対象とする関数プログラミングの概要と構成的アルゴリズム論の従来の成果を概観し、以下の各章で詳述する変換の基礎となる規則を圏論(カテゴリー論)の記法を用いて述べている。構成的アルゴリズム論では、プログラムを集合上の関数とし、集合を対象(object)、その上の関数を射(arrow)とする圏(category)においてその性質を議論する。ここでは、集合の圏の間の構造を保存する関手(functor)によって、プログラムの制御構造とデータ構造を代数系(F-algebra)として捉え、代数系を対象とし、これらの代数系の間の準同型(homomorphism)を射とする圏の上になり立つ性質に基づいていくつかの変換規則を導き出している。なかでも、関数の合成で表現された関数を、それと等価なひとつの関数に変換するという融合(fusion)の規則が本論文で扱う最適化手法の基礎になっている。

 第3章Towards Calculation:Deriving Hylomorphismsでは、本研究の中心的な課題である「計算(calculation)による変換」の基礎となる考え方と手法を扱っている。第2章であげた変換規則は変換後の関数の存在性を示しているが、そのような関数を求める方法は述べていない。本章では、その関数を(発見的に求めるのではなく)計算によって構成できる(機械的に求められる)ことを主張し、そのための準備を行なっている。ここでは、データ構造の上に定義される関数のほとんどのものは、対象とするデータ構造の分解、分解されたデータの変換、あらたなデータ構造の構築という3要素から構成されるhylomorphismという特別な形の関数に変換できることを述べ、一般の関数の定義をhylomorphismに変換するアルゴリズムを提示している。

 第4章Fusion in Calculational Formでは、前章に述べたアルゴリズムによってhylomorphismの形で表現された関数f,gの合成関数f・gをひとつの関数の定義に変換する融合の手法を述べている。この融合変換は、直観的にはhylomorphism gによるデータ構造の構築とhylomorphism fによるデータ構造の分解を相殺するものと捉えられるが、ここではそのために必要とされる条件を数学的に確立するとともに、融合変換を実現するためのアルゴリズムを示している。

 第5章Cheap Tupling in Calculational Formでは、関連する関数の組を構成することによって、データ構造を何度も走査したり重複した計算を伴うような関数の定義(明解な記述)を、データ構造を一度だけしかたどらず、重複計算もない効率のよい関数の定義に変換する構成的な手法を述べている。ここでも、従来の発見的な手法に対する計算的手法の優位性を主張している。

 第6章Calculating Accumulationsでは、伝統的な最適化手法である累積パラメタ(accumulating parameter)を構成的アルゴリズム論の立場から再検討し、それが関数に対する融合変換に対応していることを示し、従来は発見的に求めていたパラメタが機械的に得られることを主張している。また、そのアルゴリズムに基づいていくつかのプログラムを変換して有効性を示している。

 第7章Calculating Monadic Programsでは、関数プログラムで状態や入出力を扱うモナド(monad)を用いたプログラムに対する構成的な変換手法を述べている。

 第8章Calculating Parallel Functional Programsでは、プログラムの制御構造とデータ構造を一体化して捉える構成的アルゴリズム論の立場から、効率のよい並列関数プログラムを得る方法を述べている。ここでは、連接演算によって構成されるリスト構造が分割統治による並列性を具現していることに着目し、そのデータ構造の上に定義される関数に融合変換を適用して効率のよい並列プログラムを求める手法を提示している。

 第9章Concluding Remarksでは、以上をまとめると同時に、本論文の成果を実用規模のプログラムに適用するための変換システムの提案を行なっている。

 以上を要するに、本論文は計算機プログラムの最適化に関してあらたな方法論を理論的に展開するとともに、プログラムの変換アルゴリズムを示してその有効性を示したもので、情報工学・計算機科学の発展に寄与するところが大きい。よって本論文は博士(工学)の学位請求論文として合格と認められる。

UTokyo Repositoryリンク