Modular Termination of Term rewriting Systems revisited

We study modularity properties of alien-decreasing rewrite relations, of which shared rewriting is a particular case. We give a new, abstract and elegant proof of modularity of termination of alien-decreasing unions in presence of shared constructors. This abstract proof is reminiscent from Tait's strong normalization proof for the typed lambda calculus. The proof method is robust enough to be then adapted to the case of hierarchical specifications (with shared defined function symbols) for which we give new modularity results.

full paper