| 研究概要 |
リダクションの近似の概念をもちいることによって,従来よりもより広いクラスの項書き換えシステムに対して決定可能な必須呼び戦略を明らかにした.決定可能な必須戦略の解析には,これまでも項書き換えシステムのさまざまな近似がもちいられていたが,本研究では従来必要とされていた右線形性の制限を取り除いても,グローイング近似が決定可能な近似であることを示した.ここで提案した左線形グローイング近似をもちいると,弾逐次系,NVNF逐次系,シャロー逐次系,さらに従来の線形グローイング逐次系を含むより広いクラスの項書換え系に対して,決定可能な必須呼び戦略の存在を示すことが可能である.
さらに,ここで得られた左線形グローイング近似に基づいて,項書き換えシステムの計算過程の解析を行った.右基底項書き換えシステムの計算の到達可能性および合流性が決定であることは従来知られていたが,左線形グローイング近似の書き換え規則を逆向きに適用することで,従来の結果が拡張できることを示した.
リダクションの近似に基づく計算の停止性の解析はこれまでほとんど知られていなかった.本研究では,左線形グローイング近似の解析手法を適用することで,準直交項書き換えシステムの停止性の解析を行った.Gramlich(1995)は準直交項書き換えシステムの停止性と弱停止性が等価であることを明らかにしている.この結果を我々が示した左線形グローイング近似の到達可能性の決定性と組み合わせることにより,準直交項書き換えシステムの停止性の判定が決定可能となる十分条件を得ることができた.
|
