| 研究課題/領域番号 |
20500008
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
草刈 圭一朗 名古屋大学, 情報科学研究科, 准教授 (90323112)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
|
|---|
| 研究期間 (年度) |
2008 – 2011
|
| 研究課題ステータス |
完了 (2011年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2011年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2010年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2009年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2008年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
|---|
| キーワード | 計算理論 / 関数プログラム / 再帰定義 / 停止性 / 静的依存対法 / 関数型言語 / 単純型付き書換え系 / 停止性証明 / 静的再帰構造 |
|---|
| 研究概要 |
本研究の目的は、関数プログラムの停止性証明法の理論整備と、得られた理論成果に基づく停止性自動証明システムの構築である。特に、関数プログラムで広く利用されている高階関数への対応を重点的に研究する。
本目的に従い、我々は静的依存対法と言う、関数プログラムの静的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法を提案する。これは現在、高階関数を含む関数プログラムの停止性証明法としては実用上最も強力な手法である。本手法は一階の書換え系で提案された依存対法と、型付きλ計算の停止性証明のために導入された強計算性の概念に基づき設計される。また、静的依存対法により効果的かつ効率的に停止性を証明するために必須となる引数切り落とし法や実効規則も高階の書換え系上に拡張する。
さらに、得られた成果に基づき高階定理自動証明系HOPSYS(Higher-Order Proving SYStem)の停止性ライブラリを作成した。現在は、公開に向けてWebユーザインターフェースを開発中である。
|
