Abstract
We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments. Examples of shapely function definitions may be matrix multiplication and the Cartesian product of two lists.
The type checking problem for the type system is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear or monotonic. Furthermore, a method that infers polynomial size dependencies for a non-trivial class of function definitions is suggested.
This research is sponsored by the Netherlands Organisation for Scientific Research (NWO), project Amortized Heap Space Usage Analysis (AHA), grantnr. 612.063.511.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: Quasi-interpretations, a way to control resources. Theoretical Computer Science (to appear)
Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science 6, 579–612 (1996)
Chatterjee, S., Blelloch, G.E., Fischer, A.L.: Size and access inference for data-parallel programs. In: PLDI ’91. Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, pp. 130–144 (1991)
Chui, C., Lai, H.C.: Vandermonde determinant and Lagrange interpolation in R s. Nonlinear and convex analysis, 23–35 ( 1987)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. SIGPLAN Not. 38(1), 185–197 (2003)
Herrmann, C.A., Lengauer, C.: A transformational approach which combines size inference and program optimization. In: Taha, W. (ed.) SAIG 2001. LNCS, vol. 2196, pp. 199–218. Springer, Heidelberg (2001)
Jay, C.B., Sekanina, M.: Shape checking of array programs. In: Computing: the Australasian Theory Seminar, Proceedings. Australian Computer Science Communications, vol. 19, pp. 113–121 (1997)
Pareto, L.: Sized Types. Dissertation for the Licentiate Degree in Computing Science. Chalmers University of Technology (1998)
Lorenz, R.A.: SAFECOMP 1998. Lecture Notes in Math, vol. 1516. Springer, Heidelberg (1992)
Matiyasevich, Y., Jones, J.-P.: Proof or recursive unsolvability of Hilbert’s tenth problem. American Mathematical Monthly 98(10), 689–709 (1991)
Shkaravska, O., van Kesteren, R., van Eekelen, M.: polynomial size analysis of first-order functions. Technical Report ICIS-R07004, Radboud University Nijmegen (2007)
Vasconcelos, P.-B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86–101. Springer, Heidelberg (Revised Papers) (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Shkaravska, O., van Kesteren, R., van Eekelen, M. (2007). Polynomial Size Analysis of First-Order Functions. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)