The Cost of Skeletal Call-by-Need, Smoothly
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866918146105933824 |
|---|---|
| author | Accattoli, Beniamino Magliocca, Francesco Peyrot, Loïc Coen, Claudio Sacerdoti |
| author_facet | Accattoli, Beniamino Magliocca, Francesco Peyrot, Loïc Coen, Claudio Sacerdoti |
| contents | Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared. Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge. Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_09242 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Cost of Skeletal Call-by-Need, Smoothly Accattoli, Beniamino Magliocca, Francesco Peyrot, Loïc Coen, Claudio Sacerdoti Logic in Computer Science F.4.1 Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared. Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge. Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al. |
| title | The Cost of Skeletal Call-by-Need, Smoothly |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2505.09242 |