This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear, yielding the LCBV strategy. We then further restrict substitution in LCBV, so that substitution contributes to the progress of the computation. This optimisation is the UCBV strategy, and its notion of substitution is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we show that UCBV is a sound and complete implementation of LCBV, optimised to implement useful evaluation. As a further contribution, we show that an existing notion of usefulness in the literature, namely the GLAMoUr abstract machine, implements the UCBV strategy with polynomial overhead in time. This establishes that UCBV is time-invariant, i.e., that the number of reduction steps to normal form in UCBV can be used as a measure of time complexity. Defining UCBV leads us to the first semantic model of useful CBV evaluation through system U, a non-idempotent intersection type system. Our main result is a characterisation of termination for useful CBV evaluation via system U: a term is typable in system U if and only if it terminates in UCBV. Additionally, system U provides a quantitative interpretation for UCBV, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of UCBV is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for a call-by-value strategy.

Abstract Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. In this work, we define useful call-by-value evaluation inductively, proceeding in two stages. First, we refine the well-known Value Substitution Calculus , so the substitution operation becomes linear , yielding the $$\textsc {lcbv} $$ L C B V calculus. The two calculi are observationally equivalent. We then further refine $$\textsc {lcbv} $$ L C B V by restricting linear substitution only when it contributes to the progress of the computation, yielding the $$\textsc {ucbv} $$ U C B V strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we formally show that the resulting $$\textsc {ucbv} $$ U C B V is a sound and complete implementation of $$\textsc {lcbv} $$ L C B V , optimised to implement useful evaluation. As a further contribution, we show that the $$\textsc {ucbv} $$ U C B V strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that $$\textsc {ucbv} $$ U C B V is time-invariant , i.e. , that the number of reduction steps to normal form in $$\textsc {ucbv} $$ U C B V can be used as a measure of time complexity. Our $$\textsc {ucbv} $$ U C B V strategy is part of the preliminary work required to develop semantic interpretations of useful evaluation, for which its inductive formulation is more suitable than the (non-inductive) existing ones.

Intersection type systems have been independently applied to different evaluation strate- gies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together, without making use of an encoding into a common target framework. This work proposes an intersection type system for a specific notion of evaluation for PCF, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV- like behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the reduction sequences to normal form. This first type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.