関数型言語の実行では、複数の規則が適用可能な場合に上方に書かれた規則が優先的
に適用される。項書換え系に優先順序を付けたものが優先順序付き項書換え系であ
り、規則の優先順序を考慮した上で関数型プログラムの性質の解析が可能となる。関
数型プログラムでは、計算が停止せず計算結果全体が存在しない場合でも確定した部
分が存在する。これを頭正規形といいそれを求めることは計算結果を求める上で重要
である。それゆえ、項が頭正規形を持つときそこに到達することを保証する頭正規化
戦略の研究が進められている。項書換え系の頭正規化戦略は1997年にDurandらによっ
て示された。Durandらは、頭正規形でない全ての項はそれに到達するために書換えが
必要なリデックス（頭必須リデックス）を持っており、それを繰り返し書き換える頭
必須戦略が頭正規化戦略であることを示した。しかしながら一般的には、リデックス
が頭必須かどうかを決定することは不可能である。なぜなら、書換えの到達可能性が
決定不可能であるからである。Durandらは書換えの近似を導入してこれを解決した。
これにより項書換え系の到達可能性及び頭正規形の集合が決定可能な線形な項書換え
系において頭必須戦略が決定可能であることを示した。
本論文では、優先順序付き項書換え系のリデックスの集合と頭正規形の集合が木
オートマトンで受理できること、また、どの規則も両辺も共通変数を持たない線形な
優先順序付き項書換え系の到達可能性が決定可能であることを示す。また、それらの
結果を用いることにより、Durandらが示した項書換え系の頭必須計算戦略の決定可能
性が優先順序付き項書換え系でも成立することを示す。