Fine-grain call-by-value

The fine-grain call-by-value \lambda-calculus (FGCBV) is a version of the call-by-value \lambda-calculus that is useful for studying evaluation order and effects. It was introduced in Levy, Power, and Thielecke 2003.

Rationale

Partially inspired by Moggi's computational lambda calculus and call-by-push-value, FGCBV was introduced to resolve certain difficulties in the theory of the CBV \lambda-calculus:

1. The CBV theory is not purely equational, because the a "is value" predicate (normally written \downarrow) is required.
2. In both application MN and pairs (M, N), the choice that M is evaluated before N is completely arbitrary.
3. Application and pairing are clearly complex constructs, with ad-hoc semantics. For example, the semantics of application MN consist of 3 distinct steps: evaluating M to a \lambda abstraction; evaluating N to a value; and evaluating the body of the abstraction with the value of N substituted for the bound variabe.
4. If we also add effects, then a value (i.e. an effect-free term) has at least two denotations. While they are related, it would be theoretically advantageous if they're different pieces of syntax.

All of these problems were resolved by Moggi's monadic metalanguage, by making everything a value, and enclosing computations in monadic terms. However, that does not have clear operational semantics.

FGCBV combines the advantages of the computational \lambda-calculus with the monadic metalanguage, as it features aspects of both.

Definition

Please expand.

References

• FGCBV was (seemingly independently!) introduced in Søren Lassen's 1998 thesis, and in a Info&Comp 2003 paper:

@phdthesis{lassen_1998,
	title = {Relational {Reasoning} about {Functions} and {Nondeterminism}},
	url = {https://www.brics.dk/DS/98/2/},
	school = {Aarhus University},
	author = {Lassen, Søren Bøgh},
	year = {1998},
	note = {Series: BRICS Dissertation Series},
}

@article{levy_2003,
	title = {Modelling environments in call-by-value programming languages},
	volume = {185},
	doi = {10.1016/S0890-5401(03)00088-9},
	number = {2},
	journal = {Information and Computation},
	author = {Levy, Paul Blain and Power, John and Thielecke, Hayo},
	year = {2003},
	pages = {182--210}
}