Olha Shkaravska ; Marko van Eekelen ; Ron van Kesteren - Polynomial Size Analysis of First-Order Shapely Functions

lmcs:1148 - Logical Methods in Computer Science, May 25, 2009, Volume 5, Issue 2 - https://doi.org/10.2168/LMCS-5(2:10)2009
Polynomial Size Analysis of First-Order Shapely FunctionsArticle

Authors: Olha Shkaravska ; Marko van Eekelen ; Ron van Kesteren

    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 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.


    Volume: Volume 5, Issue 2
    Published on: May 25, 2009
    Imported on: February 29, 2008
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.4.1,F.2.2,D.1.1
    Funding:
      Source : OpenAIRE Graph
    • AHA - Amortized Heap Space Usage Analysis; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.063.511

    11 Documents citing this article

    Consultation statistics

    This page has been seen 1108 times.
    This article's PDF has been downloaded 292 times.