自然数、有理数和实数上的多项式解释再探
计算机科学中的逻辑
2015-07-01 v2
摘要
多项式解释是证明项重写系统终止性的一种有用技术。它们有多种形式：具有实数、有理数和整数系数的多项式解释。关于它们在终止性证明能力方面的关系，Lucas 在 2006 年证明了存在某些重写系统，可以用具有实（代数）系数的多项式解释证明其多项式终止，但不能仅用具有有理系数的多项式证明。他还证明了关于使用有理系数与整数系数的相应陈述。在本文中，我们扩展了这些结果，从而给出了上述多项式解释变体之间关系的完整图景。特别是，我们证明了具有实数或有理数系数的多项式解释并不包含具有整数系数的多项式解释。我们的结果也适用于具有多项式解释的增量终止性证明。
引用
@article{arxiv.1407.0406,
title = {Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited},
author = {Friedrich Neurauter and Aart Middeldorp},
journal= {arXiv preprint arXiv:1407.0406},
year = {2015}
}
备注
28 pages; special issue of RTA 2010