Polynomial Size Analysis of First-Order Shapely Functions
| Autor: | Ron van Kesteren, Olha Shkaravska, Marko van Eekelen |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Polynomial General Computer Science Monotonic function 0102 computer and information sciences 02 engineering and technology Computational Complexity (cs.CC) 01 natural sciences Operational semantics Theoretical Computer Science symbols.namesake 0202 electrical engineering electronic engineering information engineering GeneralLiterature_REFERENCE(e.g. dictionaries encyclopedias glossaries) Mathematics Discrete mathematics D.1.1 F.4.1 F.2.2 020207 software engineering Function (mathematics) Cartesian product Matrix multiplication Logic in Computer Science (cs.LO) Undecidable problem Decidability Computer Science - Computational Complexity 010201 computation theory & mathematics symbols Digital Security |
| Zdroj: | Logical Methods in Computer Science, 5, 1-35 Logical Methods in Computer Science, 5, 2:10, pp. 1-35 |
| ISSN: | 1860-5974 |
| Popis: | 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. Comment: 35 pages, 1 figure |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|