研究課題
基盤研究(C)
本研究の目的は、関数プログラムの停止性証明法の理論整備と、得られた理論成果に基づく停止性自動証明システムの構築である。特に、関数プログラムで広く利用されている高階関数への対応を重点的に研究する。本目的に従い、我々は静的依存対法と言う、関数プログラムの静的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法を提案する。これは現在、高階関数を含む関数プログラムの停止性証明法としては実用上最も強力な手法である。本手法は一階の書換え系で提案された依存対法と、型付きλ計算の停止性証明のために導入された強計算性の概念に基づき設計される。また、静的依存対法により効果的かつ効率的に停止性を証明するために必須となる引数切り落とし法や実効規則も高階の書換え系上に拡張する。さらに、得られた成果に基づき高階定理自動証明系HOPSYS(Higher-Order Proving SYStem)の停止性ライブラリを作成した。現在は、公開に向けてWebユーザインターフェースを開発中である。
すべて 2012 2011 2010 2009
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (12件)
IPSJ Transactions on Programming
巻: Vol.4, No.2 ページ: 1-12
IEICE Transactions on Information and Systems
巻: Vol.E92-D, No.10 ページ: 2007-2015
巻: Vol.2, No.3 ページ: 20-32
巻: Vol.E92-D, No.2 ページ: 235-247
