Article ID Journal Published Year Pages File Type
6876045 Theoretical Computer Science 2015 16 Pages PDF
Abstract
Interpretation methods have been introduced in the 70s by Lankford [1] in rewriting theory to prove termination. Actually, as shown by Bonfante et al. [2], an interpretation of a program induces a bound on its complexity. However, Lankford's original analysis depends deeply on the Archimedean property of natural numbers. This goes against the fact that finding a real interpretation can be solved by Tarski's decision procedure over the reals (as described by Dershowitz in [3]), 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 (well-)ordering of N used to bound the complexity of programs. We prove that one may take 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.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , ,