2014 Fiscal Year Research-status Report
静的再帰構造解析に基づく関数プログラムの停止性自動証明
| Project/Area Number |
24500012
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
草刈 圭一朗 岐阜大学, 工学部, 教授 (90323112)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829) [Withdrawn]
|
|---|
| Project Period (FY) |
2012-04-01 – 2017-03-31
|
| Keywords | 情報基礎 / 関数プログラム / 停止性 / 再帰定義 |
|---|
| Outline of Annual Research Achievements |
静的な再帰構造解析に基づく関数プログラムの停止性証明法が有効に機能するためには簡約化順序と呼ばれる順序が必須となる．我々は平成25年度に重み付き経路順序と呼ぶ強力な順序を提案し，SMTソルバとの連携を図るための効果的かつ効率的なコーディング法も与えた．
平成26年度には，これらの成果をさらに発展させた．また，発展させた成果に基づき停止性自動証明ツールである Nagoya Termination Tool を作成した．停止性証明ツールの競技会である2014年度の International Termination Competition に我々のツールで出場したところ，ほぼ重み付き経路順序のみに停止性証明を頼っているにも関わらず，総合2位の成績を獲得できた．これは我々の重み付き経路順序の強力さを証明するものであり，我々の研究方向の正しさを証明するものであると考える．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
得られた成果である重み付き経路順序とSMTソルバとの連携法に基づき非常に強力な停止性証明ツールを作成できた．
一方，本ツールは関数プログラムで広く利用されている高階関数への対応がまだできていない．
|
| Strategy for Future Research Activity |
我々の目標である関数プログラム停止性自動証明ツールは静的な再帰構造解析に基づく停止性証明法である静的依存対法に基づき設計する予定である．この静的依存対法の設計は完了している．静的依存対法が有効に機能するためには簡約化順序，引数切り落とし法，実効規則の３つの理論が必要となる．簡約化順序としては非常に強力な重み付き経路順序を設計したものの高階関数に対応していないため，この対応が目標となる．また，引数切り落とし法と実効規則に関しては関数抽象に完全に対応しきれていない．この対応も目標となる．これらの理論的目標を達成した後に，得られた理論に基づく関数プログラムの停止性自動証明ツールを作成してするのが最終目標となる．
|
-
-
[Presentation] Nagoya Termination Tool2014
Author(s)
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
Organizer
n Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications
Place of Presentation
Vienna (Austria)
Year and Date
2014-07-15 – 2014-07-15
-
