Strong Call-by-Value and Multi Types

TL;DR

This paper establishes a semantic framework for strong call-by-value lambda calculus evaluation using Ehrhard's multi types, showing termination corresponds to typability and analyzing differences with call-by-extended-value.

Contribution

It introduces a typing-based characterization of strong call-by-value evaluation and compares it with call-by-extended-value, revealing their non-equivalence.

Findings

External strategy terminates iff term is typable with shrinking multi types.

External strategy is normalizing in untyped setting.

External divergence does not imply non-termination in call-by-extended-value.

Abstract

This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the lambda-calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard's call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.