Real or natural numbers interpretations and their effect on complexity
Résumé
Interpretation methods have been introduced in the 70’s by
Lankford in rewriting theory to prove termination. Actually, as shown by
Bonfante et al., they provide some good tools to prove the complexity of
programs. However, such an analysis depends deeply on the archimedean
property of natural numbers. This is in contradiction with the fact that
finding an interpretation can be solved by Tarski’s decision procedure
(as described by Dershowitz), and consequently interpretations are
usually 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 prove
that one may benefit from the best of both worlds: the complexity
analysis still holds even with real numbers. The reason lies in a deep
algebraic property of polynomials over the reals. We illustrate this by
two characterizations, one of polynomial time and one of polynomial space.