Proving termination of (conditional) rewrite systems. A semantic approach (Q1323317)

An important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a rewrite system \(R\), do not suffice for proving termination of \(R\). Indeed sometimes semantic information is needed to orient a rewrite rule. Therefore we integrate a semantic interpretation of rewrite systems and terms into a well-founded ordering on terms: the notion of semantic ordering is the first main contribution of this paper. The use and usefulness of the semantic ordering in proving termination is illustrated by means of some realistic examples. Furthermore, the concept of semantic information induces a novel approach for proving termination in conditional rewrite systems. The idea is to employ not only semantic information contained in the terms that are to be compared, but also extra (semantic) information contained in the premiss of the conditional equation in which the terms appear. This leads to our second contribution in the termination problem area: the notion of contextual ordering and contextual semantic ordering. The contextual approach allows to prove termination of conditional rewrite systems where all classical partial orderings would fail.