2021 Fiscal Year Research-status Report
Incremental Computing based on Program Transformations
| Project/Area Number |
19K11896
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
森畑 明昌 東京大学, 大学院総合文化研究科, 准教授 (10582257)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 漸増計算 / パラメトリック多相型 / プログラム変換 |
|---|
| Outline of Annual Research Achievements |
ある入力に対して一度計算を行った後に入力がわずかに変化したとき、以前の計算結果を利用して迅速に変更された入力に対する計算結果を得る技法を漸増計算と呼ぶ。本研究では、漸増計算を考慮せずに記述したプログラムを漸増計算を行うプログラムへ変換する（これを「漸増化」と呼ぶ）というプローチによって、一般的な漸増計算技法を与えることを目標としている。
本研究では、特にパラメトリック多相型の理論に基づく漸増計算手法に注目し、これを用いて既存手法を整理し一般化することを目指してきた。しかし、昨年度の時点で、当初考えていた方針では、手法の正しさの証明に行き詰まることが発覚していた。これをふまえ、今年度は、以下の2点に関して研究を進めた。
(1) パラメトリック多相型の理論を用いた既存の（漸増計算に限らない）研究を精査し、漸増計算に利用できる証明技法を抽出すること
(2) 特定の漸増計算パターンに対してのケーススタディを行い、漸増計算手法として求められる用件を整理すること
(1) に関しては、融合変換と呼ばれる、漸増計算の実現にも用いられることのあるプログラム変換技法について、その証明が既存のパラメトリック多相型の理論では（驚くべきことに）あまりうまく行かないことを確認し、さらにこの問題を解決する新しい証明技法を開発した。この内容の初期の成果は日本ソフトウェア科学会の大会で発表し、現在論文投稿に向けて準備中である。またこれ以外にも、パラメトリック多相型を用いた証明についての発見があり、既に論文を投稿中である。
(2) に関しては、特に多次元配列を何度も処理するような計算パターンについて、漸増化を用いて自動的に効率を改善する新しい手法を開発した。この成果は情報処理学会論文誌 「プログラミング」に投稿し、採択された。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初考えていた証明方針がうまく行かないことが昨年度に発覚し、その問題は本年度を通しても完全には解決していない。その意味で、研究はやや遅れているといわざるを得ない。一方で、本年度には当初の見通しとは異なる形での研究成果が複数出ており、全体としてみれば良い進捗があったとも言える。
|
| Strategy for Future Research Activity |
本年度を通して、パラメトリック多相型を用いた証明技法についての理解は大いに深まった。これをふまえ、当初の問題に立ち返り、パラメトリック多相型に基づく漸増計算手法を確立する。場合によっては、当初考えていたほど一般性の高い理論を与えることはできないかも知れないが、どの範囲であれば証明が問題なく可能であるかも含め精査したい。
|
| Causes of Carryover |
コロナ禍ということもあり、オンライン開催の学会ばかりであり、旅費等での出費がほとんど無かったことが主な理由である。
|
