| 研究課題/領域番号 |
19K11891
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | 書き換えシステム / プログラム検証 |
|---|
| 研究実績の概要 |
昨年度までの研究により、第一階項書き換えシステムにおける帰納的定理の証明手法である潜在帰納法の適用のためには、合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。
(1) 束縛変数を伴う項を扱えるように第一階項書き換えシステムを拡張した名目書き換えシステムに対し、新たな合流性の成立条件等の提案を行った。具体的には、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムの合流性とその一般化である可換性の成立条件を提案した。アトム変数を用いる書き換え規則によって定義される名目書き換えシステムは、書き換えの対象が基底名目項に制限されるものの、置換ではなく代入を用いて書き換えが定義されるため、従来の名目書き換えシステムよりも理解が容易である。帰納的定理の証明やプログラム変換の正当性に応用するためには、基底項に対する合流性を考えれば十分であるため、ここで得られた成果・知見は、第一階項書き換えシステムに基づく潜在帰納法等の手法を名目書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 局所十分完全性については、昨年度提案した判定のための導出システムと、自動判定に適した十分条件を整理・発展させることに取り組んだ。まず、自動判定に適した十分条件を洗練し、その正当性の証明を見通しの良い形に整理した。この十分条件を用いることにより、昨年度提案した導出システムでは判定困難な例に対しても局所十分完全性の成立を判定可能な場合が存在する。一方、導出システムのほうでは、局所十分完全性の対象となる項における最外の関数記号だけでなく、部分項の構造についても考慮されている。そのため、これら2つの手法を相補的に用いることにより、適用範囲の広い判定手続きが得られることが期待できる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムを対象とした成果・知見が、また、局所十分完全性については、判定手続きに関する知見がそれぞれ得られ、おおむね計画通りに研究を進めることができたため。
|
| 今後の研究の推進方策 |
局所十分完全性については、関連する手法に対して調査を行うとともに、第一階項書き換えシステムを拡張した体系における同様な性質についても検討する。また、具体例による実験の準備に取り掛かる。合流性については、束縛変数を伴う高階の書き換えシステムに対する新しい判定条件の提案を検討する。
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染拡大防止に伴う自粛の要請を受けて出張を控えたことにより、旅費の使用額にずれが生じたため。繰り越し分は次年度の助成金と合わせ研究環境整備に充てる予定である。
|
