| 研究実績の概要 |
項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である. 本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている．
今年度は，前年度に与えたホーン節帰納的定理の自動証明法の改良に取り組んだ．等式帰納的定理の書き換え帰納法においては，方向付けが可能でない等式についても有界接続性を用いた証明手法により扱いが可能である．ホーン節帰納的定理について，同様の手法が適用できないか検討し，その健全性の証明を与えた．また，アンラベリング法を利用した条件付き項書き換えシステムの基底合流性証明システムについて検討した．アンラベリングして得られた項書き換えシステムの基底合流性が，変換前の基底合流性を保証する条件について検討を行った．その結果，ある種の十分完全性が必要となることが判明し，条件付き項書き換えシステムの十分完全性の自動検証法および自動検証システムの構築に取り組んだ．
また，条件付き書き換えシステムの危険対解析について調査を進め，3型指向式条件付き項書き換えシステムの階層合流性を保証する危険対条件を理論的に与えた．また，リストプログラムを対象とした新たな十分完全性の証明手法や，シャロー項書き換えシステムの変換に関する一意正規化可能性の効率的な自動判定手続きを考案した．
|
