2012 Fiscal Year Research-status Report
静的再帰構造解析に基づく関数プログラムの停止性自動証明
| Project/Area Number |
24500012
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
草刈 圭一朗 名古屋大学, 情報科学研究科, 准教授 (90323112)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
|
|---|
| Project Period (FY) |
2012-04-01 – 2017-03-31
|
| Keywords | 情報基礎 / 関数プログラム / 停止性 / 再帰定義 |
|---|
| Research Abstract |
平成２４年度には，静的な再帰構造解析に基づく関数プログラムの停止性証明法である静的依存対法を二つの方向に拡張することに成功した．
一つ目は，多相型と代数的データ型を含む系への拡張である．この拡張は実用上大きな意味を持つ．この拡張により，実用的な関数プログラミング言語(SML#,SML/NJ,OCaml,Haskell等)により記述された多くの関数プログラムに静的依存対法を適用することが可能になった．
二つ目は，パターン付きの関数抽象を含む系への拡張である．この拡張は理論上大きな意味を持つ．この拡張により，書換え系モデルを土台に得てきた静的依存対法の研究成果がλ計算や型理論の枠組みでの研究にも応用可能になった．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
平成２４年度の目標としていた代数的データ型と多相型への静的依存対法への対応が完全にできた．さらに，平成２４年度の目標としては考慮していなかったパターン付きの関数抽象への対応にも成功した．
|
| Strategy for Future Research Activity |
現在の所，順調に研究が進展していることもあり，今後の研究は応募時の予定通りに行いたいと考える．平成２５年度の研究目標は応募時と同じく以下の拡張とする．
静的依存対法と全く異なる停止性証明手法である高階経路順序法の研究において，OCaml等の開発で有名なフランス国立研究所であるINRIAのJ.-P. JouannaudとF. Blanqui によって可触性の概念が与えられた．彼らの研究においては，型の解釈に基づく完備束となる関数空間を与え，その上のある種の単調関数が与える最小不動点をもって強計算性の定義を与えている．我々が用いていた"強計算性"の定義を，この非常に高度な数学を駆使した手法により与えられる"強計算性"に置き換えることにより，静的依存対法の適用可能なクラスが拡張できるという感触を得ている．この拡張を平成２５年度の目標とする．
|
| Expenditure Plans for the Next FY Research Funding |
予定通りである．すなわち，物品費100,000円，旅費400,000円，人件費・謝金100,000円，その他100,000円に，間接経費210,000円を加えた合計910,000円である．
|
