The Theory of Call-by-Value Solvability (long version)

TL;DR

This paper explores the semantics of call-by-value lambda calculus, comparing it to call-by-name, and shows how solvability concepts can be adapted, revealing differences in the role of unsolvability.

Contribution

It provides a new presentation of call-by-value semantics that recovers properties of solvability known from call-by-name, highlighting fundamental differences.

Findings

CbV solvable terms can be characterized similarly to call-by-name.

Unsolvable terms in CbV do not serve as a notion of meaningless terms.

The role of solvability in CbV differs fundamentally from call-by-name.

Abstract

The denotational semantics of the untyped lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.