項書換え系(TRS)とは書換え規則の集合で定義され、与えられた項において 書換え規則にマッチする部分項を右辺で置き換えることを計算の基本ステップと する計算モデルである。このTRSについては定理の自動証明や代数的仕様記述 などに広く利用され、解析技法などに関してこれまでに多くの 理論的成果が得ら れている。これらの成果を活用し、新たな解析アルゴリズムを開発するための枠組 としてメタ項書換え計算(MRC)が提案されている。MRCはTRSの記述・実行を直接的 に表現できるだけではなく、TRSの解析、生成、変換等のアルゴリズムの記述・実行 が可能である。さらに、等式論理における帰納推論の自動化、項書換え系の等価性証明 の自動化への応用が示されている。
本研究では、MRCプログラム開発環境としてデバッグ機能を持つMRCインタプリタの提案、
設計、実現を行なう。
デバッガを設計する上でシングルステップの単位(イベント)を決定することは最も重要である。
一般的なプログラム言語のデバッガでは関数定義や条件分岐等、ソースコード上
の場所にイベントを設定する。一方、 MRCデバッガでは文脈に対してその位置で
有効な規則集合を求め、その規則集合を用いて書換えを行なことに注目して、
イベントを書換えと文脈の移動に設定する。なぜなら、MRCプログラムでは書換え
規則を自分自身の中に持ち、その規則によって自分自身を書き換える。
したがって関数定義や条件分岐等が記されているコードが書き換わる場合もあり、
ソースコード上にイベントを設定することができないからである。また、
書換え時のイベントをマッチング成功時とマッチング失敗時に設定する。
つまり、リデックスの探索のためのメタ項上の移動に対してイベントを設定する。
また、デバッガの重要な機能の一つにブレークポイントがあげられる。ブレーク
ポイントはイベント上に設定し、プログラムの実行を中断させるものであるが、
一般的なデバッガではイベントはソースコード上に設定されるので、ブレークポ
イントもやはりソースコード上に設定される。MRCデバッガではイベントはリデッ
クスの探索のためのメタ項上の移動と文脈の移動という二つの手続きのうちどち
らかがメタ項上で移動したときに設定されているとみることができる。したがっ
てブレークポイントはメタ項の部分項に対して設定される。
このようなアイディアをもとにしてMRCデバッガの設計を行ない、
デバッグ機能を持つMRCインタプリタを実現する。