|
項書き換えシステムの基底合流性は，項書き換えシステムに基づくソフトウェア検証法を構築する上で基礎となる性質である．項書き換えシステムにおいてよく解析手法の研究が進んでいる性質に合流性があるが，基底合流性の解析は，一般的に，データ構造に関する帰納法を用いて合流性を推論する必要があるため，通常の合流性の解析よりはるかに困難である．このため，従来，基底合流性は合流性で近似されることが多く，理論的な解明もあまり進んでいなかった．本研究では，まず，同様にデータ構造に関する帰納法が必要な帰納的定理証明に用いられる書き換え帰納法に着目し，書き換え帰納法において，束縛的変換可能性を保証すれば，基底合流性が成立することを見出した．そして，束縛的変換可能性を保証するような書き換え帰納法を設計して，その理論的な正当性の証明を与えた．次に，提案手法に基づく基底合流性自動証明ツールAGCPの構築するとともに，実験的な評価にも取り組んだ．次に，さまざまな実験に基づき，書き換え規則の変換に基づく適切な関数定義の補完手法，順序付け不能な構成子規則を扱うための推論規則の拡張，基底合流性の反証法などの改良や拡張を考案した．そして，これらを組み込むことにより，基底合流性自動証明ツールの改良を行なった．以上により，従来ほとんど研究の進んでいなかった，項書き換えシステムの基底合流性について，その自動証明法の基礎理論を与えるとともに，その理論に基づく強力な基底合流性自動証明ツールを構築することができた．また，これらの結果を第1回，第2回国際会議FSCDで報告した．また，第6回合流性競技会にて基底合流性カテゴリを新規に創設するとともに，基底合流性自動証明ツールAGCPにより第1位を獲得した．
|
