Call-by-value evaluation precisely measured and linked to program termination
A Quantitative Interpretation of Useful Call-by-Value
Logic in Computer Science
Summary
Some programs stop running (terminate), and others keep going forever. This paper shows a way to tell exactly which programs stop when evaluated with a certain method called useful call-by-value. The authors create a simple system that can count exactly how many steps it takes to run a program using this method. They also prove that different evaluation methods with subtle rules about erasing parts of programs behave the same in terms of whether programs stop or not. This helps us better understand how programs run and when they finish.
What this means in practice
- •For compiler engineers: Use system U to predict which programs terminate and how many steps useful call-by-value evaluation takes during compilation optimization.
- •For program analysis teams: Employ the paper’s equivalence results to compare different evaluation strategies for program termination behavior in static analysis tools.
A theory result. No direct application yet.
Authors
Pablo Barenbaum, Delia Kesner, Mariana Milicich
Abstract
In this work, we present the first semantic interpretation of useful call-by-value evaluation through a non-idempotent intersection type system called U. One first contribution of this paper is a characterisation of termination of useful call-by-value evaluation via U-typability. That is, a term is typable in system U if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system U provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of useful evaluation 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 variables and abstractions in an open call-by-value strategy. Our third contribution is a termination-equivalence result between standard call-by-value, which may perform erasing reductions, and useful call-by-value, which is non-erasing. To establish this result, we introduce a non-erasing restriction of standard call-by-value, a refinement that serves as an intermediate calculus bridging standard and useful call-by-value. We show that all three calculi have the same termination behaviour, and hence induce the same observational equivalence.