Generating polynomial orderings (Q1318775)

More and more, term rewriting systems (TRSs) are applied in computer science as well as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs. Termination is a key property for computing with TRSs. There are various methods of proving termination of TRSs. Most of these are based on reduction orderings, which are well-founded, compatible with the structure of terms and stable with respect to substitutions. The notion of reduction ordering allows the following characterization of termination of TRSs: A TRS \({\mathcal R}\) terminates iff there exists a reduction ordering \(\succ\) such that \(l\succ r\) for each rule \(l\to r\) of \({\mathcal R}\). Polynomial orderings are special reduction orderings, mapping terms into a well-founded set by attaching monotonic polynomials (so- called interpretations) to operators. One of the main problems concerning polynomial orderings is the choice of adequate interpretations for a given TRS. The object of this paper is to describe an algorithm for finding polynomial interpretations for a given TRS. Based on the algorithm of U. Martin for generating an appropriate Knuth- Bendix ordering, we transform the set of rules into a set of linear inequalities based on the coefficients of the interpretations with respect to common monomials. The class of interpretations is restricted to so-called simple-mixed polynomials which are sufficient in practice. We make use of the simplex method for deciding whether a system of linear inequalities has a solution. Unfortunately, we do not have linear inequalities initially, because there might be sums of products resulting from strictly simple-mixed interpretations. In order to apply the simplex method we approximate more general inequalities to linear ones by (1) transforming the inequalities into inequalities, each side of which represents only one product (using a variant of the arithmetic-mean- geometric-mean inequality and by (2) applying the binary logarithmic function to these products. We have implemented a prototype of this algorithm. The implementation does not require any user interactions. Note that the technique is not a decision procedure (because of the approximation). However, it is very useful in practice as confirmed by the following statistics: We have applied the algorithm to 242 TRSs occurring in the literature (which are all orientable with the help of simple-mixed polynomials). For 228 TRSs (94.2 \%) the method was successful.