Beyond Absolute Positiveness for Universally Quantified Non-Linear Polynomial Constraints
2026-06-29 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a way to analyze how certain rewriting systems behave using polynomial interpretations, which assign natural numbers to functions. Usually, checking these interpretations involves solving complex inequalities, and current methods simplify these problems using a rule called absolute positiveness. Their work explores going beyond this rule to find more complex polynomial interpretations that were previously unreachable. This could help better understand or prove properties like termination in these systems.
polynomial interpretationsterm rewrite systemsmonotone algebraswell-founded orderstermination analysisexistential universal inequalitiesabsolute positivenessnon-linear polynomials
Authors
Carsten Fuhs
Abstract
Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for termination analysis and complexity analysis of term rewrite systems. Finding such polynomial interpretations for a given set of term constraints involves solving a set of $\exists\forall$ inequalities over the natural numbers. Conventionally, the absolute positiveness criterion is used to reduce $\exists\forall$ inequalities to $\exists$ inequalities. This extended abstract reports on work in progress to go beyond absolute positiveness, allowing for finding non-linear polynomial interpretations that were outside the reach of existing techniques.