Abstract
We present a new method for inferring complexity properties for imperative programs with bounded loops. The properties handled are: polynomial (or linear) boundedness of computed values, as a function of the input; and similarly for the running time.
It is well known that complexity properties are undecidable for a Turing-complete programming language. Much work in program analysis overcomes this obstacle by relaxing the correctness notion: one does not ask for an algorithm that correctly decides whether the property of interest holds or not, but only for “yes” answers to be sound. In contrast, we reshaped the problem by defining a “core” programming language that is Turing-incomplete, but strong enough to model real programs of interest. For this language, our method is the first to give a certain answer; in other words, our inference is both sound and complete.
The essence of the method is that every command is assigned a “complexity certificate”, which is a concise specification of dependencies of output values on input. These certificates are produced by inference rules that are compositional and efficiently computable. The approach is inspired by previous work by Niggl and Wunderlich and by Jones and Kristiansen, but use a novel, more expressive kind of certificates.
Keywords
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cousot, P.: Abstract interpretation. ACM Computing Surveys 28(2), 324–328 (1996)
Jones, N.D., Kristiansen, L.: The flow of data and the complexity of algorithms. In: Cooper, S.B., Löwe, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol. 3526, pp. 263–274. Springer, Heidelberg (2005)
Jones, N.D., Kristiansen, L.: A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Computational Logic (to appear)
Kristiansen, L., Niggl, K.-H.: On the computational complexity of imperative programming languages. Theor. Comput. Sci. 318(1-2), 139–161 (2004)
Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear/polynomial space for imperative programs. SIAM J. Comput 35(5), 1122–1147 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben-Amram, A.M., Jones, N.D., Kristiansen, L. (2008). Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds) Logic and Theory of Algorithms. CiE 2008. Lecture Notes in Computer Science, vol 5028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69407-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-69407-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69405-2
Online ISBN: 978-3-540-69407-6
eBook Packages: Computer ScienceComputer Science (R0)