Decomposable Termination of Composable Term Rewriting Systems


IEICE TRANSACTIONS on Information and Systems   Vol.E78-D    No.4    pp.314-320
Publication Date: 1995/04/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Algorithm and Computational Complexity
term rewriting system,  termination,  modularity,  algebraic specification,  automated reasoning,  

Full Text: PDF>>
Buy this Article

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 R1, R-1 are composable, terminating term rewriting systems such that their union is nonterminating then for some a {1, -1}, Ra OR is nonterminating and R-aRa 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.