2016 Fiscal Year Research-status Report
代数的ソフトウェア向き多重文脈型推論基盤システムによる帰納的定理の発見と証明
| Project/Area Number |
16K00090
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 帰納的定理証明 / 項書換え系 / 書換え帰納法 / 多重文脈型推論 / 補助定理 / 定理発見 / 発散鑑定 |
|---|
| Outline of Annual Research Achievements |
本研究は，推論システムにおける「文脈」が互いに類似した複数の非決定性並行プロセスにおける推論を共通に効率良く処理する「多重文脈型推論」の基盤を開発するという全体構想の中で，(1)補助定理を自動生成して帰納的定理の自動証明を行うこと，及び(2)それを代数的ソフトウェアの正しさの検証に応用することを目的としている。
平成28年度には，要素技術の調査とシステムの計画に係る研究を推進した。具体的には以下の研究実績を得た。
（１）トップダウン的な補助定理自動生成技術の最近の状況について調査を行った。その代表的な手法である「発散鑑定法」は既存研究と本研究は理論的枠組みが異なるため，既存研究の成果を本研究の「書換え帰納法」の枠組みで形式化を行った。
（２）ボトムアップ的な補助定理自動生成技術の最近の状況について調査を行い，その代表的な手法である「定理発見」について，書換え帰納法の枠組みで形式化を行った。また，その一部に新しいヒューリスティックスを導入した手法を考案し，国際会議(SMC 2016)において公表した。具体的には，補助定理を動的に生成してシステムに追加するときの制約，冗長な補助定理を除去する基準，補助定理の書換え規則への向き付けに関して新しいヒューリスティクスを導入し，実験により良好な結果を得ている。
（３）上記で調査・整理したトップダウン及びボトムアップの手法の特徴を，書換え帰納法を基礎とする多重文脈型推論システム内で総合化するために，システムの基本的な骨組みとなる推論系及びアルゴリズムの開発に着手し，一部を実装した。特に，関数型言語の遅延評価の仕組みを利用した効率良い実装技術については，国際研究集会(CLA 2016)において公表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初計画のとおり，以下の３つの平成２８年度計画項目を順調に実施している。
（１）トップダウン的な補助定理自動生成技術の最近の状況調査については，当初の計画のとおり，その代表的な手法である「発散鑑定法」について調査を行ったほか，その調査結果を本研究の「書換え帰納法」の枠組みで形式化することができた。
（２）ボトムアップ的な補助定理自動生成技術の最近の状況調査については，当初の計画のとおり，その代表的な手法である「定理発見」について調査を行ったほか，書換え帰納法の枠組みで形式化を行った。また，その一部に新しいヒューリスティックスを導入した手法を考案し，国際会議(SMC 2016)において公表した。
（３）上記で調査・整理したトップダウン及びボトムアップの手法の特徴を，書換え帰納法を基礎とする多重文脈型推論システム内で総合化するために，当初の計画のとおり，システムの基本的な骨組みとなる推論系の開発に着手し，一部を実装した。特に，関数型言語の遅延評価の仕組みを利用した効率良い実装技術については，国際研究集会(CLA 2016)において公表した。
|
| Strategy for Future Research Activity |
平成２９年度は，当初の計画どおり，実装のプラットフォームとして並列計算機システムを本研究経費で購入し，システムの設計・実装に関して研究を進める。特に，平成２８年度の成果である発散鑑定法と定理発見については，より深く技術を追求し，独創的な研究成果が得られるように努める。
平成３０年度は，当初の計画どおり，代数的ソフトウェアの応用分野を対象としてシステムの性能評価を行い，必要に応じて設計・実装の改善を行う。
なお，引き続き，連携研究者の佐藤晴彦と実装及び評価に係る研究に関して連携協力を行う。また，実装の具体は，引き続き，研究協力者（大学院生）が行う。
|
| Causes of Carryover |
計画当初は，平成２８年度旅費として，研究代表者と連携研究者の２名について，外国旅費の予算を想定していたが，実際には，連携研究者は本研究費以外の予算を旅費として使用することとなったため，それに相当する程度の予算が余ることとなった。
|
| Expenditure Plan for Carryover Budget |
次年度使用額に相当する予算については，平成２９年度の旅費に追加し，研究代表者または連携研究者または研究協力者が使用できるようにしたい。
|
