| 研究概要 |
本研究の目的は,関数プログラムの停止性証明法の理論整備と,得られた理論成果に基づく停止性自動証明システムの構築である.特に,関数プログラムで広く利用されている高階関数への対応を重点的に研究する.
今年度は以下の成果が得られた。
1.我々が提案した静的依存対法は関数プログラムの静的再帰構造を解析することにより停止性を証明する非常に強力でかつ効率的な手法である.しかしながら,関数渡しが"適切"に行なわれていない場合は適用不能であることが判明している.すでに我々は関数渡しが平坦(plain)ならば静的依存対法が健全となることを明らかにしていた.今年度は,剥離型及び剥離順序と呼ぶ概念を導入することによって,静的依存対法が健全となるための条件を抽象的に定式化することに成功し,適用可能なクラスを拡張することに成功した.
2.静的依存対法で停止性証明を行なう際には,静的再帰構造解析の結果得られる全ての静的再帰成分が非循環的であることを示す必要がある.今年度は,簡約対と呼ばれる非循環性を示す順序の代表的な生成法である引数切り落とし法を改良した.従来の引数切り落とし法は項の型構造を破壊するため順序の生成に関して非常に強い制限が課されていたが,項の型構造を破壊しないよう改良することにより,引数切り落とし法の取り扱いやすさを飛躍的に向上させた.
3.実効規則の概念を用いると静的再帰成分の非循環性を示す際の制約を劇的に削減できる.今年度は,実効規則に引数切り落とし法を組合せ,制約の削減度合いを向上させることに成功した.
|
