| 研究実績の概要 |
書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.
本研究は,条件付き項書き換えシステムにおける帰納的定理および基底合流性の自動証明・検証理論の基盤構築および証明・検証ツールの実現を目標としている.
本年度は,前年度に与えたホーン節帰納的定理の改良書き換え帰納法の自動証明手続きを検討し実装システムを構築した。また実装したシステムを用いた計算機実験により、帰納的定理の証明に成功する新たな例を明らかにした。また、条件付き項書き換えシステムの十分完全性の自動検証法および自動検証システムの構築について引き続き研究を進め、異なるアプローチに基づく複数の検証システムを構築し比較実験を行った。
また、可換式条件付き項書き換えシステムの合流性条件について取り組んだ．従来ほとんど知られていなかった2型可換式条件付き項書き換えシステムにおいて合流性を保証する危険対条件を与えるとともに，3型の可換式条件付き項書き換えシステムについて，その合流性の判定を2型可換式条件付き項書き換えシステムに帰着する変換法を考案した．
また，正則項書き換えシステムについて，可換書き換えの特徴的な性質を明らかにするとともに，単一化に関する性質の圏論を用いた一般化を与えた．さらに，フラット項書き換えシステムの正規形に関する性質についての決定不能性を明らかにした．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初考案したホーン節帰納的定理の証明法である書き換え帰納法では,証明する等式が順序付けできない場合には,展開規則が適用できないという欠点を抱えていた.前年度は異なる証明手法を用いることで，その制約を解消した改良書き換え帰納法を考案し，その健全性を証明を与えるところまでは進捗があった．本年度はその改良書き換え帰納法に基づく証明手続きを検討しシステムを実装を実現することが出来た。実装したシステムを用いた計算機実験により，幾つかの新規の例についての自動証明にも成功した．さらに,アンラベリング法を用いた条件付き項書き換えシステムの基底合流性証明システムの実現するための十分完全性については引き続き解決に取り組み，実装システムによる検討を行った．
また，条件付き項書き換えシステムの合流性の危険対解析に必要となる技術的な蓄積について，前年度3型指向式条件付き項書き換えシステムの階層合流性について取り組み成果が得られたところであったが，今年度は可換式条件付き項書き換えシステムについて取り組みを行った．階層合流性についての解決できなかったが，2型システムの合流性については危険対条件を与えることが出来た．3型システムについては直接的な危険対条件は与えることが出来なかったものの，場合によっては2型システムの合流性に帰着することで間接的に合流性を示せる手法を考案することによって，3型可換式条件付き項書き換えシステムの合流性証明手法を構築することができた．
さらに，関連する技術についての研究という点では，正則項書き換えシステムの合流性の基礎的な研究やフラット項書き換えシステムにおける合流性の関連性質の基礎理論についても成果が得られた．これらは条件付き項書き換えシステムの基底合流性解析のための理論基盤にさまざまな側面から資する成果であり,一定の成果が得られたと考えている.
|
