| 研究課題/領域番号 |
25330096
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 大学院理学研究科, 准教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | Coq / 型推論 / コード抽出 |
|---|
| 研究実績の概要 |
Scalaコード抽出機能の理論的扱いについては，正当性証明をすすめた．平成25年度に証明した，生成コードの型検査が成功する事実をうけ，抽出前実行と抽出後実行の同一性の証明を目標とした．前段階として，Scala言語の意味論に基づいて同一性の定義を明確にした．証明については検討を進めた結果，この事実は常には成立しないことが判明し，その要因として2点を特定した．これら2点に影響されないための条件の検討を行い，判定可能な十分条件を得，平成25年度に作成したアルゴリズムの一部変更と合わせて，この十分条件の下での同一性の証明を完了した．
Scalaコード抽出機能の実装については，平成25年度にすでに実施しているが，平成26年度は型検査が成功することの証明をCoqによって形式化し，OCamlへのコード抽出機能を用いて実装を得ることに成功した．これによって，検証済のコード抽出機能が得られたことになる．なお，Coqによる証明の実装は，型推論アルゴリズム以降の部分であり，そこから呼び出されているユニフィケーション部分は引き続きOCamlのコードを用いている．また，前述したアルゴリズムの一部変更を反映したものを使用している．
ケーススタディーについては，LMNtalコンパイラ中間命令生成を拡充した．平成25年度にリンク生成削除に関するいくつかの命令を選び，その異なる実装の同値性を示したが，平成26年度は命令体系を見直し，追加・削除以外は1種類のリンク交換命令だけですべての処理を実施するモデルを選択し，その基本的な正当性記述を行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Scala抽出プログラムについては，主に理論的扱いについての進展を見た．当初の予想とは異なる形となることが判明したが，判定可能な十分条件を得たので，これに基づく実装を利用する際にも大きな障害はないと考えられる．実装についても，検証済プログラムを得たことは，平成26年度のまとまった成果だと言える．
ケーススタディーについても，平成25年度より格段に大きな規模のものとなったので，最終年度である平成27年度にこれを完成させることで，意味のある結果を得る準備が整った．
|
| 今後の研究の推進方策 |
当初予定していたライブラリ機能の拡充を重点的に行う．また，ケーススタディーも重要であるので，平成26年度に着手したLMNtalの新たなモデルの完成も，優先度を上げて取り組む．さらに，平成27年度は最終年度であるため，成果が一般から利用できるようにするために，ソースコードの公開や，利用文書の整備についても力を入れていく．
|
| 次年度使用額が生じた理由 |
平成26年度当初計画では，各年度ごとにほぼ同額を使用する予定でいた．しかし，平成25年度途中で計画の見直しを行った結果，1年目はより理論的な扱いに重心を置き，後の年度で実際のライブラリ開発など謝金等で費用の発生する研究項目を実施することとした．このため，平成27年度に繰り越しが生じている．
|
| 次年度使用額の使用計画 |
当初予定配分については，計画通り使用する予定である．また，繰り越し分は，ライブラリなどのコード開発作業に対する謝金として使用する．
|
