Termination of linear rewriting systems

Abstract

Limitations, such as right-linearity, on the form of rules in a term-rewriting system are shown to restrict the class of derivations that must be considered when determining whether or not the system terminates for all inputs. These restricted derivations, termed "chains", are obtained by attempting to apply rules to the final terms of derivations that issue from the left-hand side of rules. Similar limitations are shown to guarantee that combining two terminating systems yields a terminating system.