定理自動証明やソフトウェアの代数的仕様記述などへ広く応用されている
書き換え型計算モデル「項書換え系(TRS)」について、これまでに多くの
理論的成果がえられているが、それらの多くはTRSの処理アルゴリズムであ
る。また、TRSの組み合わせに関する研究も盛んに行われている。
これらの研究成果のを活用するためには、それらを記述する言語,すなわち、TRSのメタ
言語が必要である。また、そのメタ言語で書かれた処理プログラムの解析
も重要であることは言うまでもない。メタ項書換え計算(MRC)は、このよう
な観点から提案された計算モデルである。
計算モデル一般に求められる最も基本的な性質として、計算結果の一意性
を保証する合流性があげられる。合流性は、MRCで記述されたTRSの処理プ
ログラムの解析に役立つと期待される。
本研究では、MRCで記述されたプログラム(以下、MRC項)の合流性について検討し、ある条件を満たす範囲のMRC項に
ついて、その合流性が保証できることを証明した。