項書換え系における決定可能な必須呼び計算

点击翻译按钮获取中文摘要

本研究プロジェクトの第1段階では,必須呼び計算理論のための新しい枠組を提案した.これは,木オートマトンと基底木変換子を利用し,項書換え系における正規形や根安定形を求めるものである.これまでに知られていた逐次性といく複雑な概念を利用することなく,より大きな書換え系のクラスが決定可能であることを簡潔に証明することに成功した.得られた研究成果は国際会議CAD'97で発表した.プロジェクトの第2段階では,基底木変換子を使うことなく,木オートマトンだけを利用して決定可能性を直接証明できることを示した.これにより,計算量の新たな上限を与えることが可能になった.より詳しく言えば,大山口のNV近似に関して,あるいは,Jacquemardの増大近似に関して,最適正規化簡約戦略が倍指数時間で決定可能であることを証明した.増大近似に関する計算量は,先行研究と比較して著しく改善されている.本研究ではさらに,遅延ナローイング計算系(Lazy Narrowin Calculus, LNCと略す)の推論規則適用時に問題となる非決定性を排除するため,どのような制限を加えればよいかを明らかにした.これにより,LNCの研究は完了したといえる.非決定性を取り除いて得られた計算系LNCdは正交な書換え系において最適性(同じ解を繰り返し計算しなという性質)を持ち,LNCよりも効率的である.LNCやLNCdに関する研究成果は,昨年,学術誌Journal of Symbolic Computationに公表した.また,LNCの条件付き書換え系への拡張であるLCNC計算系に関して,新たな完全性定理を証明し,その結果を国際会議DMTCS/CATS'99において発表した.その他,最近の研究としては,帰納的逐次書換え系と強逐次書換え系とのクラスの等価性を証明し,研究成果をInformation Processing Lettersで公表した.また,合流性や停止性に関連した書換え系の性質の決定不能性についての研究論文を現在投稿中である.この論文は,現在知られる決定不能性の結果をさらに発展させるものである.