| 研究課題/領域番号 |
24500012
|
|---|
| 研究機関 | 岐阜大学 |
|---|
研究代表者 |
草刈 圭一朗 岐阜大学, 工学部, 教授 (90323112)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829) [辞退]
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2017-03-31
|
| キーワード | 情報基礎 / 関数プログラム / 停止性 / 再帰定義 |
|---|
| 研究実績の概要 |
静的な再帰構造解析に基づく関数プログラムの停止性証明法が有効に機能するためには簡約化順序と呼ばれる順序が必須となる．我々は平成25年度に重み付き経路順序と呼ぶ強力な順序を提案し，SMTソルバとの連携を図るための効果的かつ効率的なコーディング法も与えた．
平成26年度には，これらの成果をさらに発展させた．また，発展させた成果に基づき停止性自動証明ツールである Nagoya Termination Tool を作成した．停止性証明ツールの競技会である2014年度の International Termination Competition に我々のツールで出場したところ，ほぼ重み付き経路順序のみに停止性証明を頼っているにも関わらず，総合2位の成績を獲得できた．これは我々の重み付き経路順序の強力さを証明するものであり，我々の研究方向の正しさを証明するものであると考える．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
得られた成果である重み付き経路順序とSMTソルバとの連携法に基づき非常に強力な停止性証明ツールを作成できた．
一方，本ツールは関数プログラムで広く利用されている高階関数への対応がまだできていない．
|
| 今後の研究の推進方策 |
我々の目標である関数プログラム停止性自動証明ツールは静的な再帰構造解析に基づく停止性証明法である静的依存対法に基づき設計する予定である．この静的依存対法の設計は完了している．静的依存対法が有効に機能するためには簡約化順序，引数切り落とし法，実効規則の３つの理論が必要となる．簡約化順序としては非常に強力な重み付き経路順序を設計したものの高階関数に対応していないため，この対応が目標となる．また，引数切り落とし法と実効規則に関しては関数抽象に完全に対応しきれていない．この対応も目標となる．これらの理論的目標を達成した後に，得られた理論に基づく関数プログラムの停止性自動証明ツールを作成してするのが最終目標となる．
|
