| 研究課題/領域番号 |
20500008
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 准教授 (90323112)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
|
|---|
| キーワード | 関数プログラム / 再帰定義 / 停止性 |
|---|
| 研究概要 |
本研究の目的は、関数プログラムの停止性証明法の理論整備と、得られた理論成果に基づく停止性自動照明システムの構築である。特に、関数プログラムで広く利用されている高階関数への対応を重点的に研究する。
今年度は以下の成果が得られた。
1.我々が提案した静的依存対法は関数プログラムの性的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法である。静的依存対法を効果的かつ効率的に使用するためには引数切り落とし法と実効規則の概念が重要となってくる。本年度は、匿名関数を記述するために用いられる関数抽象を含む豊かな高階の系における、引数切り落とし法と実効規則の厳密な定義と正当性の証明を与えた。この成果により匿名関数を利用した高階関数プログラムの停止性証明が劇的に強力になった。
2.開発中の高階定理自動証明系HOPSYS(Higher-Order Proving SYStem)の停止性ライブラリに前年度までのほぼ全ての成果を実装した。現在は、公開に向けてWebユーザインターフェース等の開発中である。
|
