Decomposable Termination of Composable Term Rewriting Systems

概要

論文の詳細を見る
We extend the theorem of Gramlich on modular termination of term rewriting systems, by relaxing the disjointness condition and introducing the composability instead. More precisely, we prove that if R_l, R_<-1> are composable, terminating term rewriting systems such that their union is nonterminating then for some a ∈ {1, -1}, R_a ∪ OR is nonterminating and R_<-a>＼Ra is Fa-lifting. Here, OR is defined to be the special system {or(x, y) → x, or(x, y) → y}, Fa is the set of function symbols associated with Ra, and an Fa -lifting system contains a rule which has either a variable or a symbol from Fa at the leftmost position of its right-hand side. The extended theorem is stronger than the original one in that it relaxed the disjointness and constructor-sharing conditions and allowed the two systems to share defined symbols in common under the restriction of composability. The corollaries of the theorem show several sufficient conditions for decomposability of termination, which are useful for proving termination of term rewriting systems defined by combination of several composable modules.
社団法人電子情報通信学会の論文
1995-04-25