2026-08-17T05:10:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23620 2025-10-27T10:30:19Z ddc:004 open_access

The Cost of Skeletal Call-By-Need, Smoothly Accattoli, Beniamino Magliocca, Francesco Peyrot, Loïc Sacerdoti Coen, Claudio λ-calculus abstract machines call-by-need cost models 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Beniamino Accattoli and Francesco Magliocca and Loïc Peyrot and Claudio Sacerdoti Coen 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.5 urn:nbn:de:0030-drops-236206 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.5 eng https://creativecommons.org/licenses/by/4.0/legalcode