2012 Fiscal Year Annual Research Report
代数的ソフトウェア向き多重文脈型推論基盤システムのスケーラブルな並列実装と応用
| Project/Area Number |
22500022
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | 項書換えシステム / 並列プログラミング / 多重文脈推論 / 停止性検証 / 人工知能 / ソフトウェア学 / 代数学 |
|---|
| Research Abstract |
文脈が互いに類似した非決定性並行プロセス間には，多くの場合，同一の計算・推論処理が多数共通に存在するため，本研究は，それらを共通に処理することによってシステム性能を飛躍的に高めることを狙った「多重文脈型推論」の基盤を開発するという全体構想の中で，(1)並列計算機におけるスケーラブルな並列実装方式を開発してシステムのパワーを格段に高めること，及び(2)代数的ソフトウェアの仕様検証分野においてこれまで解けなかった帰納的定理証明等の応用課題に挑戦してその可用性を高めること，を目的として実施してきた。
平成24年度には，平成23年度までに実施した「帰納的定理証明とその並列性に関する調査・検討」及び「並列プログラミング言語に関する動向調査」の結果に基づき，(1)「スケーラブルな並列実行方式の検討」を引き続き実施すると共に，(2)「多重文脈型推論基盤システムのスケーラブルな並列実装」を行い，計算機実験による評価を行った。
(1)並列プログラミングの基礎となる並列計算モデルについて基本的な検討を行い，不適切なPRAMモデルの代わりに実践的なCTAモデルに基づき，項書換えシステムにおける等式や書換え規則の生成・更新処理を含む停止性チェッカーの並列化処理、特にプロセス間のシステム終了（成功）条件の判定処理等の実装を検討の対象として，スケーラブルな並列実行方式について検討し，関数型言語Erlangを採用して実装を行い，期待していた性能を確認した。
(2)多重文脈型推論基盤システムを再実装し，帰納的定理証明システムに応用して計算機実験による評価を行うとともに，今後の課題を明らかにした。
なお，連携研究者として，佐藤晴彦（北大）からソフトウェアの実装・実験を行う等の連携協力を得た。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
