2019 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 |
書き換えシステムに基づく新しいプログラム検証手法を開発することを目的として研究を進めている。本年度の研究では、以下のような成果・知見が得られた。
帰納的定理の証明手法である潜在帰納法では、従来、合流性と十分完全性が条件として必要であると考えられてきた。本研究では、十分完全性を緩和した局所十分完全性に基づく潜在帰納法を提案し、無限リストのような計算が停止しない式を部分的に含むプログラムに対しても適用できるように手法を拡張した。また、類似の考え方を用いることにより、項書き換えシステムの等価変換として実現されるプログラム変換法を拡張し、その正当性を示した。さらに、局所十分完全性を判定する手続きの構築に取り組み、判定のための導出システムや自動判定に適した十分条件を提案した。
以上は第一階項書き換えシステムの場合を対象とした成果であるが、本研究の最終的な目的である高階の関数型プログラムに対する検証手法の開発のため、高階書き換えシステムの研究についても取り組んでいる。本年度は、主に多相型を持つ高階書き換えシステムの合流性の判定条件について、危険対の強交差性に基づく条件など新たな条件についての成果・知見が得られた。ここで得られた危険対や合流性に関する成果・知見は、従来の第一階項書き換えシステムに基づく帰納的定理証明手法である潜在帰納法を、高階関数や多相型を持つ高階書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
|
| 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 |
潜在帰納法に基づく新しいプログラム検証手法を開発するため、局所十分完全性については、提案した判定手続きを洗練し、関連する手法に対して調査を行うとともに、具体例による実験の準備に取り掛かる。また、合流性については、高階書き換えシステムに対する新しい判定条件の提案を検討する。
|
Research Products
(3 results)
