Termination of term rewriting: interpretation and type elimination

We investigate proving termination of term rewriting systems by interpretation of terms in a well-founded monotone algebra. The well-known polynomial interpretations can be considered as a particular case in this framework. A classification of types of termination, including simple termination, is proposed based on properties in the semantic level. A transformation on term rewriting systems eliminating distributive rules is introduced. Using this distribution elimination a new termination proof of the system SUBST of Hardin and Laville (1986) is given. This system describes explicit substitution in λ-calculus. Another tool for proving termination is based on introduction and removal of type restrictions. A property of many-sorted term rewriting systems is called persistent if it is not affected by removing the corresponding typing restriction. Persistence turns out to be a generalization of direct sum modularity, but is more powerful for both proving confluence and termination. Termination is proved to be persistent for the class of term rewriting systems for which not both duplicating rules and collapsing rules occur, generalizing a similar result of Rusinowitch for modularity. This result has nice applications, in particular in undecidability proofs.