| 研究課題/領域番号 |
15K15974
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | 定理証明支援系 / 計算量 / 不等式 / 並列 |
|---|
| 研究実績の概要 |
本年度は、大きくふたつの観点について研究を進めた。
まず、定理証明支援系 Coq 上で並列計算量の形式的証明を支援するためのライブラリを構築し、そのライブラリの応用として極簡単な並列計算例についての並列計算量の形式的証明を示した。本ライブラリは、極簡単な並列モデルである fork/join をベースとし、プロセッサの動的再割当てのない環境を対象とした計算量の算出をサポートする。これにより、予め全データを利用可能な並列数に応じて分割しておくタイプのデータ並列な処理や並列スケルトンの証明が可能となった。また、簡単な実例を通し、実際に提案した枠組みで並列計算量の証明に応用できることを確認した。
次に、上記の応用例の証明において、定理証明支援系 Coq における形式的証明での不等式に関する扱いが非直観的であることに起因する困難を認識し、その困難解決のために不等式の証明を支援するライブラリの設計・構築を試みた。計算量の証明ではしばしば見積もられた計算量をより扱いやすい形の式で上から押さえるという操作を行う。そして、そのような不等式を連鎖させることで計算量の上限・上界を得る。しかし、この不等式の連鎖という証明の作法は通常の定理証明支援系での証明のそれとは異なるため、既存の環境では記述が煩雑になり困難であるという問題点が判明した。本研究ではそのような作法での証明記述を支援するライブラリのプロトタイプを構築し、その期待される有用性を確認した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究の目標であった定理証明支援系 Coq 上での並列計算量の形式的証明を支援するためのライブラリ構築が一段落し、その応用として簡単ではあるが並列計算例についての並列計算量の形式的証明を示すことができた。次の目標としてはより複雑な例への応用であるが、そこに存在する新たな問題点を発見することができ、その解決に取り組むアイデアの着想を得ることができた。そのため、総じて目標に向けて概ね順調に進んでいると判断する。
|
| 今後の研究の推進方策 |
次の目標である「より複雑な例への応用」に関して発見された「不等式操作が直観的でない」という問題に対し、それを解決する手法・ライブラリ等を実現し、並列計算量証明の枠組みと合わせてより大きな例に対する計算量証明を行って枠組み全体の評価を行おうと考えている。
|
| 次年度使用額が生じた理由 |
別に獲得した共同研究費を用いて出張を行ったため、次年度使用額が生じた。
次年度の対外発表の目の旅費として用いる予定である。
|
