2009 Fiscal Year Annual Research Report
| Project/Area Number |
20500008
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
草刈 圭一朗 Nagoya University, 大学院・情報科学研究科, 准教授 (90323112)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
|
|---|
| Keywords | 関数型言語 / 単純型付き書換え系 / 停止性 / 静的依存対法 |
|---|
| Research Abstract |
本研究の目的は、関数プログラムの停止性証明法の理論整備と、得られた理論成果に基づく停止性自動証明システムの構築である。特に、関数プログラムで広く利用されている高階関数への対応を重点に研究する。
今年度は以下の成果が得られた。
1.我々が提案した静的依存対法は関数プログラムの静的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法である。しかしながら、関数渡しが"適切"に行われていない場合は適用不能であることが判明している。昨年度に、剥離型と剥離順序と呼ばれる概念を導入することにより、関数渡しが安全となり、それゆえに静的依存対法が健全となるクラスを明らかにした。今年度は、このクラスが決定可能であることを明らかにした。また、より豊かな高階の系においても静的依存対法の理論が構築でき、この関数渡しが安全なクラスにおいては静的依存対法が健全となることを明らかにした。
2.静的依存対法を効果的かつ効率的に使用するためには引数切り落とし法と実効規則の概念が重要となってくる。本年度は、λ抽象を含む(それゆえにλ算法を含む)豊かな高階の系における、引数切り落とし法と実効規則の厳密な定義と正当性の証明を与えた。この成果によりλ抽象を含む高階の系における停止性証明が劇的に強力になった。
|
