本論文の目的は、項書換え系の合流性を証明するシステムの構築で ある。証明手法としては、従来の手法の他に外山によって提案され たラベル付けによる方法を用いた。この方法は、関数記号にラベル を割り当て、項に対してトップダウンにラベルを付けることにより 項書換え系R をラベル付き項書換え系R'に変換する方法である。新 しく得られたR'の導出関係は、ラベルを取り除いた項上のR の導出 関係と等しいため、R'の合流性を示すことによって、従来の手法が 適用できなかったR の合流性を証明できる場合がある。しかし、こ れまでにラベルの割当ての自動化手法は考案されていない。
そこで本研究では、与えられた項書換え系に対して順序付きソート 推論を行い、その情報に基づいてラベル割当ての自動化を図る。本 研究における順序付きソート推論は、型の情報を持たない項書換え 系から、それと矛盾しない順序付きシグニチャのうちで最も情報量 の多いシグニチャを、規則の両辺のソートの関係と引数のソートの 関係により自動的に推論する手法である。ラベルの自動割当ては、 そのソート情報に基づき極大のソートを持つ関数記号にそれぞれラベ ルを付けることによって行われる。本論文はこの考え方に基づくソ ート自動推論のアルゴリズムと2種類のラベル自動割り当てアルゴ リズムを提案する。また、この方法に基づいて、従来の合流性判定方 法、ソート推論によるラベル割当て、ラベル付けによる直和分解 の3つのモジュールからなる合流性判定システムを作成した。