| 研究課題/領域番号 |
25330096
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60443199)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | Coq / 型推論 / コード抽出 |
|---|
| 研究概要 |
平成25年度は，研究実施計画項目のうち，(1)Scalaコード抽出機本機能，(4)Scalaライブラリ，(5-1)MapReduceモデルを実施する計画であった．研究開始後の方針再策定の結果，平成25年度の作業としては(4)は基本的な機能に限定し，その替わりとして(1)を単に機能の実装にとどまらず，正当性の理論的な確立にまで範囲を広げて実施することとした．正当性を，型推論が常に成功することと，実行時エラーが生じないことの2つに分けて定式化し，前者の証明は完了した．抽出プログラムについては，Coqの他モジュールの変更に影響を受けにくい形となるように設計を行い，実装を完了させた．
項目(4)については，Coq の FSet モジュールに基づく集合ライブラリの実装のみを実施した．
項目(5-1)については，基本モデルとして，MapReduce 計算方式を Coq で記述した先行研究を用い，上述の実装によるコード抽出を行い，nativeなコードの場合とほぼ同等な性能が得られることを示した．
なお，当初計画になかった項目として，次の2点をケーススタディとして実施した．(a) データベースにおけるBASE特性の検証システムの構築を指向した，使用者の負担を減らすLtacライブラリの構築．(2) LMNtalコンパイラにおける中間命令のCoqによる実装．両項目とも，目標とするシステムの部分的な実装である．(a)では利用者の選択肢を限定しての証明から，(b)ではグラフ構造に関する証明からのコード抽出が可能であることを示した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
平成25年度で最も重要であると考えていた，基本機能の実装は完了した．一方で全体優先度の見直しの結果，Scalaライブラリなど一部の機能は平成26年度以降に延期したが，その替わりとして理論的扱いの強化を行い，必要な結果は得た．また，他のケーススタディは，当初予定以上の作業を実施して，結果を得ている．これらのことから，おおむね順調に進展していると判断する．
|
| 今後の研究の推進方策 |
基本機能は実現できたので，今後はこの機能を利用したケーススタディを続け，平成27年度に教材としてまとめることができるようにする．また，手続き的なプログラミングによって構築されたシステムの一モジュールとしての抽出を可能とする方法を追求していく．
|
| 次年度の研究費の使用計画 |
昨年度当初計画では，各年度ごとにほぼ同額を使用する予定でいた．しかし，年度途中で計画の見直しを行った結果，平成25年度はより理論的な扱いに重心を置き，平成26-27年度に実際のライブラリ開発など謝金等で費用の発生する研究項目を実施することとした．このため，平成25年度の執行額が当初予定より減ることとなった．
平成26年度は，当初予定通り国内学会参加3人回，国内研究打合せ10人回，国外学会参加3人回，英文添削1回の使用を行う予定である．これに加えて進捗に応じて平成25年度からの繰越し分を研究・開発補助者への謝金として (具体的には，ライブラリコード作成に対して) 使用する予定である．
|
