|
項書換え系の効率の良い簡約を実現するため、決定可能な必須呼び計算の研究を行なった。本研究の成果は、次の通りである。
1.決定可能なルート必須簡約
木のオートマトン理論を必須簡約の決定可能性に応用すつ新たな手法に着目し、研究を進めた。決定手続きの複雑さについては、これまで議論がなされていないため、決定アルゴリズムの複雑さの上限を与えることができなかった。そこで、本研究では、定規形やルート安定形を求めるための必須呼び戦略について、木のオートマトン理論だけに基づく新たな決定手続きを開発し、複雑さの上限を与えることに成功した。また、すでに複雑さの知られている強逐次性やNV逐次性との比較を行なった。現在、これら複雑さに関する研究成果の論文を執筆中である。
2.項書換えにおける型付け
項書換え系の性質の照明を容易にするための型付け手法がすでに知られているが、本研究ではこの研究を拡張し、さらに難しい場合である等式系付き書換え系へ適用できるようにした。この結果の応用として、AC停止性の決定不能性を導くことができる。Yaroslavlで開催されたLFCS'97では、この成果についての研究発表を行なっている。
3.条件付き項書換え系の論理性
条件付き項書換え系が論理性を持つとは、対応する等式系と論理的強さが等価なことをいう。本研究では、すでに知られている論理性に関する性質をまとめ、書換え系の重要なクラスである定向条件付き書換え系の論理性を保証するような新たな十分条件を提示した。Lilleにおいて開催されたCAAP'97において、この研究成果の発表を行なった。
|
