合流性に基づく交差式条件付き項書き換えシステムのアンラベリング変換の健全性条件

項書き換えシステム（TRS）は，書き換え規則により計算を行う計算モデルである．より柔軟なモデル化を可能にするために，条件部を書き換え規則に付加することで表現能力を拡張した条件付き項書き換えシステム（CTRS）が考えられている．条件部の判定に到達可能性を用いたCTRSを指向式CTRSといい，条件部の判定に交差性を用いたCTRSを交差式CTRSと呼ぶ．CTRSの解析のために，CTRSからTRSへと変換する手法であるアンラベリング変換(Marchiori, 1996)が提案されている．アンラベリング変換の健全性は，変換により得られたTRSが元のCTRSの計算をどのように保存しているかを示す性質の1つであり，健全性を持つための様々な条件が知られている．アンラベリング変換はCTRSの合流性を解析するのにも有効である．しかし，このためにはただの健全性ではなく，項変換に関する健全性が必要となる．指向式CTRSが正規で合流性を持つ場合，アンラベリング変換は項変換tbに関する健全となることが知られている(Gmeiner and Gramlich, 2010)．また，交差式CTRSについても同様の結果を示すことができる．しかし，この健全性条件は，CTRSの合流性を仮定しているため，CTRSの合流性検証には役立たない．そこで本発表では，交差式CTRSについて，変換後のTRSの合流性を仮定し，そのような場合に成立するアンラベリング変換の項変換tbに関する健全性条件を報告する．

Term rewriting system (TRSs) are a computational model that performs computation by rewrite rules. To enable more flexible modeling, the framework of conditional term rewriting systems (CTRSs) is considered. Oriented CTRSs are CTRSs that uses reachability to determine conditions, and join CTRSs are those that uses joinability instead. To analyse properties of CTRSs, unraveling transformations (Marchiori, 1996), which are tranformations from CTRSs into TRSs, have been proposed. Soundness of a unraveling is a property that reflects how unraveling preserves the computation, and various sufficient criteria for soundness are known. Unraveling is also helpful to analyse confluence of CTRSs. For this purpose, not only the soundness of the unravaling, but the soundness of the unravaling w.r.t. a term transformation is necessary. It is known that, if an oriented CTRS is normal and confluent, then an unraveling is sound w.r.t. the term transformation tb (Gmeiner and Gramlich, 2010); A similar result can be shown for join CTRSs. However, since confluence of CTRSs is presumed, this soundness criteria is not useful for verifying the confluence of CTRSs. In this presentation, we report a soundness condition of a unraveling w.r.t. tb for join CTRSs, under the assumption of confluence of the TRS obtained by unraveling, so that the criteria can be applied to infer the confluence of CTRSs from that of transformed TRSs.