{'fraction_non_alphanumeric': 0.05444512221071596, 'fraction_numerical': 0.023250535514164526, 'mean_word_length': 3.670642019479229, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 104, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 148, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and integer coefficients. As to their relationship with respect to termination proving power, Lucas managed to prove in 2006 that there are rewrite systems that can be shown polynomially terminating by polynomial interpretations with real (algebraic) coefficients, but cannot be shown polynomially terminating using polynomials with rational coefficients only. He also proved the corresponding statement regarding the use of rational coefficients versus integer coefficients. In this article we extend these results, thereby giving the full picture of the relationship between the aforementioned variants of polynomial interpretations. In particular, we show that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients. Our results hold also for incremental termination proofs with polynomial interpretations.


Introduction
Polynomial interpretations are a simple yet useful technique for proving termination of term rewrite systems (TRSs, for short). While originally conceived in the late seventies by Lankford [11] as a means for establishing direct termination proofs, polynomial interpretations are nowadays often used in the context of the dependency pair (DP) framework [1,7,8].
In the classical approach of Lankford, one considers polynomials with integer coefficients inducing polynomial algebras over the well-founded domain of the natural numbers. To be precise, every n-ary function symbol f is interpreted by a polynomial P f in n indeterminates with integer coefficients, which induces a mapping or interpretation from terms to integer numbers in the obvious way. In order to conclude termination of a given TRS, three conditions have to be satisfied. First, every polynomial must be well-defined, i.e., it must induce a well-defined polynomial function f N : N n → N over the natural numbers. In addition, the interpretation functions f N are required to be strictly monotone in all arguments. Finally, 2 F. NEURAUTER AND A. MIDDELDORP terminating TRSs one has to show compatibility of the interpretation with the given TRS. More precisely, for every rewrite rule ℓ → r, the polynomial P ℓ associated with the left-hand side must be greater than P r , the corresponding polynomial of the right-hand side, i.e., P ℓ > P r for all values of the indeterminates. Already back in the seventies, an alternative approach using polynomials with real coefficients instead of integers was proposed by Dershowitz [5]. However, as the real numbers R equipped with the standard order > R are not well-founded, a subterm property is explicitly required to ensure well-foundedness. It was not until 2005 that this limitation was overcome, when Lucas [13] presented a framework for proving polynomial termination over the real numbers, where well-foundedness is basically achieved by replacing > R with a new ordering > R,δ requiring comparisons between terms to not be below a given positive real number δ. Moreover, this framework also facilitates polynomial interpretations over the rational numbers.
Thus, one can distinguish three variants of polynomial interpretations, polynomial interpretations with real, rational and integer coefficients, and the obvious question is: what is their relationship with regard to termination proving power? For Knuth-Bendix orders it is known [10,12] that extending the range of the underlying weight function from natural numbers to non-negative reals does not result in an increase in termination proving power. In 2006 Lucas [14] proved that there are TRSs that can be shown polynomially terminating by polynomial interpretations with rational coefficients, but cannot be shown polynomially terminating using polynomials with integer coefficients only. Likewise, he proved that there are TRSs that can be handled by polynomial interpretations with real (algebraic) coefficients, but cannot be handled by polynomial interpretations with rational coefficients.
In this article we extend these results and give a complete comparison between the various notions of polynomial termination. 1 In general, the situation turns out to be as depicted in Figure 1, which illustrates both our results and the earlier results of Lucas [14]. In particular, we prove that polynomial interpretations with real coefficients subsume polynomial interpretations with rational coefficients. Moreover, we show that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients by exhibiting the TRS R 1 in Section 4. Likewise, we prove that there are TRSs that can be shown terminating by polynomial interpretations with real coefficients as well as by polynomial interpretations with integer coefficients, but cannot be shown terminating using polynomials with rational coefficients only, by exhibiting the TRS R 2 in Section 5. The TRSs R 3 and R 4 can be found in Section 6.
The remainder of this article is organized as follows. In Section 2, we introduce some preliminary definitions and terminology concerning polynomials and polynomial interpretations. In Section 3, we show that polynomial interpretations with real coefficients subsume polynomial interpretations with rational coefficients. We further show that for polynomial interpretations over the reals, it suffices to consider real algebraic numbers as interpretation domain. Section 4 is dedicated to showing that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients. Then, in Section 5, we present a TRS that can be handled by a polynomial interpretation with real coefficients as well as by a polynomial interpretation with integer coefficients, but cannot be handled using polynomials with rational coefficients. In Section 6, we show that the relationships in Figure 1 remain true if incremental termination proofs with polynomial interpretations are considered. We conclude in Section 7.
This paper is an extended version of [17], which contained the result of Section 4. The results in Sections 3, 5 and 6 are new.

Preliminaries
As usual, we denote by N, Z, Q and R the sets of natural, integer, rational and real numbers, respectively. An irrational number is a real number, which is not in Q. Given some D ∈ {N, Z, Q, R} and m ∈ D, > D denotes the standard order of the respective domain and D m := {x ∈ D | x m}. A sequence of real numbers (x n ) n∈N converges to the limit x if for every real number ε > 0 there exists a natural number N such that the absolute distance |x n − x| is less than ε for all n > N ; we denote this by lim n→∞ x n = x. As convergence in R k is equivalent to componentwise convergence, we use the same notation also for limits of converging sequences of vectors of real numbers ( x n ∈ R k ) n∈N . A real function f : R k → R is continuous in R k if for every converging sequence ( x n ∈ R k ) n∈N it holds that lim n→∞ f ( x n ) = f (lim n→∞ x n ). Finally, as Q is dense in R, every real number is a rational number or the limit of a converging sequence of rational numbers.
Polynomials. For any ring R (e.g. Z, Q, R), we denote the associated polynomial ring in n indeterminates x 1 , . . . , x n by R[x 1 , . . . , x n ], the elements of which are finite sums of products of the form c · x i 1 1 x i 2 2 · · · x in n , where the coefficient c is an element of R and the exponents i 1 , . . . , i n in the monomial x i 1 1 x i 2 2 · · · x in n are non-negative integers. If c = 0, we call a product c · x i 1 1 x i 2 2 · · · x in n a term. The degree of a monomial is just the sum of its exponents, and the degree of a term is the degree of its monomial. An element P ∈ R[x 1 , . . . , x n ] is called an (n-variate) polynomial with coefficients in R. For example, the polynomial 2x 2 − x + 1 is an element of Z[x], the ring of all univariate polynomials with integer coefficients.
In the special case n = 1, a polynomial P ∈ R[x] can be written as follows: . For the largest k such that a k = 0, we call a k x k the leading term of P , a k its leading coefficient and k its degree, which we denote by deg(P ) = k. A polynomial P ∈ R[x] is said to be linear if deg(P ) = 1, and quadratic if deg(P ) = 2.
Polynomial Interpretations. We assume familiarity with the basics of term rewriting and polynomial interpretations (e.g. [2,18]). The key concept for establishing (direct) termination of TRSs via polynomial interpretations is the notion of well-founded monotone algebras as they induce reduction orders on terms.
Definition 2.1. Let F be a signature, i.e., a set of function symbols equipped with fixed arities. An F-algebra A consists if a non-empty carrier set A and a collection of interpretation functions f A : A n → A for each n-ary function symbol f ∈ F. The evaluation or interpretation [α] A (t) of a term t ∈ T (F, V) with respect to a variable assignment α : V → A is inductively defined as follows: for all a 1 , . . . , a n , b ∈ A. It is said to be monotone with respect to ⊐ if it is monotone in all its arguments. We define s In order to pave the way for incremental polynomial termination in Section 6, the following definition is more general than what is needed for direct termination proofs.
Definition 2.2. Let (A, >, ) be an F-algebra together with two binary relations > and on A. We say that (A, >, ) and a TRS R are (weakly) compatible if ℓ > A r (ℓ A r) for each rewrite rule ℓ → r ∈ R. An interpretation function f A is called strictly (weakly) monotone if it is monotone with respect to > ( ). The triple (A, >, ) (or just A if > and are clear from the context) is a weakly (strictly) monotone F-algebra if > is well-founded, > · ⊆ > and for each f ∈ F, f A is weakly (strictly) monotone. It is said to be an extended monotone F-algebra if it is both weakly monotone and strictly monotone. Finally, we call (A, >, ) a well-founded monotone A-algebra if > is a well-founded order on A, is its reflexive closure, and each interpretation function is strictly monotone.
It is well-known that well-founded monotone algebras provide a complete characterization of termination. Definition 2.4. A polynomial interpretation over N for a signature F consists of a polynomial f N ∈ Z[x 1 , . . . , x n ] for every n-ary function symbol f ∈ F such that for all f ∈ F the following two properties are satisfied: (1) well-definedness: f N (x 1 , . . . , x n ) ∈ N for all x 1 , . . . , x n ∈ N, (2) strict monotonicity of f N in all arguments with respect to > N , the standard order on N. Due to well-definedness, each of the polynomials f N induces a function from N n to N. Hence, the pair N = (N, {f N } f ∈F ) constitutes an F-algebra over the carrier N. Now (N , > N , N ) where N is the reflexive closure of > N constitutes a well-founded monotone algebra, and we say that a polynomial interpretation over N is compatible with a TRS R if the wellfounded monotone algebra (N , > N , N ) is compatible with R. Finally, a TRS is polynomially terminating over N if it admits a compatible polynomial interpretation over N.
In the sequel, we often identify a polynomial interpretation with its associated Falgebra.
Remark 2.5. In principle, one could take any set N m (or even Z m ) instead of N as the carrier for polynomial interpretations. However, it is well-known [18,4] that all these sets are order-isomorphic to N and hence do not change the class of polynomially terminating TRSs. In other words, a TRS R is polynomially terminating over N if and only if it is polynomially terminating over N m . Thus, we can restrict to N as carrier without loss of generality.
The following simple criterion for strict monotonicity of a univariate quadratic polynomial will be used in Sections 4 and 5.
Lemma 2.6. The quadratic polynomial f N (x) = ax 2 + bx + c with a, b, c ∈ Z is strictly monotone and well-defined if and only if a > 0, c 0, and a + b > 0. Now if one wants to extend the notion of polynomial interpretations to the rational or real numbers, the main problem one is confronted with is the non-well-foundedness of these domains with respect to the standard orders > Q and > R . In [9,13], this problem is overcome by replacing these orders with new non-total orders > R,δ and > Q,δ , the first of which is defined as follows: given some fixed positive real number δ, Analogously, one defines > Q,δ on Q. Thus, > R,δ (> Q,δ ) is well-founded on subsets of R (Q) that are bounded from below. Therefore, any set R m (Q m ) could be used as carrier for polynomial interpretations over R (Q). However, without loss of generality we may restrict to R 0 (Q 0 ) because the main argument of Remark 2.5 also applies to polynomials over R (Q), as is already mentioned in [13].
Definition 2.7. A polynomial interpretation over R for a signature F consists of a polynomial f R ∈ R[x 1 , . . . , x n ] for every n-ary function symbol f ∈ F and some positive real number δ > 0 such that f R is well-defined over R 0 , i.e., f R (x 1 , . . . , x n ) ∈ R 0 for all x 1 , . . . , x n ∈ R 0 .
Analogously, one defines polynomial interpretations over Q by the obvious adaptation of the definition above. Let D ∈ {Q, R}. As for polynomial interpretations over N, the pair D = (D 0 , {f D } f ∈F ) constitutes an F-algebra over the carrier D 0 due to the well-definedness of all interpretation functions. Together with > D 0 ,δ and D 0 , the restrictions of > D,δ and D to D 0 , we obtain an algebra (D, Hence, if for each f ∈ F, f D is weakly (strictly) monotone, that is, monotone with respect to D 0 (> D 0 ,δ ), then (D, > D 0 ,δ , D 0 ) is a weakly (strictly) monotone F-algebra. However, unlike for polynomial interpretations over N, strict monotonicity of (D, > D 0 ,δ , D 0 ) does not entail weak monotonicity as it can very well be the case that an interpretation function is monotone with respect to > D 0 ,δ but not with respect to D 0 . Definition 2.8. Let D ∈ {Q, R}. A polynomial interpretation over D is said to be weakly (strictly) monotone if the algebra (D, > D 0 ,δ , D 0 ) is weakly (strictly) monotone. Similarly, we say that a polynomial interpretation over D is (weakly) compatible with a TRS R if the algebra (D, > D 0 ,δ , D 0 ) is (weakly) compatible with R. Finally, a TRS R is polynomially terminating over D if there exists a polynomial interpretation over D that is both compatible with R and strictly monotone.
We conclude this section with a more useful characterization of monotonicity with respect to the orders > R 0 ,δ and > Q 0 ,δ than the one obtained by specializing Definition 2.2. To this end, we note that a function f : R n 0 → R 0 is strictly monotone in its i-th argument with respect to > R 0 ,δ if and only if f (x 1 , . . . , x i + h, . . . , x n ) − f (x 1 , . . . , x i , . . . , x n ) R δ for all x 1 , . . . , x n , h ∈ R 0 with h R δ. From this and from the analogous characterization of > Q 0 ,δ -monotonicity, it is easy to derive the following lemmata, which will be used in Sections 5 and 6. Lemma 2.9. For D ∈ {Q, R} and δ ∈ D 0 with δ > 0, the linear polynomial f D (x 1 , . . . , x n ) = a n x n + · · · + a 1 x 1 + a 0 in D[x 1 , . . . , x n ] is monotone in all arguments with respect to > D 0 ,δ and well-defined if and only if a 0 0 and a i 1 for all i ∈ {1, . . . , n}. In the remainder of this article we will sometimes use the term "polynomial interpretations with integer coefficients" as a synonym for polynomial interpretations over N. Likewise, the term "polynomial interpretations with real (rational) coefficients" refers to polynomial interpretations over R (Q).
Remark 2.11. Lucas [14,15] considers a different definition of polynomial termination over R (Q). He allows an arbitrary subset A ⊆ R (A ⊆ Q) as interpretation domain, provided it is bounded from below and unbounded from above. The definition of well-definedness is modified accordingly. According to his definition, polynomial termination over N trivially implies polynomial interpretations over R (and Q) since one can take A = N ⊆ R and δ = 1, in which case the induced order > A,δ is the same as the standard order on N. Our definitions are based on the understanding that the interpretation domain together with the underlying order determine whether one speaks of polynomial interpretations over the reals, rationals, or integers. As a consequence, several of the new results obtained in this paper do not hold in the setting of [14,15].

Polynomial Termination over the Reals vs. the Rationals
In this section we show that polynomial termination over Q implies polynomial termination over R. The proof is based upon the fact that polynomials induce continuous functions, whose behavior at irrational points is completely defined by the values they take at rational points.
Proof. Let x = (x 1 , . . . , x k ) ∈ R k 0 and let ( x n ) n∈N be a sequence of vectors of non-negative rational numbers x n ∈ Q k 0 whose limit is x. Such a sequence exists because Q k is dense in R k . Then by continuity of f . Thus, f ( x) is the limit of (f ( x n )) n∈N , which is a sequence of non-negative real numbers by assumption. Hence, f ( x) is non-negative, too.
Theorem 3.2. If a TRS is polynomially terminating over Q, then it is also polynomially terminating over R.
Proof. Let R be a TRS over the signature F that is polynomially terminating over Q. So there exists some polynomial interpretation I over Q consisting of a positive rational number δ and a polynomial f Q ∈ Q[x 1 , . . . , x n ] for every n-ary function symbol f ∈ F such that: (1) for all n-ary f ∈ F, f Q (x 1 , . . . , x n ) 0 for all x 1 , . . . , x n ∈ Q 0 , (2) for all f ∈ F, f Q is strictly monotone with respect to > Q 0 ,δ in all arguments, (3) for every rewrite rule ℓ → r ∈ R, P ℓ > Q 0 ,δ P r for all x 1 , . . . , x m ∈ Q 0 . Here P ℓ (P r ) denotes the polynomial associated with ℓ (r) and the variables x 1 , . . . , x m are those occurring in ℓ → r. Next we note that all three conditions are quantified polynomial inequalities of the shape "P (x 1 , . . . , x k ) 0 for all x 1 , . . . , x k ∈ Q 0 " for some polynomial P with rational coefficients. This is easy to see for the first and third condition. As to the second condition, the function f Q is strictly monotone in its i-th argument with respect to > Q 0 ,δ if and only if f Q (x 1 , . . . , for all x 1 , . . . , x n , h ∈ Q 0 . From Lemma 3.1 and the fact that polynomials induce continuous functions we infer that all these polynomial inequalities do not only hold in Q 0 but also in R 0 . Hence, the polynomial interpretation I proves termination over R.

Remark 3.3.
Not only does the result established above show that polynomial termination over Q implies polynomial termination over R, but it even reveals that the same interpretation applies.
We conclude this section by showing that for polynomial interpretations over R it suffices to consider real algebraic 2 numbers as interpretation domain. Concerning the use of real algebraic numbers in polynomial interpretations, in [15,Section 6] it is shown that it suffices to consider polynomials with real algebraic coefficients as interpretations of function symbols. Now the obvious question is whether it is also sufficient to consider only the (non-negative) real algebraic numbers R alg instead of the entire set R of real numbers as interpretation domain. We give an affirmative answer to this question by extending the result of [15]. Proof. Let R be a TRS over the signature F that is polynomially terminating over R. There exists a positive real number δ and a polynomial f R ∈ R[x 1 , . . . , x n ] for every n-ary function symbol f ∈ F such that: for all f ∈ F, f R is strictly monotone with respect to > R 0 ,δ in all arguments, (3) for every rewrite rule ℓ → r ∈ R, P ℓ > R 0 ,δ P r for all x 1 , . . . , x m ∈ R 0 . Next we treat δ as a variable and replace all coefficients of the polynomials in {f R | f ∈ F} by distinct variables c 1 , . . . , c j . Thus, for each n-ary function symbol f ∈ F, its interpretation function is a parametric polynomial f R ∈ Z[x 1 , . . . , x n , c 1 , . . . , c j ] ⊆ Z[x 1 , . . . , x n , c 1 , . . . , c j , δ], where all non-zero coefficients are 1. As a consequence, we claim that all three conditions listed above can be expressed as (conjunctions of) quantified polynomial inequalities of the shape p(x 1 , . . . , x n , c 1 , . . . , c j , δ) 0 for all x 1 , . . . , x n ∈ R 0 (3.1) for some polynomial p ∈ Z[x 1 , . . . , x n , c 1 , . . . , c j , δ]. This is easy to see for the first condition. For the third condition it is a direct consequence of the nature of the interpretation functions and the usual closure properties of polynomials. For the second condition we additionally need the fact that f R is strictly monotone in its i-th argument with respect to Now any of the quantified inequalities (3.1) can readily be expressed as a formula in the language of ordered fields with coefficients in Z, where c 1 , . . . , c j and δ are the only free variables. By taking the conjunction of all these formulas, existentially quantifying δ and adding the conjunct δ > 0, we obtain a formula Φ in the language of ordered fields with free variables c 1 , . . . , c j and coefficients in Z (as R and F are assumed to be finite). By assumption there are coefficients C 1 , . . . , C j ∈ R such that Φ(C 1 , . . . , C j ) is true in R, i.e., there exists a satisfying assignment for Φ in R mapping its free variables c 1 , . . . , c j to C 1 , . . . , C j ∈ R. In order to prove the theorem, we first show that there also exists a satisfying assignment mapping each free variable to a real algebraic number. We reason as follows. Because real closed fields admit quantifier elimination ([3, Theorem 2.77]), there exists a quantifier-free formula Ψ with free variables c 1 , . . . , c j and coefficients in Z that is R-equivalent to Φ, i.e., for all y 1 , . . . , y j ∈ R, Φ(y 1 , . . . , y j ) is true in R if and only if Ψ(y 1 , . . . , y j ) is true in R. Hence, by assumption, Ψ(C 1 , . . . , C j ) is true in R. Therefore, the sentence ∃c 1 · · · ∃c j Ψ is true in R as well. Since both R and R alg are real closed fields with R alg ⊂ R and all coefficients in this sentence are from Z ⊂ R alg , we may apply the Tarski-Seidenberg transfer principle ([3, Theorem 2.80]), from which we infer that this sentence is true in R if and only if it is true in R alg . So there exists an assignment for Ψ in R alg mapping its free variables c 1 , . . . , c j to C ′ 1 , . . . , C ′ j ∈ R alg such that Ψ(C ′ 1 , . . . , C ′ j ) is true in R alg , and hence also in R as Ψ is a boolean combination of atomic formulas in the variables c 1 , . . . , c j with coefficients in Z. But then Φ(C ′ 1 , . . . , C ′ j ) is true in R as well because of the R-equivalence of Φ and Ψ. Another application of the Tarski-Seidenberg transfer principle reveals that Φ(C ′ 1 , . . . , C ′ j ) is true in R alg , and therefore the TRS R is polynomially terminating over R alg (whose formal definition is the obvious specialization of Definition 2.7). This shows that polynomial termination over R implies polynomial termination over R alg . As the reverse implication can be shown to hold by the same technique, we conclude that polynomial termination over R is equivalent to polynomial termination over R alg .

Polynomial Termination over the Reals vs. the Integers
As far as the relationship of polynomial interpretations with real, rational and integer coefficients with regard to termination proving power is concerned, Lucas [14] managed to prove the following two theorems. 3 Theorem 4.1 (Lucas, 2006). There are TRSs that are polynomially terminating over Q but not over N. (Lucas, 2006). There are TRSs that are polynomially terminating over R but not over Q or N.
Hence, the extension of the coefficient domain from the integers to the rational numbers entails the possibility to prove some TRSs polynomially terminating, which could not be proved polynomially terminating otherwise. Moreover, a similar statement holds for the extension of the coefficient domain from the rational numbers to the real numbers. Based on these results and the fact that we have the strict inclusions Z ⊂ Q ⊂ R, it is tempting to believe that polynomial interpretations with real coefficients properly subsume polynomial interpretations with rational coefficients, which in turn properly subsume polynomial interpretations with integer coefficients. Indeed, the former proposition holds according to Theorem 3.2. However, the latter proposition does not hold, as will be shown in this section. In particular, we present a TRS that can be proved terminating by a polynomial interpretation with integer coefficients, but cannot be proved terminating by a polynomial interpretation over the reals or rationals.

4.1.
Motivation. In order to motivate the construction of this particular TRS, let us first observe that from the viewpoint of number theory there is a fundamental difference between the integers and the real or rational numbers. More precisely, the integers are an example of a discrete domain, whereas both the real and rational numbers are dense 4 domains. In the context of polynomial interpretations, the consequences of this major distinction are best explained by an example. To this end, we consider the polynomial function x → 2x 2 − x depicted in Figure 2 and assume that we want to use it as the interpretation of some unary function symbol. Now the point is that this function is permissible in a polynomial interpretation over N as it is both non-negative and strictly monotone over the natural numbers. However, viewing it as a function over a real (rational) variable, we observe that non-negativity is violated in the open interval (0, 1 2 ) (and monotonicity requires a properly chosen value for δ). Hence, the polynomial function x → 2x 2 − x is not permissible in any polynomial interpretation over R (Q). Thus, the idea is to design a TRS that enforces an interpretation of this shape for some unary function symbol, and the tool that can be used to achieve this is polynomial interpolation. To this end, let us consider the following scenario, which is fundamentally based on the assumption that some unary function symbol f is interpreted by a quadratic polynomial f(x) = ax 2 + bx + c with (unknown) coefficients a, b and c. Then, by polynomial interpolation, these coefficients are uniquely determined by the image of f at three pairwise different locations; in this way the interpolation constraints f(0) = 0, f(1) = 1 and f(2) = 6 enforce the interpretation f(x) = 2x 2 − x. Next we encode these constraints in terms of the TRS R consisting of the following rewrite rules, where s n (x) abbreviates s(s(· · · s n-times (x) · · · )), and consider the following two cases: polynomial interpretations over N on the one hand and polynomial interpretations over R on the other hand.
In the context of polynomial interpretations over N, we observe that if we equip the function symbols s and 0 with the (natural) interpretations s N (x) = x + 1 and 0 N = 0, then the TRS R indeed implements the above interpolation constraints. 5 For example, the which is equivalent to f N (0) = 0 in the domain of the natural numbers. Thus, this interpolation constraint can be expressed by a single rewrite rule, whereas the other two constraints require two rules each. Summing up, by virtue of the method of polynomial interpolation, we have reduced the problem of enforcing a specific interpretation for some unary function symbol to the problem of enforcing natural semantics for the symbols s and 0.
Next we elaborate on the ramifications of considering the TRS R in the context of polynomial interpretations over R. To this end, let us assume that the symbols s and 0 are interpreted by s R (x) = x + s 0 and 0 R = 0, so that s has some kind of successor function semantics. Then the TRS R translates to the following constraints: Basically, this means that these constraints do not uniquely determine the function f R . In other words, the method of polynomial interpolation does not readily apply to the case of polynomial interpretations over R. However, we can make it work. To this end, we observe that if s 0 = δ, then the above system of inequalities actually turns into the following system of equations, which can be viewed as a set of interpolation constraints (parameterized by s 0 ) that uniquely determine f R : Clearly, if s 0 = δ = 1, then the symbol f is fixed to the interpretation 2x 2 − x, as was the case in the context of polynomial interpretations over N (note that in the latter case δ = 1 is 5 In fact, one can even show that s N (x) = x + 1 is sufficient for this purpose. implicit because of the equivalence x > N y ⇐⇒ x N y + 1). Hence, we conclude that once we can manage to design a TRS that enforces s 0 = δ, we can again leverage the method of polynomial interpolation to enforce a specific interpretation for some unary function symbol. Moreover, we remark that the actual value of s 0 is irrelevant for achieving our goal. That is to say that s 0 only serves as a scale factor in the interpolation constraints determining f R . Clearly, if s 0 = 1, then f R is not fixed to the interpretation 2x 2 − x; however, it is still fixed to an interpretation of the same (desired) shape, as will become clear in the proof of Lemma 4.4.

Main Theorem.
In the previous subsection we have presented the basic method that we use in order to show that polynomial interpretations with real or rational coefficients do not properly subsume polynomial interpretations with integer coefficients. The construction presented there was based on several assumptions, the essential ones of which are: (a) The symbol s had to be interpreted by a linear polynomial of the shape x + s 0 . (b) The condition s 0 = δ was required to hold. (c) The function symbol f had to be interpreted by a quadratic polynomial. Now the point is that one can get rid of all these assumptions by adding suitable rewrite rules to the TRS R. The resulting TRS will be referred to as R 1 , and it consists of the rewrite rules given in Table 1. The rewrite rules (4.7) and (4.8) serve the purpose of ensuring the first of the above items. Informally, (4.8) constrains the interpretation of the symbol s to a linear polynomial by simple reasoning about the degrees of the left-and right-hand side polynomials, and (4.7) does the same thing with respect to g. Because both interpretations are linear, compatibility with (4.8) can only be achieved if the leading coefficient of the interpretation of s is one. Concerning item (c) above, we remark that the tricky part is to enforce the upper bound of two on the degree of the polynomial f R that interprets the symbol f. To this end, we make the following observation. If f R is at most quadratic, then the function , for all values of x. This can be encoded in terms of rule (4.12) as soon as the interpretation of h corresponds to addition of two numbers. And this is exactly the purpose of rules (4.9), (4.10) and (4.11). More precisely, by linearity of the interpretation of g, we infer from (4.9) that the interpretation of h must have the linear shape h 2 x+h 1 y +h 0 . Furthermore, compatibility with (4.10) and (4.11) implies h 2 = h 1 = 1 due to item (a) above. Hence, the interpretation of h is x + y + h 0 , and it really models addition of two numbers (modulo adding a constant).
Next we comment on how to enforce the second of the above assumptions. To this end, we remark that the hard part is to enforce the condition s 0 δ. The idea is as follows. First, we consider rule (4.2), observing that if f is interpreted by a quadratic polynomial f R and s by the linear polynomial x + s 0 , then (the interpretation of) its right-hand side will eventually become larger than its left-hand side with growing s 0 , thus violating compatibility. In this way, s 0 is bounded from above, and the faster the growth of f R , the lower the bound. The problem with this statement, however, is that it is only true if f R is fixed (which is a priori not the case); otherwise, for any given value of s 0 , one can always find a quadratic polynomial f R such that compatibility with (4.2) is satisfied. The parabolic curve associated with f R only has to be flat enough. So in order to prevent this, we have to somehow control the growth of f R . Now that is where rule (4.6) comes into play, which basically expresses that if one increases the argument of f R by a certain amount (i.e., 2s 0 ), then the value of the function is guaranteed to increase by a certain minimum amount, too. Thus, this rule establishes a lower bound on the growth of f R . And it turns out that if f R has just the right amount of growth, then we can readily establish the desired upper bound δ for s 0 .
Finally, having presented all the relevant details of our construction, it remains to formally prove our main claim that the TRS R 1 is polynomially terminating over N but not over R or Q. Proof. We consider the following interpretation: Note that the polynomial 2x 2 − x is a permissible interpretation function as it is both nonnegative and strictly monotone over the natural numbers by Lemma 2.6 (cf. Figure 2). The rewrite rules of R 1 are compatible with this interpretation because the resulting inequalities are clearly satisfied for all natural numbers x.
Lemma 4.4. The TRS R 1 is not polynomially terminating over R.
Proof. Let us assume that R 1 is polynomially terminating over R and derive a contradiction. Compatibility with rule (4.8) implies As a consequence, deg(s R (x)) ≤ 1, and because s R and g R must be strictly monotone, we conclude deg(s R (x)) = 1. The same reasoning applied to rule (4.7) yields deg(g R (x)) = 1. Hence, the symbols s and g must be interpreted by linear polynomials. So s R (x) = s 1 x + s 0 and g R (x) = g 1 x + g 0 with s 0 , g 0 ∈ R 0 and, due to Lemma 2.9, s 1 R 1 and g 1 R 1. Then the compatibility constraint imposed by rule (4.8) gives rise to the inequality which must hold for all non-negative real numbers x. This implies the following condition on the respective leading coefficients: g 1 s 1 R s 2 1 g 1 . Because of s 1 R 1 and g 1 R 1, this can only hold if s 1 = 1. Hence, s R (x) = x+s 0 . This result simplifies (4.13) to g 1 s 0 > R 0 ,δ 2s 0 , which implies g 1 s 0 > R 2s 0 . From this, we conclude that s 0 > R 0 and g 1 > R 2.
Now suppose that the function symbol f were also interpreted by a linear polynomial f R . Then we could apply the same reasoning to rule (4.7) because it is structurally equivalent to (4.8), thus inferring g 1 = 1. However, this would contradict g 1 > R 2; therefore, f R cannot be linear.
Next we turn our attention to the rewrite rules (4.9), (4.10) and (4.11). Because g R is linear, compatibility with (4.9) constrains the function h : R 0 → R 0 , x → h R (x, x) to be at most linear. This can only be the case if h R contains no terms of degree two or higher. In other words, h R (x, y) = h 1 · x + h 2 · y + h 0 , where h 0 ∈ R 0 , h 1 R 1 and h 2 R 1 (cf. Lemma 2.9). Because of s R (x) = x + s 0 , compatibility with (4.11) implies h 1 = 1, and compatibility with (4.10) implies h 2 = 1; thus, h R (x, y) = x + y + h 0 .
Using the obtained information in the compatibility constraint associated with rule (4.12), we get , which simplifies to 1 deg(f R (x)) − 1 because s 0 = 0. Consequently, f R must be a quadratic polynomial. Without loss of generality, let f R (x) = ax 2 + bx + c, subject to the constraints: a > R 0 and c R 0 because of non-negativity (for all x ∈ R 0 ), and aδ + b R 1 because f R (δ) > R 0 ,δ f R (0) due to strict monotonicity of f R .
Next we consider the compatibility constraint associated with rule (4.6), from which we deduce an important auxiliary result. After unraveling the definitions of > R 0 ,δ and the interpretation functions, this constraint simplifies to 4as 0 x + 4as 2 0 + 2bs 0 R 2g 1 x + g 1 h 0 + g 0 + h 0 + δ for all x ∈ R 0 , which implies the following condition on the respective leading coefficients: 4as 0 R 2g 1 ; from this and g 1 > R 2, we conclude as 0 > R 1 (4.14) and note that as . Hence, as 0 expresses the change of the slopes of the tangents to f R at the points (0, f R (0)) and ( s 0 2 , f R ( s 0 2 )), and thus (4.14) actually sets a lower bound on the growth of f R . Now let us consider the combined compatibility constraint imposed by the rules (4.2) and (4.4), namely 0 R + 2s 0 > R 0 ,δ f R (s R (0 R )) > R 0 ,δ 0 R , which implies 0 R + 2s 0 R 0 R + 2δ by definition of > R 0 ,δ . Thus, we conclude s 0 R δ. In fact, we even have s 0 = δ, which can be derived from the compatibility constraint of rule (4.2) using the conditions s 0 R δ, 14 F. NEURAUTER AND A. MIDDELDORP aδ + b R 1 and as 0 + b R 1, the combination of the former two conditions: . But because of (4.14) and s 0 R δ, this inequality can only be satisfied if: This result has immediate consequences concerning the interpretation of the constant 0.
To this end, we consider the compatibility constraint of rule (4.10), which simplifies to s 0 R 0 R + h 0 + δ. Because of (4.15) and the fact that 0 R and h 0 must be non-negative, we conclude 0 R = h 0 = 0. Moreover, condition (4.15) is the key to the proof of this lemma. To this end, we consider the compatibility constraints associated with the five rewrite rules (4.1) -(4.5): By definition of > R 0 ,s 0 , these inequalities give rise to the following system of equations: After unraveling the definition of f R and substituting z := as 0 , we get a system of linear equations in the unknowns z, b and c c = 0 z + b = 1 4z + 2b = 6 which has the unique solution z = 2, b = −1 and c = 0. Hence, f R must have the shape f R (x) = ax 2 −x = ax(x− 1 a ) in every compatible polynomial interpretation over R. However, this function is not a permissible interpretation for the function symbol f because it is not non-negative for all x ∈ R 0 . In particular, it is negative in the open interval (0, 1 a ); e.g.
. Hence, R 1 is not compatible with any polynomial interpretation over R. Remark 4.5. In this proof the interpretation of f is fixed to f R (x) = ax 2 − x, which violates well-definedness in R 0 . However, this function is obviously well-defined in R m for a properly chosen negative real number m. So what happens if we take this R m instead of R 0 as the carrier of a polynomial interpretation? To this end, we observe that f R (0) = 0 and f R (δ) = δ(aδ − 1) = δ(as 0 − 1) = δ. Now let us consider some negative real number x 0 ∈ R m . We have f R (x 0 ) > R 0 and thus f R (δ) − f R (x 0 ) < R δ, which means that f R violates monotonicity with respect to the order > Rm,δ .
The previous lemma, together with Theorem 3.2, yields the following corollary.
Corollary 4.6. The TRS R 1 is not polynomially terminating over Q.

POLYNOMIAL INTERPRETATIONS REVISITED 15
Finally, combining the material presented in this section, we establish the following theorem, the main result of this section.
Theorem 4.7. There are TRSs that can be proved polynomially terminating over N, but cannot be proved polynomially terminating over R or Q.
We conclude this section with a remark on the actual choice of the polynomial serving as the interpretation of the function symbol f. Remark 4.8. As explained at the beginning of this section, the TRS R 1 was designed to enforce an interpretation for f, which is permissible in a polynomial interpretation over N but not over R (Q). The interpretation of our choice was the polynomial 2x 2 − x. However, we could have chosen any other polynomial as long as it is well-defined and strictly monotone over N but not over R (Q). The methods introduced in this section are general enough to handle any such polynomial. So the actual choice is not that important.

Polynomial Termination over the Integers and Reals vs. the Rationals
This section is devoted to showing that polynomial termination over N and R does not imply polynomial termination over Q. The proof is constructive, so we give a concrete TRS having the desired properties. In order to motivate the construction underlying this particular system, let us consider the following quantified polynomial inequality where P ∈ Z[a] is a polynomial with integer coefficients, all of whose roots are irrational and which is positive for some non-negative integer value of a. To be concrete, let us take P (a) = a 2 − 2 and try to satisfy ( * ) in N, Q 0 and R 0 , respectively. First, we observe that a := √ 2 is a satisfying assignment in R 0 . Moreover, ( * ) is also satisfiable in N by assigning a := 2, for example, and observing that the polynomial 2x 2 − x is non-negative for all x ∈ N. However, ( * ) cannot be satisfied in Q 0 as non-negativity of 2x 2 − x does not hold for all x ∈ Q 0 and P has no rational roots. To sum up, ( * ) is satisfiable in N and R 0 but not in Q 0 . Thus, the basic idea now is to design a TRS containing some rewrite rule whose compatibility constraint reduces to a polynomial inequality similar in nature to ( * ). To this end, we rewrite the inequality (2x 2 − x) · (a 2 − 2) 0 to because now both the left-and right-hand side can be viewed as a composition of several functions, each of which is strictly monotone and well-defined. In particular, we identify the following constituents: h(x, y) = x + y, r(x) = 2x, p(x) = x 2 and k(x) = a 2 x. Thus, the above inequality can be written in the form h(r(k(p(x))), r(x)) h(r(r(p(x))), k(x)) ( * * ) which can easily be modeled as a rewrite rule. (Note that r(x) is not strictly necessary as r(x) = h(x, x), but it gives rise to a shorter encoding.) And then we also need rewrite rules that enforce the desired interpretations for the function symbols h, r, p and k. For this purpose, we leverage the techniques presented in the previous section, in particular the method of polynomial interpolation. The resulting TRS will be referred to as R 2 , and it consists of the rewrite rules given in Table 2. Each of the blocks serves a specific purpose. The largest block consists of the rules (5.1) -(5.10) and is basically a slightly modified version of the TRS R 1 of Table 1. These rules ensure that the symbol s has the semantics of a successor function x → x + s 0 . Moreover, for any compatible polynomial interpretation over Q (R), it is guaranteed that s 0 is equal to δ, the minimal step width of the order > Q,δ . In Section 4, these conditions were identified as the key requirements for the method of polynomial interpolation to work in this setting. Finally, this block also enforces h(x, y) = x + y. The next block, consisting of the rules (5.11) -(5.14), makes use of polynomial interpolation to achieve r(x) = 2x. Likewise, the block consisting of the rules (5.15) -(5.20) equips the symbol p with the semantics of a squaring function. And the block (5.21) -(5.25) enforces the desired semantics for the symbol k, i.e., a linear function x → k 1 x whose slope k 1 is proportional to the square of the interpretation of the constant a. Finally, the rule (5.26) encodes the main idea presented at the beginning of this section (cf. ( * * )).
Lemma 5.1. The TRS R 2 is polynomially terminating over N and R.
Proof. For polynomial termination over N, the following interpretation applies: Note that the polynomial 3x 2 −2x+1 is a permissible interpretation function by Lemma 2.6. Rule (5.26) gives rise to the constraint which holds for all x ∈ N. For polynomial termination over R, we let δ = 1 but we have to modify the interpretation as 4x 2 − 2x + 1 > R 0 ,δ 0 does not hold for all x ∈ R 0 . Taking a R = √ 2, k R (x) = 2x and the above interpretations for the other function symbols establishes polynomial termination over R. Note that the constraint 4x 2 + 2x + 1 > R 0 ,δ 4x 2 + 2x associated with rule (5.26) trivially holds. Moreover, the functions f R (x) = 3x 2 − 2x + 1 and p R (x) = x 2 are strictly monotone with respect to > R 0 ,δ due to Lemma 2.10.
Lemma 5.2. The TRS R 2 is not polynomially terminating over Q.
Proof. Let us assume that R 2 is polynomially terminating over Q and derive a contradiction. Adapting the reasoning in the proof of Lemma 4.4, we infer from compatibility with the rules (5.1) -(5.9) that s Q (x) = x + s 0 , g Q (x) = g 1 x + g 0 , h Q (x, y) = x + y + h 0 , and f Q (x) = ax 2 + bx + c, subject to the following constraints: Next we consider the compatibility constraints associated with the rules (5.9) and (5.10), from which we deduce an important auxiliary result. Compatibility with rule (5.9) implies the condition g 1 Q 5 on the respective leading coefficients since h Q (x, y) = x + y + h 0 , and compatibility with rule (5.10) simplifies to 4as 0 x + 4as 2 0 + 2bs 0 Q 2g 1 x + g 1 h 0 + g 0 + h 0 + δ for all x ∈ Q 0 , from which we infer 4as 0 Q 2g 1 ; from this and g 1 Q 5, we conclude as 0 > Q 2. Now let us consider the combined compatibility constraint imposed by the rules (5.6) and (5.7), namely 0 Q + 3s 0 > Q 0 ,δ f Q (s Q (0 Q )) > Q 0 ,δ 0 Q + s 0 , which implies 0 Q + 3s 0 Q 0 Q + s 0 + 2δ by definition of > Q 0 ,δ . Thus, we conclude s 0 Q δ. In fact, we even have s 0 = δ, which can be derived from the compatibility constraint of rule (5.6) using the conditions s 0 Q δ, aδ + b Q 1, as 0 + b Q 1, the combination of the former two conditions, and f Q (0 Q ) Q 0 Q + δ, the compatibility constraint of rule (5.5): But since as 0 > Q 2 and s 0 Q δ, this inequality can only hold if This result has immediate consequences concerning the interpretation of the constant 0.
To this end, we consider the compatibility constraint of rule (5.3), which simplifies to s 0 Q 0 Q + h 0 + δ. Because of (5.27) and the fact that 0 Q and h 0 must be non-negative, we conclude 0 Q = h 0 = 0. Moreover, as in the proof of Lemma 4.4, condition (5.27) is the key to the proof of the lemma at hand. To this end, we consider the compatibility constraints associated with the rules (5.15) - (5.19). By definition of > Q 0 ,s 0 , these constraints give rise to the following system of equations: Viewing these equations as polynomial interpolation constraints, we conclude that no linear polynomial can satisfy them (because s 0 = 0). Hence, p Q must at least be quadratic. Moreover, by rule (5.20), p Q is at most quadratic (using the same reasoning as for rule (5.8), cf. the proof of Lemma 4.4). So we let p Q (x) = p 2 x 2 + p 1 x + p 0 in the equations above and infer the (unique) solution p 0 = p 1 = 0 and p 2 s 0 = 1, i.e., p Q (x) = p 2 x 2 with p 2 = 0. Next we consider the compatibility constraints associated with the rules (5.11) -(5.13), from which we deduce the interpolation constraints r Q (0) = 0 and r Q (s 0 ) = 2s 0 . Because g Q is linear, r Q must be linear, too, for compatibility with rule (5.14). Hence, by polynomial interpolation, r Q (x) = 2x. Likewise, k Q must be linear for compatibility with rule (5.24), i.e., k Q (x) = k 1 x + k 0 . In particular, k 0 = 0 due to compatibility with rule (5.21), and then the compatibility constraints associated with rule (5.22) and rule (5.23) yield p 3 2 a 4 Q + 2s 0 − δ Q k 1 p 2 a 2 Q + s 0 Q p 3 2 a 4 Q + δ. But s 0 = δ, hence k 1 p 2 a 2 Q = p 3 2 a 4 Q , and since a Q cannot be zero due to compatibility with rule (5.25), we obtain k 1 = p 2 2 a 2 Q . In other words, k Q (x) = p 2 2 a 2 Q x. Finally, we consider the compatibility constraint associated with rule (5.26), which simplifies to (2p 2 x 2 − x)((p 2 a Q ) 2 − 2) Q 0 for all x ∈ Q 0 . However, this inequality is unsatisfiable as the polynomial 2p 2 x 2 − x is negative for some x ∈ Q 0 and (p 2 a Q ) 2 − 2 cannot be zero because both p 2 and a Q must be rational numbers.
Combining the previous two lemmata, we obtain the main result of this section. Theorem 5.3. There are TRSs that can be proved polynomially terminating over both N and R, but cannot be proved polynomially terminating over Q.

Incremental Polynomial Termination
In this section, we consider the possibility of establishing termination by using polynomial interpretations in an incremental way. In this setting, which goes back to Lankford [11,Example 3], one weakens the compatibility requirement of the interpretation and the TRS R under consideration to P ℓ P r for every rewrite rule ℓ → r of R and P ℓ > δ P r for at least one rewrite rule ℓ → r of R. After removing those rules of R satisfying the second condition, one is free to choose a different interpretation for the remaining rules. This process is repeated until all rewrite rules have been removed. Definition 6.1. For D ∈ {N, Q, R alg , R} and n 1, a TRS R is said to be polynomially terminating over D in n steps if either n = 1 and R is polynomially terminating over D or n > 1 and there exists a polynomial interpretation P over D and a non-empty subset S R such that (1) P is weakly and strictly monotone, (2) R ⊆ P and S ⊆ > P , and (3) R \ S is polynomially terminating over D in n − 1 steps. Furthermore, we call a TRS R incrementally polynomially terminating over D if there exists some n 1, such that R is polynomially terminating over D in n steps.
In Section 6.1 we show that incremental polynomial termination over N and R does not imply incremental polynomial termination over Q. In Section 6.2 we show that incremental polynomial termination over N does not imply incremental polynomial termination over R. Below we show that the TRSs R 1 and R 2 cannot be used for this purpose. We moreover extend Theorems 3.2, 4.1, and 4.2 to incremental polynomial termination. Theorem 6.2. Let D ∈ {N, Q, R alg , R}, and let R be a TRS. If R is incrementally polynomially terminating over D, then it is terminating.
Proof. Note that the polynomial interpretation P in Definition 6.1 is an extended monotone algebra that establishes relative termination of S with respect to R, cf. [6,Theorem 3]. The result follows by an easy induction on the number of steps n in Definition 6.1.
For weak monotonicity of univariate quadratic polynomials we use the following obvious criterion. We give the full picture of the relationship between the three notions of incremental polynomial termination over N, Q and R, showing that it is essentially the same as the one depicted in Figure 1 for direct polynomial termination. However, we have to replace the TRSs R 1 and R 2 as the proofs of Lemmata 4.4 and 5.2 break down if we allow incremental termination proofs. In more detail, the proof of Lemma 4.4 does not extend because the TRS R 1 is incrementally polynomially terminating over Q.
Lemma 6.4. The TRS R 1 is incrementally polynomially terminating over Q.
Proof. This can be seen by considering the interpretation with δ = 1. The rewrite rules of R 1 give rise to the following inequalities: x + 1 Q x x 2 + 5x + 6 Q x 2 + 5x + 5 2 x 2 + 3x + 5 2 Q x 2 + 3x + 2 Removing the rules from R 1 for which the corresponding constraint remains true after strengthening Q to > Q 0 ,δ , leaves us with (4.2), (4.8) and (4.12), which are easily handled, e.g. by the interpretation Similarly, the TRS R 2 of Table 2 can be shown to be incrementally polynomially terminating over Q. The following result strengthens Theorem 4.1.
Theorem 6.5. There are TRSs that are incrementally polynomially terminating over Q but not over N.
Proof. Consider the TRS R 3 consisting of the single rewrite rule It is easy to see that R 3 cannot be polynomially terminating over N. As the notions of polynomial termination and incremental polynomial termination coincide for one-rule TRSs, R 3 is not incrementally polynomially terminating over N.
f(g(x)) → g(g(f(x))) (4.7) g(s(x)) → s(s(g(x))) (4.8) The following interpretation establishes polynomial termination over Q: To this end, we note that the compatibility constraint associated with the single rewrite rule gives rise to the inequality 2 > Q 0 ,1 1, which holds by definition of > Q 0 ,1 . Further note that the interpretation functions are well-defined and monotone with respect to > Q 0 ,1 as a consequence of Lemmata 2.9 and 2.10.
In fact, the TRS R 3 proves the stronger statement that there are TRSs which are polynomially terminating over Q but not incrementally polynomially terminating over N. Our proof is both shorter and simpler than the original proof of Theorem 4.1 in [14, pp. 62-67], but see Remark 2.11.
In analogy to Theorem 3.2, incremental polynomial termination over Q implies incremental polynomial termination over R. Theorem 6.6. If a TRS is incrementally polynomially terminating over Q, then it is also incrementally polynomially terminating over R.
Proof. The proof of Theorem 3.2 can be extended with the following statements, which also follow from Lemma 3.1: (1) weak monotonicity of f Q with respect to Q implies weak monotonicity on R 0 with respect to R , (2) P ℓ Q P r for all x 1 , . . . , x m ∈ Q 0 implies P ℓ R P r for all x 1 , . . . , x m ∈ R 0 . Hence the result follows.
To show that the converse of Theorem 6.6 does not hold, we consider the TRS R 4 consisting of the rewrite rules of Table 3.
Lemma 6.7. The TRS R 4 is polynomially terminating over R.
Proof. We consider the following interpretation: The rewrite rules of R 4 are compatible with this interpretation because the resulting inequalities are clearly satisfied for all x ∈ R 0 .
It remains to show that R 4 is not incrementally polynomially terminating over Q. We also show that it is neither incrementally polynomially terminating over N. But first we present the following auxiliary result on a subset of its rules. Lemma 6.8. Let D ∈ {N, Q, R}, and let P be a strictly monotone polynomial interpretation over D that is weakly compatible with the rules (4.7) -(4.11). Then the interpretations of the symbols s, h and g have the shape where all coefficients are non-negative and g 1 2. Moreover, the interpretation of the symbol f is at least quadratic.
Proof. Let the unary symbols f, g and s be interpreted by non-constant polynomials f D (x), g D (x) and s D (x). (Note that strict monotonicity of P obviously implies these conditions.) Then the degrees of these polynomials must be at least 1, such that weak compatibility with (4.8) implies which simplifies to deg(s D (x)) 1. Hence, we obtain deg(s D (x)) = 1 and, by applying the same reasoning to (4.7), deg(g D (x)) = 1. So the function symbols s and g must be interpreted by linear polynomials s D (x) = s 1 x+s 0 and g D (x) = g 1 x+g 0 , where s 0 , s 1 , g 0 , g 1 ∈ D 0 due to well-definedness over D 0 and s 1 , g 1 > 0 to make them non-constant. Then the weak compatibility constraint imposed by (4.8) gives rise to the inequality which must hold for all x ∈ D 0 . This implies the following condition on the respective leading coefficients: g 1 s 1 s 2 1 g 1 . Due to s 1 , g 1 > 0, this can only hold if s 1 1. Now suppose that the function symbol f were also interpreted by a linear polynomial f D . Then we could apply the same reasoning to the rule (4.7) because it is structurally equivalent to (4.8), thus inferring g 1 1. So f D cannot be linear if g 1 > 1.
Next we consider the rewrite rules (4.9), (4.10) and (4.11). As g D is linear, weak compatibility with (4.9) implies that the function h D (x, x) is at most linear as well. This can only be the case if the interpretation h D is a linear polynomial function h D (x, y) = h 1 x+h 2 y+h 0 , where h 0 , h 1 , h 2 ∈ D 0 due to well-definedness over D 0 . Since s D (x) = s 1 x+s 0 , weak compatibility with (4.11) implies s 1 h 1 , and weak compatibility with (4.10) implies s 1 h 2 . Similarly, we obtain g 1 h 1 + h 2 from weak compatibility with (4.9). Now if s 1 , h 1 , h 2 1, conditions that are implied by strict monotonicity of s D and h D (using Lemma 2.9 for D ∈ {Q, R}), then we obtain s 1 = h 1 = h 2 = 1 and g 1 2, such that F. NEURAUTER AND A. MIDDELDORP with g 1 2, which shows that f D cannot be linear. Due to the fact that all of the above assumptions (on the interpretations of the symbols f, g, h and s) follow from strict monotonicity of P, this concludes the proof.
With the help of this lemma it is easy to show that the TRS R 4 is not incrementally polynomially terminating over Q or N. Lemma 6.9. The TRS R 4 is not incrementally polynomially terminating over Q or N.
Proof. Let D ∈ {N, Q}, and let P be a strictly monotone polynomial interpretation over D that is weakly compatible with R 4 . Then, by Lemma 6.8, the interpretations of the symbols s, h and g have the shape As the interpretations of the symbols s and h are linear, weak compatibility with (6.2) implies that the interpretation of k is at most linear as well. Then, letting k D (x) = k 1 x + k 0 , the weak compatibility constraints associated with (6.1) and (6.2) give rise to the following conditions on the respective leading coefficients: 2 k 2 1 2. Hence, k 1 = √ 2, which is not a rational number. So we conclude that there is no strictly monotone polynomial interpretation over N or Q that is weakly compatible with the TRS R 4 . This implies that R 4 is not incrementally polynomially terminating over N or Q.
Combining Lemmata 6.7 and 6.9, we obtain the following result. Corollary 6.10. There are TRSs that are incrementally polynomially terminating over R but not over Q or N.
As a further consequence of Lemmata 6.7 and 6.9, we see that the TRS R 4 is polynomially terminating over R but not over Q or N, which provides an alternative proof of Theorem 4.2.
6.1. Incremental Polynomial Termination over N and R vs. Q. Next we establish the analogon of Theorem 5.3 in the incremental setting. That is, we show that incremental polynomial termination over N and R does not imply incremental polynomial termination over Q. Again, we give a concrete TRS having the desired properties, but unfortunately, as was already mentioned in the introduction of this section, we cannot reuse the TRS R 2 directly. Nevertheless, we can and do reuse the principle idea underlying the construction of R 2 (cf. ( * * )). However, we use a different method than polynomial interpolation in order to enforce the desired interpretations for the involved function symbols. To this end, let us consider the (auxiliary) TRS S consisting of the rewrite rules given in Table 4. The purpose of this TRS is to equip the symbol s (f) with the semantics of a successor (squaring) function and to ensure that the interpretation of the symbol h corresponds to the addition of two numbers. Besides, this TRS will not only be helpful in this subsection but also in the next one.
Lemma 6.11. Let D ∈ {N, Q, R}, and let P be a strictly monotone polynomial interpretation over D that is weakly compatible with the TRS S. Then where as 0 = 1, g 1 2 and all coefficients are non-negative.
Proof. By Lemma 6.8, the interpretations of the symbols s, h and g have the shape s D (x) = x + s 0 , h D (x, y) = x + y + h 0 and g D (x) = g 1 x + g 0 , where all coefficients are non-negative and g 1 2. Moreover, the interpretation of f is at least quadratic. Applying this partial interpretation in (6.4) and (6.5), we obtain, by weak compatibility, the inequalities which imply k D (x) = 2x + k 0 with k 0 0 (due to well-definedness over D 0 ).
Next we consider the rule (6.7) from which we infer that s D (x) = x because otherwise weak compatibility would be violated; hence, s 0 > 0. Then, by weak compatibility with (6.6), we obtain the inequality Now this can only be the case if deg(k D (x) + h 0 ) deg(f D (x + s 0 ) − f D (x)), which simplifies to 1 deg(f D (x)) − 1 since s 0 = 0 and f D is at least quadratic (hence not constant). Consequently, f D must be a quadratic polynomial function, that is, f D (x) = ax 2 + bx + c with a > 0 (due to well-definedness over D 0 ). Then the inequalities arising from weak compatibility with (6.6) and (6.7) simplify to 2x + k 0 + h 0 D 0 2as 0 x + as 2 0 + bs 0 4as 0 x + 4as 2 0 + 2bs 0 D 0 4x + 3h 0 + k 0 both of which must hold for all x ∈ D 0 . Hence, by looking at the leading coefficients, we infer that as 0 = 1. Furthermore, weak compatibility with (6.8) is satisfied if and only if the inequality 2as 0 x + as 2 0 + bs 0 D 0 0 D + s 0 + h 0 holds for all x ∈ D 0 . For x = 0, and using the condition as 0 = 1, we conclude that bs 0 D 0 0 D + h 0 D 0 0, which implies that b 0 as s 0 > 0.
Using all the information gathered above, the compatibility constraint associated with (6.9) gives rise to the inequality 0 D 0 f D (0 D ) + 2 0 D + bs 0 + h 0 , all of whose summands on the right-hand side are non-negative as b 0 and all interpretation functions must be well-defined over D 0 . Consequently, we must have 0 h(r(q(f(x))), r(x)) → h(r 2 (f(x)), q(x)) (6.13) m → s(0) (6.18) In order to establish the main result of this subsection, we extend the TRS S by the rewrite rules given in Table 5, calling the resulting system R 5 . As in Section 5, each block serves a specific purpose. The one made up of (6.10) -(6.12) enforces the desired semantics for the symbol r, that is, a linear function x → 2x that doubles its input, while the block (6.14) -(6.18) enforces a linear function x → q 1 x for the symbol q whose slope q 1 is proportional to the square of the interpretation of the constant m. Finally, (6.13) encodes the main idea of the construction, as mentioned above.
Lemma 6.12. The TRS R 5 is incrementally polynomially terminating over N and R.
Proof. For incremental polynomial termination over N, we start with the interpretation All interpretation functions are well-defined over N and strictly monotone (i.e., monotone with respect to > N ) as well as weakly monotone (i.e., monotone with respect to N ). Moreover, it is easy to verify that this interpretation is weakly compatible with R 5 . In particular, the rule (6.13) gives rise to the constraint which holds for all x ∈ N. After removing the rules from R 5 for which (strict) compatibility holds, we are left with the rules (6.8), (6.9), (6.12), (6.13) and (6.15) -(6.17), all of which can be handled (that is, removed at once) by the following linear interpretation: For incremental polynomial termination over R, we consider the interpretation which is both weakly and strictly monotone according to Lemmata 2.10 and 6.3. So all interpretation functions are well-defined over R 0 and monotone with respect to > R 0 ,δ and R 0 . Moreover, one easily verifies that this interpretation is weakly compatible with R 5 . In particular, the constraint 4x 2 + 2x R 0 4x 2 + 2x associated with (6.13) trivially holds. After removing the rules from R 5 for which (strict) compatibility holds (i.e., for which the corresponding constraint remains true after strengthening R 0 to > R 0 ,δ ), we are left with (6.8), (6.9), (6.12), (6.13) and (6.15) -(6.18), all of which can be removed at once by the following linear interpretation: Lemma 6.13. The TRS R 5 is not incrementally polynomially terminating over Q.
Proof. Let P be a strictly monotone polynomial interpretation over Q that is weakly compatible with R 5 . According to Lemma 6.11, the symbols 0, s, f, g, h and k are interpreted as follows: where s 0 , g 1 , a > 0 and g 0 , k 0 0.
As the interpretation of k is linear, weak compatibility with the rule (6.10) implies that the interpretation of r is at most linear as well, i.e., r Q (x) = r 1 x + r 0 with r 0 0 and 2 r 1 0. We also have r 1 2 due to weak compatibility with (6.11) and 0 r 0 due to weak compatibility with (6.12); hence, r Q (x) = 2x.
Similarly, by linearity of g Q and weak compatibility with (6.14), the interpretation of q must have the shape q Q (x) = q 1 x + q 0 . Then weak compatibility with (6.15) yields 0 q 0 ; hence, q Q (x) = q 1 x, q 1 0. Next we note that weak compatibility with (6.16) and (6.17) implies that f Q (f Q (m Q )) = q Q (f Q (m Q )), which evaluates to a 3 m 4 Q = a q 1 m 2 Q . From this we infer that q 1 = a 2 m 2 Q as a > 0 and m Q s 0 > 0 due to weak compatibility with (6.18); i.e., q Q (x) = a 2 m 2 Q x. Finally, we consider the weak compatibility constraint associated with (6.13), which simplifies to (2ax 2 − x)((a m Q ) 2 − 2) 0 for all x ∈ Q 0 . However, this inequality is unsatisfiable as the polynomial 2ax 2 − x is negative for some x ∈ Q 0 and (a m Q ) 2 − 2 cannot be zero because both a and m Q must be rational numbers. So we conclude that there is no strictly monotone polynomial interpretation over Q that is weakly compatible with the TRS R 5 . This implies that R 5 is not incrementally polynomially terminating over Q.
Together, Lemma 6.12 and Lemma 6.13 yield the main result of this subsection. Corollary 6.14. There are TRSs that are incrementally polynomially terminating over N and R but not over Q.
6.2. Incremental Polynomial Termination over N vs. R. In this subsection, we show that there are TRSs that are incrementally polynomially terminating over N but not over R. For this purpose, we extend the TRS S of Table 4 by the single rewrite rule f(x) → x and call the resulting system R 6 . Lemma 6.15. The TRS R 6 is incrementally polynomially terminating over N.
Proof. First, we consider the interpretation h N (x, y) = x + y g N (x) = 3x + 5 k N (x) = 2x + 2 which is both weakly and strictly monotone as well as weakly compatible with R 6 . In particular, the constraint x 2 N x associated with f(x) → x holds for all x ∈ N. Removing the rules from R 6 for which (strict) compatibility holds leaves us with the rules (6.8), (6.9) and f(x) → x, which are easily handled, e.g. by the linear interpretation 0 N = 0 s N (x) = 3x + 2 f N (x) = 2x + 1 h N (x, y) = x + y Lemma 6.16. The TRS R 6 is not incrementally polynomially terminating over R or Q.
Proof. Let D ∈ {Q, R}, and let P be a polynomial interpretation over D that is weakly compatible with R 6 , and in which the interpretation of the function symbol f has the shape f D (x) = ax 2 with a > 0. Then the weak compatibility constraint ax 2 D 0 x associated with f(x) → x does not hold for all x ∈ D 0 because the polynomial ax 2 − x = ax x − 1 a is negative in the open interval 0, 1 a . As the above assumption on the interpretation of f follows from Lemma 6.11 if P is strictly monotone, we conclude that there is no strictly monotone polynomial interpretation over R or Q that is weakly compatible with the TRS R 6 . This implies that R 6 is not incrementally polynomially terminating over R or Q.
Together, Lemma 6.15 and Lemma 6.16 yield the main result of this subsection. Corollary 6.17. There are TRSs that are incrementally polynomially terminating over N but not over R or Q.
The results presented in this section can be summarized by stating that the relationships expressed in Figure 1 remain true for incremental polynomial termination, after replacing R 1 by R 6 and R 2 by R 5 .

Concluding Remarks
In this article, we investigated the relationship of polynomial interpretations with real, rational and integer coefficients with respect to termination proving power. In particular, we presented three new results, the first of which shows that polynomial interpretations over the reals subsume polynomial interpretations over the rationals, the second of which shows that polynomial interpretations over the reals or rationals do not properly subsume polynomial interpretations over the integers, a result that comes somewhat unexpected, and the third of which shows that there are TRSs that can be proved terminating by polynomial interpretations over the naturals or the reals but not over the rationals. These results were extended to incremental termination proofs. In [16] it is shown how to adapt the results to the dependency pair framework [7,8].
We conclude this article by reviewing our results in the context of automated termination analysis, where linear polynomial interpretations, i.e., polynomial interpretations with all interpretation functions being linear, play an important role. This naturally raises the question as to what extent the restriction to linear polynomial interpretations influences the hierarchy depicted in Figure 1, and in what follows we shall see that it changes considerably. More precisely, the areas inhabited by the TRSs R 1 and R 2 become empty, such that polynomial termination by a linear polynomial interpretation over N implies polynomial termination by a linear polynomial interpretation over Q, which in turn implies polynomial termination by a linear polynomial interpretation over R. The latter follows directly from Theorem 3.2 and Remark 3.3, whereas the former is shown below.
Lemma 7.1. Polynomial termination by a linear polynomial interpretation over N implies polynomial termination by a linear polynomial interpretation over Q.
Proof. Let R be a TRS that is compatible with a linear polynomial interpretation I over N, where every n-ary function symbol f is associated with a linear polynomial a n x n + · · · + a 1 x 1 + a 0 . We show that the same interpretation also establishes polynomial termination over Q with the value of δ set to one. To this end, we note that in order to guarantee strict monotonicity and well-definedness over N, the coefficients of the respective interpretation functions have to satisfy the following conditions: a 0 0 and a i 1 for all i ∈ {1, . . . , n}. Hence, by Lemma 2.9, we also have well-definedness over Q 0 and strict monotonicity with respect to the order > Q 0 ,1 . (Strict monotonicity also follows from [13,Theorem 2].) Moreover, as R is compatible with I, each rewrite rule ℓ → r ∈ R satisfies P ℓ − P r > N 0 for all x 1 , . . . , x m ∈ N, (7.1) where P ℓ (P r ) denotes the polynomial associated with ℓ (r) and the variables x 1 , . . . , x m are those occurring in ℓ → r. Since linear functions are closed under composition, the polynomial P ℓ − P r is a linear polynomial c m x m + · · · + c 1 x 1 + c 0 , such that (7.1) holds if and only if c 0 1 and c i 0 for all i ∈ {1, . . . , m}. However, then we also have P ℓ − P r > Q 0 ,1 0 for all x 1 , . . . , x m ∈ Q 0 , which shows that R is compatible with the linear polynomial interpretation (I, δ) = (I, 1) over Q.
Hence, linear polynomial interpretations over R subsume linear polynomial interpretations over Q, which in turn subsume linear polynomial interpretations over N, and these subsumptions are proper due to the results of [14], which were obtained using linear polynomial interpretations.