Sciweavers

Share
TLCA
2007
Springer

Polynomial Size Analysis of First-Order Functions

10 years 2 months ago
Polynomial Size Analysis of First-Order Functions
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.1
Olha Shkaravska, Ron van Kesteren, Marko C. J. D.
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TLCA
Authors Olha Shkaravska, Ron van Kesteren, Marko C. J. D. van Eekelen
Comments (0)
books