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...
Main Authors: | , |
---|---|
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 |