Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.22982 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914058972692480 |
|---|---|
| author | Kahn, David M Hoffmann, Jan Reps, Thomas Grosen, Jessie |
| author_facet | Kahn, David M Hoffmann, Jan Reps, Thomas Grosen, Jessie |
| contents | The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring cost-free types using the current state-of-the-art algorithm is expensive due to recursive dependence on additional cost-free types. Furthermore, that algorithm uses a heuristic only applicable to polynomial cost bounds, and not, e.g., exponential bounds. This paper presents a new approach to these problems by representing the cost-free types of a function in a new way: with a linear map, which can stand for infinitely many cost-free types. Such maps enable an algebraic flavor of reasoning about cost bounds (including non-polynomial bounds) via matrix inequalities. These inequalities can be solved with off-the-shelf linear-programming tools for many programs, so that types can always be efficiently checked and often be efficiently inferred. An experimental evaluation with a prototype implementation shows that-when it is applicable-the inference of linear maps is exponentially more efficient than the state-of-the-art algorithm. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_22982 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Efficient Cost Bounds with Linear Maps Kahn, David M Hoffmann, Jan Reps, Thomas Grosen, Jessie Programming Languages The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring cost-free types using the current state-of-the-art algorithm is expensive due to recursive dependence on additional cost-free types. Furthermore, that algorithm uses a heuristic only applicable to polynomial cost bounds, and not, e.g., exponential bounds. This paper presents a new approach to these problems by representing the cost-free types of a function in a new way: with a linear map, which can stand for infinitely many cost-free types. Such maps enable an algebraic flavor of reasoning about cost bounds (including non-polynomial bounds) via matrix inequalities. These inequalities can be solved with off-the-shelf linear-programming tools for many programs, so that types can always be efficiently checked and often be efficiently inferred. An experimental evaluation with a prototype implementation shows that-when it is applicable-the inference of linear maps is exponentially more efficient than the state-of-the-art algorithm. |
| title | Efficient Cost Bounds with Linear Maps |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.22982 |