Termination of term rewriting: Interpretation and type elimination (Q1332336)

The paper discusses three techniques for proving termination of rewrite systems: (1) defining reduction orderings by means of semantic interpretations, (2) using a transformation technique called distribution elimination, and (3) refining the term structure by introducing sorts. Ad(1): If \(\succ\) is a reduction ordering and \(\ell \succ r\) for each rule \(\ell \to r\) in the rewrite system \(R\), then \(R\) is terminating. Based on an idea of Lankford, one can define reduction orderings on the set \({\mathcal T} ({\mathcal F}, {\mathcal X})\) of terms by interpreting the function symbols in \({\mathcal F}\) as monotone functions over an ordered set \(({\mathcal A},>)\). The well-known polynomial orderings are constructed this way by using \((\mathbb{N},>)\) as the ordered set. The paper suggests to use other ordered sets \(({\mathcal A},>)\) and discusses in this context simple termination (i.e. using simplification orderings) and total termination (i.e. using total orderings \(>\) on \({\mathcal A})\). Ad(2): An interesting transformation technique is presented which is based on eliminating a function symbol \(a \in {\mathcal F}\): Given a rewrite system \(R\), one may compute the transformed system \(E_ a(R)\) and conclude (simple, total) termination of \(R\) from (simple, total) termination of \(E_ a (R)\). Ad(3): To any many sorted signature \(\text{sig} = (S,F, \tau)\) one may associate the homogeneous signature \(\text{sig}'\) by identifying all sort \(s \in S\). For a rewrite system \(R\) over sig let \(R'\) be the rewrite system over \(\text{sig}'\). A property \(P\) is called persistent if for all \(R\) we have \(P(R)\) iff \(P(R')\). This notion of persistence is a generalization of modularity. Termination is not a persistent property in general. However, it is proved that termination is persistent on the classes of (a) non-collapsing and (b) non-duplicating rewrite systems. The results of the paper may be used to prove termination of rewrite systems over a homogeneous signature by introducing sorts in a suitable way and proving termination over the many sorted signature. The results may also be used to prove undecidability of some termination problems. The paper mainly contains the results of two papers in the Proceedings of CTRS '92, published in LNCS 656.