Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
From MaRDI portal
Publication:2921119
DOI10.2168/LMCS-10(3:22)2014zbMATH Open1342.68181arXiv1407.0406OpenAlexW2011901971MaRDI QIDQ2921119
Aart Middeldorp, Friedrich Neurauter
Publication date: 30 September 2014
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/1407.0406
Uses Software
This page was built for publication: Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2921119)
