A decision procedure for accurate polynomial evaluation

For integer polynomials $p$ with $p(0) = 0$, the paper characterizes the
existence of an accurate evaluation algorithm on $\mathbb{R}^n$ in the model
of finite computation trees with exact real inputs, independently rounded
addition, subtraction and multiplication, exact negation and comparisons,
branching, stored values and no constants. The
characterization uses the finitely many regions determined by input signs and
the ordering of input absolute values. After changing to nonnegative gap
coordinates on each region, accurate evaluability is equivalent to a uniform
bound of the coefficientwise absolute polynomial by the absolute value of the
polynomial itself. Each bound is a first-order sentence over the reals, so
effective real quantifier elimination gives a halting decision procedure. The
necessity argument couples two nearby executions while preserving
error-dependent branches and all stored rounded values; the sufficiency
argument constructs an evaluator using only exact sign and order branching and
rounded evaluation in the gap coordinates.