Call-by-value (CBV) refers to a reduction strategy of the λ-calculus in which identifiers must always refer to values.
The usual -reduction for a function applied to an argument is given by
This is referred to as call-by-name reduction, as the bound identifier stands for an arbitrary term .
In CBV we must not substitute an arbitrary term for the identifier . Thus, -reduction is restricted to cases where the argument is already a value:
What a value is depends on our whims!
In terms of Strachey's characteristic domains, CBV corresponds to a situation in which only values are denotable.
CBV reduction is closely related to applicative order reduction, though they are not the same.
A classic paper by Gordon Plotkin [Plotkin 1975] that compares CBN and CBV by establishing simulations of one into the other, using continuations.
Please expand: call-by-push-value.
The term call-by-value seems to have first appeared in the report defining ALGOL 60 [Backus et al 1960].
Here is the exact quote:
4.7.3.1. Value assignment (call by value)
All formal parameters quoted in the value part of the procedure declaration heading are assigned the values (cf. section 2.8. Values and Types) of the corresponding actual parameters, these assignments being considered as being performed explicitly before entering the procedure body. These formal parameters will subsequently be treated as local to the procedure body.
The intuition for the fact values map to variables was made rigorous in the classic paper by Landin on the SECD machine [Landin 1964]. Indeed, environments in the SECD machine are defined as mapping identifiers to values. (Moreover, the word value occurs 43 times in the paper.)
Backus, J. W., F. L. Bauer, J. Green, C. Katz, J. McCarthy, A. J. Perlis, H. Rutishauser, et al. 1960. ‘Report on the Algorithmic Language ALGOL 60’. Edited by Peter Naur. Communications of the ACM 3 (5): 299–314. https://doi.org/10.1145/367236.367262. [pdf]
@article{backus_1960,
title = {Report on the algorithmic language {ALGOL} 60},
volume = {3},
doi = {10.1145/367236.367262},
number = {5},
journal = {Communications of the ACM},
author = {Backus, J. W. and Bauer, F. L. and Green, J. and Katz, C. and McCarthy, J. and Perlis, A. J. and Rutishauser, H. and Samelson, K. and Vauquois, B. and Wegstein, J. H. and van Wijngaarden, A. and Woodger, M.},
editor = {Naur, Peter},
year = {1960},
pages = {299--314},
}
Landin, P. J. 1964. ‘The Mechanical Evaluation of Expressions’. The Computer Journal 6 (4): 308–20. https://doi.org/10.1093/comjnl/6.4.308. [pdf]
@article{landin_mechanical_1964,
title = {The {Mechanical} {Evaluation} of {Expressions}},
volume = {6},
doi = {10.1093/comjnl/6.4.308},
number = {4},
journal = {The Computer Journal},
author = {Landin, P. J.},
year = {1964},
pages = {308--320}
}
Plotkin, G.D. 1975. ‘Call-by-Name, Call-by-Value and the λ-Calculus’. Theoretical Computer Science 1 (2): 125–59. https://doi.org/10.1016/0304-3975(75)90017-1. [pdf]
@article{plotkin_1975,
title = {Call-by-name, call-by-value and the λ-calculus},
volume = {1},
doi = {10.1016/0304-3975(75)90017-1},
number = {2},
journal = {Theoretical Computer Science},
author = {Plotkin, G.D.},
year = {1975},
pages = {125--159}
}