表明付き項書き換え系A-TRS : リダクション戦略の表明  [in Japanese] A-TRS : An annotated Term Rewriting System : Annotations for redunction strategies  [in Japanese]

項書き換え系(TRS)は,それをプログラミング言語としてみると,記述の容易さ,意味の把握のしやすさ等優れた言語である。また,仕様としてみると,すべての関数の実現を行わなくとも,実現されていない関数を単なる記号として扱うことにより実行することができる実行可能仕様でもある。TRSにおける書き換えを行うシステム(reducer)の実現に当たっては,正規化戦略の実現のみでなく速度も要求される。この2つは,互いに排反する条件であり,速度向上のため正規化戦略を実現しない方法もある。このように従来の処理系は正しさか,速度のいずれかを犠牲にすることにより他方の利点を導入し作成されてきた。しかしTRSをプログラミング言語として有効に使用するためには,双方とも満足のゆく処理系が必要である。そのためには単一の戦略を用いるのではなく,それぞれのTRSプログラムに応じた戦略を用いることが有効である。すなわち,各TRSプログラム中に,そのTRSプログラムを有効に使うための戦略を定められることが望ましい。それによりユーザーが意図した通りに,書き換えが有効に行なわれるTRSプログラムを作成する事ができる。本論文では,TRSプログラム中に傷に戦略を表明する事が出来る項書き換え系A-TRSを提案する。