Exact bounds for acyclic higher-order recursion schemes
| Authors |
|
|---|---|
| Publication date | 01-2023 |
| Journal | Information and Computation |
| Article number | 104982 |
| Volume | Issue number | 290 |
| Number of pages | 15 |
| Organisations |
|
| Abstract | Beckmann [1] derives bounds on the length of reduction chains of classes of simply typed λ-calculus terms which are exact up-to a constant factor in their highest exponent. Afshari et al. [2] obtain similar bounds on acyclic higher-order recursion schemes (HORS) by embedding them in the simply typed λ-calculus and applying Beckmann's result. In this article, we apply Beckmann's proof strategy directly to acyclic HORS, proving exactness of the bounds on reduction chain length and obtaining exact bounds on the size of languages generated by acyclic HORS. |
| Document type | Article |
| Language | English |
| Published at | https://doi.org/10.1016/j.ic.2022.104982 |
| Downloads |
1-s2.0-S0890540122001377-main
(Final published version)
|
| Permalink to this page | |
