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