Call-by-Value Solvability and Multi Types

TL;DR

This paper characterizes call-by-value solvability through multi types, linking termination with typability in a specialized type system and enabling extraction of bounds on evaluation length and normal form size.

Contribution

It introduces a novel multi type system that precisely characterizes call-by-value solvability and allows extraction of evaluation bounds, extending prior semantic and type-theoretic work.

Findings

Termination of solving strategy corresponds to typability in the multi type system.

Exact bounds on evaluation length can be extracted from the type system.

Normal form size bounds are obtainable using adapted techniques.

Abstract

This paper provides a characterization of call-by-value solvability using call-by-value multi types. Our work is based on Accattoli and Paolini's characterization of call-by-value solvable terms as those terminating with respect to the solving strategy of the value substitution calculus, a refinement of Plotkin's call-by-value $\lambda$-calculus. Here we show that the solving strategy terminates on a term $t$ if and only if $t$ is typable in a certain way in the multi type system induced by Ehrhard's call-by-value relational semantics. Moreover, we show how to extract from the type system exact bounds on the length of the solving evaluation and on the size of its normal form, adapting de Carvalho's technique for call-by-name.