Polynomial Size Analysis of First-Order Functions

DOI10.1007/978-3-540-73228-0_25zbMATH Open1163.68316arXiv0902.2073OpenAlexW1568405722MaRDI QIDQ3612643FDOQ3612643

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

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Full work available at URL: https://arxiv.org/abs/0902.2073

Recommendations

• Polynomial Size Analysis of First-Order Shapely Functions
• Inferring static non-monotone size-aware types through testing
• Collected size semantics for strict functional programs over general polymorphic lists
• Calculating sized types
• Linear types and non-size-increasing polynomial time computation.

zbMATH Keywords

Diophantine equationstype checkingshapely functionssize analysis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cited In (5)

• Polynomial solutions of algebraic difference equations and homogeneous symmetric polynomials
• Collected size semantics for strict functional programs over general polymorphic lists
• Polynomial Size Analysis of First-Order Shapely Functions
• Calculating sized types
• Inferring static non-monotone size-aware types through testing

This page was built for publication: Polynomial Size Analysis of First-Order Functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612643)