| 研究課題/領域番号 |
19K11891
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| キーワード | 書き換えシステム / プログラム検証 |
|---|
| 研究実績の概要 |
研究期間の初年度に発表した論文により、帰納的定理の証明手法である潜在帰納法の適用のためには合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。
(1) 前年度に提案した名目書き換えシステムに対する合流性の成立条件を判定するためには、書き換え規則の間の重なりについて調べる必要がある。書き換え規則の間の重なりは、アトム変数を用いた名目単一化によって定義されるため、本年度はその手続きの実装に指導学生とともに取り組んだ。既存研究の手続きではアトム変数への代入が制限されるなど扱いにくい構文が採用されていたため、本研究では手続きで扱う言語の文法を再定義し、各種演算や推論規則についてもそれに伴う変更を行った。また、アトム変数を具体化するアトムの同異による分岐を少なく抑え、なるべく抽象化された状態で手続きを進めることができるよう、新たな規則を多数導入した。このことにより、書き換え規則の間の重なりに関する有用な情報を抽出することができるようになると考えられる。
(2) 局所十分完全性については、前年度に洗練させた十分条件に関する成果を国際会議で発表した。さらに、局所十分完全性の特別な場合（通常の十分完全性を含む）を判定するための導出システムを新たに提案した。この導出システムを用いた手続きは、停止性を持つ項書き換えシステムに対する十分完全性の判定法を自然に拡張したものであり、これにより、停止性を持たない項書き換えシステムに対する既存研究の手法では扱えないいくつかの例について、十分完全性の成立を判定できることを確認した。また、局所十分完全性の特別な場合として、シグネチャ制限による局所十分完全性とソート分割による局所十分完全性について、それぞれに対応する導出システムを用いることにより判定手続きが得られることも示した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムにおける成立条件の判定で必要となる単一化手続きに関する知見が得られた。また、局所十分完全性については、前年度に洗練させた十分条件に関する成果を発表し、さらに、関連する手法に対する調査を進め、導出システムを用いた判定手続きに関する新しい成果も得られた。以上のことから、研究はおおむね順調に進展していると考えられる。
|
| 今後の研究の推進方策 |
合流性については、アトム変数を用いた名目単一化に関して得られた知見をもとに、束縛変数を伴う書き換えシステムに対する判定手続きの構築に取り組む。局所十分完全性については、関連する手法に対する調査を進めるとともに、第一階項書き換えシステムを拡張した体系における同様な性質に関しても検討を行う。以上を含めたこれまでの成果・知見に基づくプログラム検証手法を実際のプログラムの例に適用することにより、その有効性を明らかにする。
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染拡大の影響を受けて出張を控えたことにより、旅費の使用額にずれが生じたため。繰り越し分は次年度の助成金と合わせ、研究環境整備と成果発表のための費用に充てる予定である。
|
