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...

Full description

Bibliographic Details
Main Authors: Friedrich Neurauter, Aart Middeldorp
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2014-09-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/853/pdf
_version_ 1797268683570020352
author Friedrich Neurauter
Aart Middeldorp
author_facet Friedrich Neurauter
Aart Middeldorp
author_sort Friedrich Neurauter
collection DOAJ
description 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.
first_indexed 2024-04-25T01:36:23Z
format Article
id doaj.art-30dfb9deaf59481c8062263fd55a7ecb
institution Directory Open Access Journal
issn 1860-5974
language English
last_indexed 2024-04-25T01:36:23Z
publishDate 2014-09-01
publisher Logical Methods in Computer Science e.V.
record_format Article
series Logical Methods in Computer Science
spelling doaj.art-30dfb9deaf59481c8062263fd55a7ecb2024-03-08T09:37:13ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742014-09-01Volume 10, Issue 310.2168/LMCS-10(3:22)2014853Polynomial Interpretations over the Natural, Rational and Real Numbers RevisitedFriedrich NeurauterAart Middeldorphttps://orcid.org/0000-0001-7366-8464Polynomial 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.https://lmcs.episciences.org/853/pdfcomputer science - logic in computer science
spellingShingle Friedrich Neurauter
Aart Middeldorp
Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
Logical Methods in Computer Science
computer science - logic in computer science
title Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
title_full Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
title_fullStr Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
title_full_unstemmed Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
title_short Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
title_sort polynomial interpretations over the natural rational and real numbers revisited
topic computer science - logic in computer science
url https://lmcs.episciences.org/853/pdf
work_keys_str_mv AT friedrichneurauter polynomialinterpretationsoverthenaturalrationalandrealnumbersrevisited
AT aartmiddeldorp polynomialinterpretationsoverthenaturalrationalandrealnumbersrevisited