To prove that a program terminates, one typically finds an invariant that strictly decreases with each executed instruction. In rewriting theory, the program becomes a term, and the invariant a so-called interpretation: a function from the symbols of the rewriting system to some domain. The domain is typically a well-founded totally ordered set, such as the natural numbers. However, well-foundedness is not necessary. For some programs, the most natural invariant takes values in a non-well-founded ordered set such as the real numbers. Finally, Tarski’s decision procedure often makes finding interpretations valued in real numbers the more practical option.

An interpretation of a program automatically provides a bound on its complexity. The original proof of this fact relies on the Archimedean property of natural numbers. The authors prove that the complexity bounds are still induced by interpretations valued in real numbers, by using a result from algebraic geometry about properties of polynomials with real coefficients: the Positivstellensatz, a variation on Hilbert’s famous Nullstellensatz. Using such deep mathematical results is a powerful improvement of the state of the art. The main thesis is illustrated by characterizations of polynomial time and of polynomial space. For example, the authors characterize functions computable in polynomial time as precisely those that can be computed by programs with a real-valued interpretation that is additive--a pleasantly satisfying concrete application of such abstract mathematics.