A Sufficient Condition for Termination of Transformations from Equations to Rewrite Rules

項書換え系(TRS)と等式集合から等価なTRSを得る変換手続きが様々な目的で提案されている.これらの手続きを活用するにはその停止性を明らかにすることが必要であるが,これまでに手続きの停止性に関する研究はほとんどなされていない.本稿では,TRSと等式集合の変換手続きに共通する特徴を捉えて,共通して適用できる停止性の十分条件を与える.具体的には,手続きの停止性をナローイング到達可能集合の有限性に帰着させる.そして,等式付き書換え系の等式数削減手続き[10]と正規化手続き[2]について停止性の十分条件を与える.
Several procedures which transform pairs of term rewriting systems (TRSs, for short) and sets of equations into equivalent TRSs have been proposed so far for different purposes. There has been few works on termination of these procedures, while we need some criteria assuring termination in applying them. In this paper, we show a common sufficient condition for the termination of those procedures. We reduce the termination of the procedures to finiteness of sets of narrowing reachable terms. In particular, we discuss sufficient conditions for the termination of the equation elimination procedure [10] and the normalization procedure [2].