| 研究概要 |
文脈(計算開始から現時点までに行った選択の列)が互いに類似した非決定性並行プロセス間には,多くの場合,同一の計算・推論処理が多数共通に存在する。本研究は,それらを共通に処理することによってシステム性能を飛躍的に高めることを狙った「多重文脈型推論」の基盤を開発するという全体構想の中で,(1)並列計算機におけるスケーラブルな並列実装方式を開発してシステムのパワーを格段に高めること,及び(2)代数的ソフトウェアの仕様検証分野においてこれまで解けなかった帰納的定理証明等の応用課題に挑戦してその可用性を高めること,を目的とする。
平成23年度には,主としてシステムの計画・設計及びそれに続く下記研究を実施した。
(1)スケーラブルな並列実行方式の検討
並列プログラミングの基礎となる並列計算モデルについて基本的な検討を行い,実践的なCTAモデルを採用して,等式や書換え規則の生成・更新処理,停止性検証の処理,及びシステム終了(成功)条件の判定処理等を検討の対象として,スケーラブルな並列実行方式について検討を行い,基本設計を行った。
(2)並列プログラミング言語に関する動向調査
実装に用いる並列プログラミング言語に関する調査を行い,関数型言語をベースとして並列計算を可能とするErlangに候補をしぼる作業を行い,本研究経費の設備備品費で購入した並列計算機により,予備的な実験等を実施した。
(3)多重文脈型推論基盤システムのスケーラブルな並列実装
(1)及び(2)の検討結果に基づき,多重文脈型推論基盤システムをErlangにより実装し,帰納的定理証明システムへの応用へ向けた開発を実施した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
スケーラブルな並列実行方式の検討を行い,並列プログラミング言語に関する動向調査を行い,その結果に基づいて,多重文脈型推論基盤システムのスケーラブルな並列実装を行った点で,当初の計画どおりである。しかし,実装の評価までは進んでいないため,当初の計画以上に進展しているというほどではない。
|
| 今後の研究の推進方策 |
平成24年度には,平成23年度までに実施した「帰納的定理証明とその並列性に関する調査・検討」及び「並列プログラミング言語に関する動向調査」の結果に基づき,「スケーラブルな並列実行方式の検討」を引き続き実施すると共に,「多重文脈型推論基盤システムのスケーラブルな並列実装」を行い,計算機実験による評価を行う。
ソフトウェアの実装・実験と評価に関しては,連携研究者である佐藤晴彦氏(北海道大学)からの連携協力を得る。
|
