Polynomial Size Analysis of First-Order Shapely Functions

Polynomial Size Analysis of First-Order Shapely Functions,10.2168/LMCS-5(2:10)2009,Logical Methods in Computer Science,Olha Shkaravska,Marko C. J. D.

Polynomial Size Analysis of First-Order Shapely Functions   (Citations: 2)
BibTex | RIS | RefWorks Download
We present a size-aware type system for first-order shapely function defini- tions. 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 defi- nitions may be implementations of matrix multiplication and the Cartesian product of two lists. The type system is proved to be sound w.r.t. the operational semantics of the language. The type checking problem 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, we have shown that the type-inference problem is at least semi-decidable (under this restriction). We have implemented a procedure that combines run-time testing and type-checking to automatically obtain size dependencies. It terminates on total typable function definitions.
Journal: Logical Methods in Computer Science - LMCS , vol. 5, no. 2, pp. 1-35, 2009
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...This work builds on our previous research on size analysis [17], where we studied polynomial dependencies of the sizes of output data structures (e.g...
    • ...Using the result from [5], we have shown how to generate test data for size analysis of functional programs in [17]...
    • ...3.1 LBF Inference: The Basic Method This polynomial interpretation method was already applied to Size Analysis in previous work [17, 18]...

    Olha Shkaravskaet al. Test-based inference of polynomial loop-bound functions

Sort by: