Recently it was shown that it is undecidable whether a term rewrite system can be proved terminating by a polynomial interpretation in the natural numbers. In this paper we show that this is also the case when restricting the interpretations to linear polynomials, as is often done in tools, and when only considering single-rule rewrite systems. What is more, the new undecidability proof is simpler than the previous one. We further show that polynomial termination over the rationals/reals is undecidable.
翻译:近日研究表明,无法判定一个项重写系统能否通过自然数上的多项式解释证明其终止性。本文进一步证明,当限制解释为线性多项式(这在工具中常被采用)且仅考虑单规则重写系统时,该问题同样不可判定。此外,新的不可判定性证明比此前更为简洁。我们还证明了在有理数/实数域上的多项式终止性亦不可判定。