Real or natural numbers interpretations and their effect on complexity

International audienceInterpretation methods have been introduced in the 70’s byLankford in rewriting theory to prove termination. Actually, as shown byBonfante et al., they provide some good tools to prove the complexity ofprograms. However, such an analysis depends deeply on the archimedeanproperty of natural numbers. This is in contradiction with the fact thatfinding an interpretation can be solved by Tarski’s decision procedure(as described by Dershowitz), and consequently interpretations areusually chosen over the reals rather than over the integers. Doing so,one cannot use anymore the (good) properties of the natural(welordering of N used to bound the complexity of programs. We provethat one may benefit from the best of both worlds: the complexityanalysis still holds even with real numbers. The reason lies in a deepalgebraic property of polynomials over the reals. We illustrate this bytwo characterizations, one of polynomial time and one of polynomial space