| 研究概要 |
合流性を満たす高階(無限)項書換えシステムのクラスの拡張・定式化を目標として,左線形かつK-開発閉包な項書換えシステムの合流性の理論的な解析を行った.さらに,項書換えシステムを拡張した無限項書換えシステムの理論的な解析を行った.無限項書換えシステムは,遅延リストやストリームといった仮想的に無限長として見做されるデータを扱う関数型プログラミング言語の計算モデルとして知られている.項書換えシステムにおける停止性に対応する基本的な性質として,無限項書換えシステムにおける強頭部正規化可能性(強収束性)があり,その証明法がZantemaやEndrullisらによって報告されている.また,Endrullisらは無限項書換えシステムの部分クラスであるストリーム項書換えシステムを提案し,ある十分条件のもとでのストリームの生成性判定手続きを報告している.
本年度の具体的な成果は以下のとおりである.
1.強頭部正規化可能性および一般生成性に対する反証手続きを提案した.提案した手続きの基本的なアイデアは,有限表現を持つ無限項である正則項の反例を構成する点にある.
2.反証手続きの正しさを示すとともに,手続きの実装を報告した.実験の結果,自動反証法が従来知られていない例について有効であることを確認した.
本研究は,現在,学術雑誌に投稿中である.
|
