TY - GEN
T1 - The Cost of Skeletal Call-By-Need, Smoothly
AU - Accattoli, Beniamino
AU - Magliocca, Francesco
AU - Peyrot, Loïc
AU - Coen, Claudio Sacerdoti
N1 - Publisher Copyright:
© Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen;
PY - 2025/7/7
Y1 - 2025/7/7
N2 - 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.
AB - 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.
KW - abstract machines
KW - call-by-need
KW - cost models
KW - λ-calculus
UR - https://www.scopus.com/pages/publications/105010688204
U2 - 10.4230/LIPIcs.FSCD.2025.5
DO - 10.4230/LIPIcs.FSCD.2025.5
M3 - Conference contribution
AN - SCOPUS:105010688204
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025
A2 - Fernandez, Maribel
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025
Y2 - 14 July 2025 through 20 July 2025
ER -