項書換え系(TRS)は書換えに基づく関数型言語の計算モデルである。 TRS における重要な問題として、正規化戦略と最適書換え問題がある。正規化 戦略は与えられた項が正規形を持つ場合には必ず正規形、すなわち解に到達す ることを保証する計算の場所を示すものである。一方、最適書換え問題はさら に最小のステップ数の書換えで正規形を得る方法を見つけるものである。本論 文では正規化戦略に関する研究を行う。
項が与えられたとき、正規形を得るために必ずいつかは書換えを行わなければ ならないリデックスを必須リデックスという。Huet と Levy(1979) は必須呼びが直交 TRS での正規化戦略であること を示した。しかし、一般には必須呼びは決定可能ではないため、それを近似し た決定可能な強逐次戦略を提案した。その後、Oyamaguchi(1993) は NV逐次性 を提示し、それが決定可能であることを証明した。 また、H.Comon(1995) は与えられた TRS の逐次性の判定に単項二階論理を 利用した。彼は、述語を木オートマトンで表現し、それを単項二階論理に直すこ とで、述語が決定可能であることを示した。そこでは Rabin(1979)、 Thomas(1990) の結果を用いている。 Nagaya(1999) は Growing TRS が決定可能であることを示した。
これらの戦略は決定可能である。しかし、莫大な計算量が必要であることが知 られているだけであり、それを求めるアルゴリズムの実装はなされていない。 そこで、本論文では、これらの戦略の実装を行いその実用性について評価する。 本システムは、TRS から述語を作成する、述語から論理式に変換する、論理式 の判定を行うというモジュールから構成される。TRS から述語を作成するモジュ ー ルでは、述語を木オートマトンで表現する。任意の項に対して、この述語が成 り立つならば、戦略が決定可能であることが示せる。次に、述語から論理式に 変換を行う部分では、先のモジュールで構成された木オートマトンを単項二階論 理に変換する部分と、この論理式を用いて戦略が決定可能であることを示す論 理式に変換する部分に分かれる。最後に、論理式を判定するモジュールで戦略が 決 定可能であるかを判定する。今回は MONA を使用した。また、本システムでは、 戦略が決定可能であることを判定するだけではなく、決定可能であるときには、 与えられた項の必須リデックスを発見することも可能である。