平滑分析骨架式按需调用的开销
计算机科学中的逻辑
2025-09-24 v3
摘要
骨架式按需调用是按需调用求值的一种优化,也称为“完全惰性共享”:当必须复制一个值时,首先将其拆分为随后将被复制的“骨架”,以及保持共享的“血肉”。在此,我们提供对骨架式按需调用的两种开销分析。首先,我们提供一族项,表明骨架式按需调用在时间和空间上都可以比按需调用渐近地快指数倍;据我们所知,这是首个此类证据。其次,我们证明骨架式按需调用可以被高效地实现,即具有双线性开销。这一结果是通过提供 Shivers 和 Wand 关于骨架重构思想的一种新的平滑表示获得的,然后将其平滑地插入到遵循 Accattoli 等人的提纯技术对抽象机的研究中。
引用
@article{arxiv.2505.09242,
title = {The Cost of Skeletal Call-by-Need, Smoothly},
author = {Beniamino Accattoli and Francesco Magliocca and Loïc Peyrot and Claudio Sacerdoti Coen},
journal= {arXiv preprint arXiv:2505.09242},
year = {2025}
}
备注
Version with proof appendix of the FSCD 2025 paper with the same title