2019 Fiscal Year Research-status Report
条件付き項書き換えシステムにおける帰納的定理と基底合流性に関する研究
| Project/Area Number |
18K11158
|
|---|
| Research Institution | Niigata University |
|---|
Principal Investigator |
青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 条件付き項書き換えシステム / ホーン節帰納的定理 / 基底合流性 / 補題生成法 / アンラベリング変換 |
|---|
| Outline of Annual Research Achievements |
項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である. 本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている．
今年度は，前年度に与えたホーン節帰納的定理の自動証明法の改良に取り組んだ．等式帰納的定理の書き換え帰納法においては，方向付けが可能でない等式についても有界接続性を用いた証明手法により扱いが可能である．ホーン節帰納的定理について，同様の手法が適用できないか検討し，その健全性の証明を与えた．また，アンラベリング法を利用した条件付き項書き換えシステムの基底合流性証明システムについて検討した．アンラベリングして得られた項書き換えシステムの基底合流性が，変換前の基底合流性を保証する条件について検討を行った．その結果，ある種の十分完全性が必要となることが判明し，条件付き項書き換えシステムの十分完全性の自動検証法および自動検証システムの構築に取り組んだ．
また，条件付き書き換えシステムの危険対解析について調査を進め，3型指向式条件付き項書き換えシステムの階層合流性を保証する危険対条件を理論的に与えた．また，リストプログラムを対象とした新たな十分完全性の証明手法や，シャロー項書き換えシステムの変換に関する一意正規化可能性の効率的な自動判定手続きを考案した．
|
| 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型指向式条件付き項書き換えシステムの階層合流性やリストプログラムを対象とした新たな十分完全性の証明手法，変換に関する一意正規化可能性の効率的な自動判定手続き，簡約に関する一意正規化可能性の証明法などについて，技術的な蓄積を得ることができた．これらは条件付き項書き換えシステムの基底合流性解析のための理論基盤にさまざまな側面から資する成果であり，一定の成果が得られたと考えている．
|
| Strategy for Future Research Activity |
今後は改良したホーン節帰納的定理の自動証明法の実装およびそれを利用した基底合流性証明システムの実装を進める予定である．基底合流性証明システムの実現には，十分完全性の解析器が必要となるため，その実装も進める予定である．また，3型指向式条件付き項書き換えシステムの階層合流性を保証する危険対条件についても，その自動解析をどのようにするかは完全には解決できておらず，今後，検討を進める必要がある．また，シャロー項書き換えシステムの一意正規化可能性の決定可能性についても，変換に関する一意正規化可能性については満足な解決が得られたが，簡約に関する一意正規化可能性については解決しておらず，調査を進める予定である．そして，規則的な発散系列の生成法や補題の生成法の実験などのためのヒューリスティックスなどについて検討を進める予定である．これらについては，余帰納的定理のための書き換え帰納法や循環証明法との関連も深いことが見えたきため，これらの手法や理論についても調査を進める予定である．
|
