2018 Fiscal Year Annual Research Report
Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting Theory
| Project/Area Number |
16K00091
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 書き換えシステム / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
書き換えシステムに基づく新しいプログラム検証手法を開発することを目的として研究を進めている。最終年度である本年度に実施した研究では、以下のような成果が得られた。
(1) 束縛変数を伴う書き換えシステムに対しては、昨年度までの研究により、名目書き換えシステムと関連する体系における合流性の判定条件についての成果・知見が得られている。本年度は、群馬大学の浜名誠氏によって提案された高階の書き換え体系に対する合流性・停止性の自動判定システムであるSOLシステムの開発に携わった。SOLシステムは、本年度開催された国際合流性競技会および国際停止性競技会の高階部門において、最も多くの自動証明数を獲得することができた。この開発を通じて得られた合流性や停止性に関する知見は、従来の第一階項書き換えシステムに基づく帰納的定理証明手法である潜在帰納法および書き換え帰納法を、高階関数や多相型を持つ高階項に対する書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 文脈移動変換と関連する帰納的定理証明の手法に対しては、昨年度までの研究により、十分完全性を持たない書き換えシステムにおける潜在帰納法についての知見が得られている。本年度は、その知見を利用した新しいプログラム検証手法を、無限リストのような計算が停止しない式を部分的に含むプログラム例に適用し、その有効性を確認する調査を行った。この調査では、遅延評価の関数型言語とプログラム変換に精通している芝浦工業大学の篠埜功氏と共同で作業を進めた。また、提案する検証手法を適用する際に必要となる「項に対する十分完全性」を判定する手続きの構築に研究分担者とともに取り組み、第一階項書き換えシステムの場合を対象として判定のための導出システムを考案した。
|
