Using Representation Theorems for Proving Polynomials Non-negative

Abstract

Proving polynomials non-negative when variables range on a subset of numbers (e.g., [0, + ∞ )) is often required in many applications (e.g., in the analysis of program termination). Several representations for univariate polynomials P that are non-negative on [0, + ∞ ) have been investigated. They can often be used to characterize the property, thus providing a method for checking it by trying a match of P against the representation. We introduce a new characterization based on viewing polynomials P as vectors, and find the appropriate polynomial basis in which the non-negativeness of the coordinates representing P in witnesses that P is non-negative on [0, + ∞ ). Matching a polynomial against a representation provides a way to transform universal sentences ∀ x ∈ [0, + ∞ ) P(x) ≥ 0 into a constraint solving problem which can be solved by using efficient methods. We consider different approaches to solve both kind of problems and provide a quantitative evaluation of performance that points to an early result by Pólya and Szegö’s as an appropriate basis for implementations in most cases.

Developed during a sabbatical year at UIUC. Supported by projects NSF CNS 13-19109, MINECO TIN2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and GV BEST/2014/026 and PROMETEO/2011/052.