2013 Fiscal Year Research-status Report
静的再帰構造解析に基づく関数プログラムの停止性自動証明
| Project/Area Number |
24500012
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
草刈 圭一朗 岐阜大学, 工学部, 教授 (90323112)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
|
|---|
| Keywords | 情報基礎 / 関数プログラム / 停止性 / 再帰定義 |
|---|
| Research Abstract |
平成２６年度には，静的な再帰構造解析に基づく関数プログラムの停止性証明法が有効に機能するために必須となる簡約化順序として Weighted Path Order を提案した．
簡約化順序としてはこれまでにも，辞書式経路順序，再帰経路順序，Knuth-Bendix順序，多項式解釈に基づく順序など様々な順序が提案されてきている．我々の提案した Weighted Path Order はこれらの順序全てに共通する本質を洗い出し，この本質に基づき再構築することで設計してあるため，これらの順序を全て真に包含する非常に強力な順序である．
また，提案した Weighted Path Order は重みを定義する代数をパラメーターとして使用するのだが，実用上有効となる各種の代数も設計した．
さらに，近年飛躍的に能力を向上させているSMTソルバ(Satisfiability Modulo Theories Solver)との連携を図るために，Weighted Path Order と設計した代数のSMT問題への効果的かつ効率的なコーディング方法も与えた．
これらの成果により本研究は実用性を飛躍的に向上させることに成功した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成２５年度の目標としていた簡約化順序の設計としてWeighted Path Order という非常に強力な順序の設計に成功した．さらに，実用性を高めるためのSMTソルバとの連携法に関しても想定以上に良い成果が得られた．
一方，提案した順序や連携法は，本年度に計画していた関数プログラムで広く利用されている高階関数への対応がまだできていない．
|
| Strategy for Future Research Activity |
平成２５年度は，既存の簡約化順序の本質を洗い出すことに成功したために，Weighted Path Order の設計と，設計した順序のSMTソルバとの連携法に資源を集中的に投入し，本来の目標としていたのは関数プログラムで広く利用されている高階関数への対応が後回しになった．
平成２６年度にはこのやり残した箇所である，Weighted Path Order の高階関数への対応と，この順序のSMTソルバとの連携法を確立するのを目標とする．
|
-
-
-
-
-
[Presentation] Partial Status for KBO2013
Author(s)
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
Organizer
In Proc. of the 13th International Workshop on Termination (WST2013)
Place of Presentation
Bertinoro, Italy
Year and Date
20130829-20130829
