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.

翻译：针对λ演算的若干评估概念，根据Slot和van Emde Boas的不变性论题，可被视为合理的成本模型。Accattoli与Dal Lago取得的一项显著成果是：在最左最外归约具有合理性的前提下，项表示采用共享机制且归约步骤具有有用性。这些最初在按名调用中研究的成果，现已扩展至按值调用。然而，现有有用性表述缺乏归纳结构，尤其难以在无类型语法基础上定义和推理类型系统。此外，尚无基于类型的定量解释可对应有用评估。本研究首次为开放弱按值调用建立了有用评估的归纳定义。该新型有用策略通过底层抽象机与先前的有用性实现关联，仅产生线性时间开销，从而为开放按值调用的实现提供了合理成本模型。我们还利用配备紧致性概念的非幂等交集类型系统，提出有用按值调用的语义解释。该解释具有定量特性，即可为程序评估提供精确的步骤计数信息。这成为文献中首个针对有用评估概念的语义解释。