| 研究課題/領域番号 |
19K11891
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| キーワード | 書き換えシステム / プログラム検証 / 帰納的定理 / 合流性 / 局所十分完全性 |
|---|
| 研究実績の概要 |
研究期間の初年度に発表した論文により、帰納的定理の証明手法である潜在帰納法の適用のためには合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。
(1) 前々年度に国内学会で発表した名目書き換えにおける合流性の成立条件について、未完成となっていた補題や定理の証明を完成させ、論文として国際会議で発表した。具体的な内容としては、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムに対して、アルファ同値性を法とした強可換性の概念を導入し、それを利用して基底名目項上の書き換えが合流性を満たす条件を提示した。この条件は、書き換え規則の間に重なりがある場合にも適用可能であり、前々年度に国際会議で発表した条件よりも広い範囲をカバーするものとなっている。
(2) 局所十分完全性については、前年度に国際会議で発表した判定手続きを変更して、第一階項書き換えシステムよりも実際の関数型プログラミング言語に近い体系における類似の性質を判定するための手続きとして利用できないか検討した。また、第一階項書き換えシステムや関数型プログラミング言語における生成性の判定法など、関連する既存研究の手法について調査を進めた。これらを通じて得られた知見は、型変数や高階関数を持つ関数型プログラミング言語のプログラムに対する検証手法を開発するために重要になると考えられる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムにおける成立条件に関する成果を発表した。また、局所十分完全性については、関連する手法に対して調査を進めるとともに、関数型プログラミング言語に近い体系における類似の性質の判定法に関して検討を行った。以上のことと前年度までの進捗状況を合わせて考え、研究はおおむね順調に進展していると判断した。
|
| 今後の研究の推進方策 |
合流性については、名目書き換えシステムに関してこれまでに得られた知見をもとに、束縛変数を伴う書き換えシステムに対する判定手続きの構築に取り組む。局所十分完全性については、引き続き関連する手法に対して調査を進め、関数型プログラミング言語のモデルとなる体系における類似の性質を判定する手法の構築に取り組む。以上を含めたこれまでの成果・知見に基づくプログラム検証手法を実際のプログラムの例に適用することにより、その有効性を明らかにする。
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染拡大の影響を受けて出張を控えたことにより、旅費の使用額にずれが生じたため。繰り越し分は、研究環境整備と成果発表のための費用に充てる予定である。
|
