The Essense of Useful Evaluation Through Quantitative Types (Extended Version)
<|reference_start|>The Essense of Useful Evaluation Through Quantitative Types (Extended Version): Several evaluation notions for lambda calculus qualify as reasonable cost models according to Slot and van Emde Boas' Invariance Thesis. A notable result achieved by Accattoli and Dal Lago is that leftmost-outermost reduction is reasonable, where the term representation uses sharing and the steps are useful. These results, initially studied in call-by-name, have also been extended to call-by-value. However, the existing formulations of usefulness lack inductive structure, making it challenging in particular to define and reason about type systems on top of the untyped syntax. Additionally, no type-based quantitative interpretations exist for useful evaluation. In this work, we establish the first inductive definition of useful evaluation for open weak call-by-value. This new useful strategy connects to a previous implementation of usefulness through a low-level abstract machine, incurring only in linear time overhead, thus providing a reasonable cost model for open call-by-value implementation. We also propose a semantic interpretation of useful call-by-value using a non-idempotent intersection type system equipped with a notion of tightness. The resulting interpretation is quantitative, i.e. provides exact step-count information for program evaluation. This turns out to be the first semantical interpretation in the literature for a notion of useful evaluation.<|reference_end|>
@article{barenbaum2024the,
    title={The Essense of Useful Evaluation Through Quantitative Types (Extended
  Version)},
    author={Pablo Barenbaum, Delia Kesner, and Mariana Milicich},
    journal={arXiv preprint arXiv:2404.18874},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.18874},
    primaryClass={cs.LO cs.PL}
}