| 研究課題/領域番号 |
15K15965
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
森畑 明昌 東京大学, 大学院総合文化研究科, 准教授 (10582257)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | 自動並列化 / 型システム / ラムダ計算 |
|---|
| 研究実績の概要 |
2017年度は引き続き自動リダクション並列化をを研究するための理論的基盤としてのラムダ計算体系の定式化に取り組んだ。これは通常のラムダ計算に結合法則や分配法則など代数的性質を用いた式の単純化を加えたものであり、型システムによって並列計算時の計算コストに保証を与えている。前年度までに定式化の大筋はできあがっていたのだが、詳細を詰めてゆく過程で2つの問題点が発覚した。1つは、現実のプログラムをこの体系でモデル化することの難しさである。ラムダ計算は現実のプログラムのほとんどの要素を表現できることが知られている。しかし、今回の体系では、並列計算が可能となるかどうかがエンコードの詳細に依存することが発覚し、そのため既知の結果を素直に応用することはできなかった。もう一つは、型システムの能力とその安全性の証明である。本体系では型システムが並列計算の性能を保証する。この保証は、型システムが多くのプログラムを却下すれば簡単だが、何でも却下するようでは使い物にならならない。一方で、詳細な解析を型システムが行うほど、その性質の証明は難しくなり、また型推論・型検査の実用的なアルゴリズムも構築し難くなる。前年度までの型システムはアドホックに設計してきたため、適切なものがなかなか与えられずにいた。本年度はこれらの解決を目指し研究を行った。進捗が研究の細部であることもあり、具体的な成果として公表できる形にはなっていないが、上記問題を概ね解決することに成功した。
なお、これと平行し、並列プログラムの代数的性質を用いた自動的な効率化の可能性について研究を行った。特に、SMTソルバーなどの制約解消器を用いることで非自明な効率化を行う手法を提案した。この成果を第34回ソフトウェア科学界大会で発表した。この成果を発展させたものは、来年度開催される国際会議FLOPS 2018での採択が決まっている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
上述の通り、詳細を詰める際に深刻な問題が発見され、その解決に予想以上の時間を要したためである。
|
| 今後の研究の推進方策 |
現時点での成果をまとめ、出版することが重要だと考えている。
|
| 次年度使用額が生じた理由 |
研究の理論的詳細の改善が必要となったため、研究全体としてデスクワークが中心となり、また成果の発表にも至らなかった。また、研究のための備品等については前年度までに購入したもので不足がなかった。以上の状況から、今年度は予定に比して使用額が少なくなっている。
|
