本研究の目的は、項書換え系の変換アルゴリズムをＭＲＣにより記述し、 ＭＲＣをＴＲＳのメタ計算に応用する際の長所、短所を洗い出し、評価することであ る。 具体的に記述するのは、 文脈依存ＴＲＳの停止性を証明する技法で使われるＴＲＳ変換アルゴリズムである。
文脈依存ＴＲＳとは、 すべての関数の引数の位置についてリダクションが 許されるかどうかを指定し、その許されない位置において 書換えを制限することで書換え過程を制御できるＴＲＳである。 文脈依存ＴＲＳは、それを停止性に関しては同値な従来の項書換え系に変換し、 変換後のＴＲＳの停止性を証明することで停止性を示す方法が知られている。
文脈依存ＴＲＳを通常のＴＲＳへ変換するアルゴリズムで中心的な役割を 果たすのは、写像Φ、Ｂａｒ、τである。Φは項が与えられたとき、書換えが 許されない部分項の先頭の関数記号に印をつける。Ｂａｒは文脈依存ＴＲＳの 関数記号の集合が与えられたとき、次のようなＴＲＳを構成する。そのＴＲＳは 印のない関数記号がいつでも印のある関数記号に変われるようにし、かつ、 特別な関数記号ａが印を消去する働きをするように定義する。 τは規則の右辺にある変数ｘが、左辺で書換えが許可されない部分項に 含まれる変数の集合の中にある場合、ａ(ｘ)を代入をする。 このような写像をＭＲＣで記述し、 文脈依存ＴＲＳをＴＲＳへ変換するアルゴリズムを実現した。 この実現において、Φ、Ｂａｒ、τのような関数記号、項、規則を 扱う写像をＭＲＣで記述することは比較的容易である。 しかし、これらの写像の適用順序を制御するには工夫が必要である。 すなわち、処理の状況を表すデータを常に保持するようなデータ構造を用意し、 それによって処理の手順を制御するようにした。