2020 Fiscal Year Research-status Report
条件付き項書き換えシステムにおける帰納的定理と基底合流性に関する研究
| Project/Area Number |
18K11158
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | 条件付き項書き換えシステム / ホーン節帰納的定理 / 基底合流性 / 補題生成法 / アンラベリング変換 |
|---|
| Outline of Annual Research Achievements |
書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.
本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている.
本年度は,前年度に与えたホーン節帰納的定理の改良書き換え帰納法の自動証明手続きを検討し実装システムを構築した。また実装したシステムを用いた計算機実験により、帰納的定理の証明に成功する新たな例を明らかにした。また、条件付き項書き換えシステムの十分完全性の自動検証法および自動検証システムの構築について引き続き研究を進め、異なるアプローチに基づく複数の検証システムを構築し比較実験を行った。
また、可換式条件付き項書き換えシステムの合流性条件について取り組んだ．従来ほとんど知られていなかった2型可換式条件付き項書き換えシステムにおいて合流性を保証する危険対条件を与えるとともに，3型の可換式条件付き項書き換えシステムについて，その合流性の判定を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
当初考案したホーン節帰納的定理の証明法である書き換え帰納法では,証明する等式が順序付けできない場合には,展開規則が適用できないという欠点を抱えていた.前年度は異なる証明手法を用いることで，その制約を解消した改良書き換え帰納法を考案し，その健全性を証明を与えるところまでは進捗があった．本年度はその改良書き換え帰納法に基づく証明手続きを検討しシステムを実装を実現することが出来た。実装したシステムを用いた計算機実験により，幾つかの新規の例についての自動証明にも成功した．さらに,アンラベリング法を用いた条件付き項書き換えシステムの基底合流性証明システムの実現するための十分完全性については引き続き解決に取り組み，実装システムによる検討を行った．
また，条件付き項書き換えシステムの合流性の危険対解析に必要となる技術的な蓄積について，前年度3型指向式条件付き項書き換えシステムの階層合流性について取り組み成果が得られたところであったが，今年度は可換式条件付き項書き換えシステムについて取り組みを行った．階層合流性についての解決できなかったが，2型システムの合流性については危険対条件を与えることが出来た．3型システムについては直接的な危険対条件は与えることが出来なかったものの，場合によっては2型システムの合流性に帰着することで間接的に合流性を示せる手法を考案することによって，3型可換式条件付き項書き換えシステムの合流性証明手法を構築することができた．
さらに，関連する技術についての研究という点では，正則項書き換えシステムの合流性の基礎的な研究やフラット項書き換えシステムにおける合流性の関連性質の基礎理論についても成果が得られた．これらは条件付き項書き換えシステムの基底合流性解析のための理論基盤にさまざまな側面から資する成果であり,一定の成果が得られたと考えている.
|
| Strategy for Future Research Activity |
ホーン節帰納的定理のための書き換え帰納法については実装システムを用いた実験により新たな課題を発見することが出来た．これらについては，基本的な書き換え帰納法の枠組みの更なる拡張が必要ではないかと考えているが，そのアイデアは今後の課題である．また，ホーン節帰納的定理証明と十分完全性を組み合わせた基底合流性証明システムの実現については基本的な枠組みの構想は出来たが，十分完全性についてもさまざまな要素技術をどのように組み合わせて効率の良い証明手続きが実現できるかの検討が十分な結論が得られず，これらを組み合わせた基底合流性システムはプロトタイプの構築に留まった．ホーン節帰納的定理証明のための書き換え帰納法についても条件付き項書き換えシステムの十分完全性証明手法についても更なる研究が必要と考えられる．また，合流性に基づく基底合流性証明については，指向式項書き換えシステムや可換式項書き換えシステムについて合流性を保証する危険対条件や変換法を理論的に与えることには成功したが，これらの証明手法の実装手続きや検証システムの実現についてはまだ十分な検討が出来ておらず，今後の検討課題となった．
|
| Causes of Carryover |
コロナ禍により論文出版が遅れたため。論文別刷代として支出予定。
|
