2014 Fiscal Year Research-status Report
代数的ソフトウェア向き多重文脈型推論基盤システムによる帰納的定理証明とその応用
| Project/Area Number |
25330074
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書換え系 / 帰納的定理証明 / 代数的ソフトウェア / 多重文脈型推論 |
|---|
| Outline of Annual Research Achievements |
文脈（計算開始から現時点までに行った選択の列）が互いに類似した非決定性並行プロセス間には，多くの場合，同一の計算・推論の処理が多数共通に存在する。本研究は，それらを共通に処理することによってシステム性能を飛躍的に高めることを狙った「多重文脈型推論」の基盤を開発するという全体構想の中で，(1) 補助定理を自動生成して帰納的定理の自動証明を行う多重文脈型推論システムを開発すること，及び(2)それを代数的ソフトウェアの正しさの検証に応用してその可用性を高めること，を目的としている。
平成26年度は，前年度に実施した基礎技術の調査とシステムの計画に基づいて，計算環境を整備しつつ，システムの実装に着手し，一部の評価を行なった。具体的には以下のとおりである。
１．実装のプラットフォームとして，本研究経費の設備備品費で購入した64コアの並列計算機システムを用いて，システムの設計・実装に関して研究を進めた。システムが正しく帰納的定理証明を実行することを確認すると共に，予備的な評価を実施した。これは，このこと自体がこの分野における新しい技術である点で意義のある成果であるほか，平成27年度に実施する本格的な実装と評価に向けて重要なステップとなっている。
２．上記システムの一部である停止性自動証明を並列計算機に実装した技術および開発環境整備の一環として使用した自動テスト生成技術については，査読付き論文として国際的な論文誌に投稿し，掲載された。
３．上記システムの帰納的定理証明を実行するために必要な多重文脈型推論基盤システムについて，関数型言語の遅延評価機構を利用して効率的に実装する技術を，それぞれ査読付き論文として国際会議において公表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の目的に照らして事前に計画したとおり，平成25年度には，主として基礎技術の調査とシステムの計画に係る研究を推進し，補助定理の生成や定理の発見の基礎技術の調査を行い，それらの技術から本研究の目的に適したものを取捨選択し，システムを計画し，平成26年度には，その計画に基づいて，本研究経費の設備備品費で購入した64コアの並列計算機システムを用いて，開発環境を整備しつつ，システムの設計・実装に着手し，予備的な評価を実施した。
上記研究活動においてマイルストーンと考えられる成果については，国際的な論文誌あるいは国際会議に投稿し，査読の結果，良好な成果として評価され，採択されていることから，本研究はその目的の達成に向けて，おおむね順調に進展していると判断する。
|
| Strategy for Future Research Activity |
平成27年度は，研究の目的に照らして事前に計画したとおり，帰納的定理証明に関する標準問題を用いて，開発したシステムの性能評価を行い，必要に応じて設計・実装の改善を行う。また，応用分野であるプログラム検証の分野について調査を行い，その分野特有の問題群を用いて，開発したシステムの可用性の評価を行い，必要に応じて設計・実装の改善を行う。そして本研究の成果を総括し，論文等により公表するほか，ホームページ等においてアイデアの原理やその社会的意義等について啓発を行う。
なお，連携研究者の佐藤晴彦は，引き続き，実装および評価に係る部分に関して連携研究を行う。
|
| Causes of Carryover |
旅費や参加費を支出することとなる国際会議への参加について，３月中旬に行なったが，会計上，その支払い（290,256円）は翌月である４月に行なわれるので，３月末時点での状況を記入する今回の報告書にはその支出を計上していないために，形式上，残余金の一部として見えることになる。また，この出張は，当初３名参加の予定が公務のため２名となり，また，予定よりも開催地が日本に近かった（香港）ことと，登録参加費が予想より低額であったため，結果的に次年度使用額の増分の一因となった。
|
| Expenditure Plan for Carryover Budget |
上記の使用額については，平成２７年度の旅費および参加費の一部として使用する予定である。
|
