先進的な高階書き換え理論に基づく遅延評価関数型プログラムの検証

点击翻译按钮获取中文摘要

研究期間の初年度に発表した論文により、帰納的定理の証明手法である潜在帰納法の適用のためには合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。(1) 前々年度に国内学会で発表した名目書き換えにおける合流性の成立条件について、未完成となっていた補題や定理の証明を完成させ、論文として国際会議で発表した。具体的な内容としては、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムに対して、アルファ同値性を法とした強可換性の概念を導入し、それを利用して基底名目項上の書き換えが合流性を満たす条件を提示した。この条件は、書き換え規則の間に重なりがある場合にも適用可能であり、前々年度に国際会議で発表した条件よりも広い範囲をカバーするものとなっている。(2) 局所十分完全性については、前年度に国際会議で発表した判定手続きを変更して、第一階項書き換えシステムよりも実際の関数型プログラミング言語に近い体系における類似の性質を判定するための手続きとして利用できないか検討した。また、第一階項書き換えシステムや関数型プログラミング言語における生成性の判定法など、関連する既存研究の手法について調査を進めた。これらを通じて得られた知見は、型変数や高階関数を持つ関数型プログラミング言語のプログラムに対する検証手法を開発するために重要になると考えられる。