2018 Fiscal Year Annual Research Report
Towards parallel programming environment with certified correctness and complexity
| Project/Area Number |
15K15974
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | 定理証明支援系 / 並列プログラミング |
|---|
| Outline of Annual Research Achievements |
本年度は、主に、定理証明支援系における一般化した不等式（半順序など）の扱いに関する成果を得た。プログラムの効率ないし計算時間（計算量）を定理証明支援系を用いて形式的に保証するためには、厳密な計算時間の議論は環境依存となるため不可能であり、どうしても細かい差異を無視して少し多めに見積もる為の不等式の扱いが必要となる。しかし、現状の定理証明支援系ではその扱いが自然でなく、計算量の証明に本質的ではない困難が生じていた。本研究は、その不等式の扱いを自然に記述できる仕組みとその一般化を提案した。これにより、計算量証明などに現れる不等式の扱いのみならず、その他プログラムに関する一般化した関係（例えば書き換え関係など）での証明も直観的に行えるようになった。また、開発した手法を適用するための並列プログラミング言語として、大規模グラフ計算のための並列プログラムの開発を行った。
本研究の目的は、従来手法が対象とする「正しさ」のみでなく、その「並列計算量（実行時間）」をも形式的に保証できるような並列プログラミング環境の構築である。そのための基盤技術として、本研究は、研究期間中に大きく次の二点についての成果を得た：（１）局所計算量をプログラム中に自然に併記できるモナドに基づく逐次計算量の形式的記述手法の並列計算量への拡張、（２）定理証明支援系における不等式などの扱いを簡潔にし、計算量証明を行いやすくする技術。これらにより、並列実行の仕組みに制限はあるものの、機械により「速さ」と「正しさ」が保証される並列プログラムの開発が容易になった。
|
