関数型言語や項書換え系などの書換えに 基づく計算では、解が存在するにもかかわらず書き換える順序によっては解が得られ ない ことがある。これを解決するために解（正規形）が存在するならそこに 到達することを保証する正規化戦略の研究が進められている。項書換え系において は、まず１９７９年に HuetやLevyらによって正規形でないすべての項は書換えに必要なリデックスをもって おり、 それを繰り返し書き換える戦略が正規化戦略であること を証明した。しかし、この戦略は決定可能でないため、決定可能なクラスである強逐 次性を提案し これが正規化戦略であることを示した。さらに、このクラスは１９９２年に外山に よって重なりのある場合に、 １９９３年に大山口によってNF逐次性に、１９９５年に長谷らによってNVNF逐次性 に、１９９６年に Jacquemardらによってグローイング逐次性に拡張がなされてきた。 また、書換え規則に優先順序が付加された項書換え系は優先順序付き項書換え系と言 われるが、 それについては１９９８年に酒井らによって強逐次性が決定可能な正規化戦略である ことが示された。 これまでに優先順序付き項書換え系については、実際に正規化戦略 に基づいてインデックスを求めるシステムは作成されていない。 本研究では正規化戦略に よる関数型言語の処理系の構築を目的とし、優先順序付き項書換え系の正規化戦略と それに基づくインデックス決定システムを実現・評価する。 優先順序付き項書換え系の書換えは、直感的には複数の書換え規則が同時に同一場所 で 適用可能な場合には優先順序の高い方を適用するというものだが、形式的には規則の 右辺 と優先順序を捨象して定義されるω書換えを 用いて定義される。すなわち、それより上位の規則がこれより先に適用できないこと をω書換え によって確認されたときのみその規則が可能となる。 さらにこれを用いて規則の右辺を捨象して正規化戦略に用いられるΩ書換え が定義される。与えられた項の書換え可能な部分がインデックスであるかどうかの判 定は、 その部分を新しい定数●で置き換えて、それがΩ書換えにより●が消えるかどうかに よって 行われる。これに基づく正規化戦略におけるインデックス決定システム を言語Standard MLを用いて実現し評価する。