2020 Fiscal Year Research-status Report
先進的な高階書き換え理論に基づく遅延評価関数型プログラムの検証
| Project/Area Number |
19K11891
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 書き換えシステム / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
昨年度までの研究により、第一階項書き換えシステムにおける帰納的定理の証明手法である潜在帰納法の適用のためには、合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。
(1) 束縛変数を伴う項を扱えるように第一階項書き換えシステムを拡張した名目書き換えシステムに対し、新たな合流性の成立条件等の提案を行った。具体的には、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムの合流性とその一般化である可換性の成立条件を提案した。アトム変数を用いる書き換え規則によって定義される名目書き換えシステムは、書き換えの対象が基底名目項に制限されるものの、置換ではなく代入を用いて書き換えが定義されるため、従来の名目書き換えシステムよりも理解が容易である。帰納的定理の証明やプログラム変換の正当性に応用するためには、基底項に対する合流性を考えれば十分であるため、ここで得られた成果・知見は、第一階項書き換えシステムに基づく潜在帰納法等の手法を名目書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 局所十分完全性については、昨年度提案した判定のための導出システムと、自動判定に適した十分条件を整理・発展させることに取り組んだ。まず、自動判定に適した十分条件を洗練し、その正当性の証明を見通しの良い形に整理した。この十分条件を用いることにより、昨年度提案した導出システムでは判定困難な例に対しても局所十分完全性の成立を判定可能な場合が存在する。一方、導出システムのほうでは、局所十分完全性の対象となる項における最外の関数記号だけでなく、部分項の構造についても考慮されている。そのため、これら2つの手法を相補的に用いることにより、適用範囲の広い判定手続きが得られることが期待できる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムを対象とした成果・知見が、また、局所十分完全性については、判定手続きに関する知見がそれぞれ得られ、おおむね計画通りに研究を進めることができたため。
|
| Strategy for Future Research Activity |
局所十分完全性については、関連する手法に対して調査を行うとともに、第一階項書き換えシステムを拡張した体系における同様な性質についても検討する。また、具体例による実験の準備に取り掛かる。合流性については、束縛変数を伴う高階の書き換えシステムに対する新しい判定条件の提案を検討する。
|
| Causes of Carryover |
新型コロナウイルス感染拡大防止に伴う自粛の要請を受けて出張を控えたことにより、旅費の使用額にずれが生じたため。繰り越し分は次年度の助成金と合わせ研究環境整備に充てる予定である。
|
-
-
[Journal Article] The System SOL version 20202020
Author(s)
Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju
-
Journal Title
Proceedings of the 9th International Workshop on Confluence (IWC 2020)
Volume: －
Pages: 81-81
Open Access / Int'l Joint Research
-
