# call-by-value

## call-by-value

(CBV) An evaluation strategy where arguments are evaluated before the function or procedure is entered. Only the values of the arguments are passed and changes to the arguments within the called procedure have no effect on the actual arguments as seen by the caller. See applicative order reduction, call-by-value-result, strict evaluation, call-by-name, lazy evaluation.
References in periodicals archive ?
We use as our source language Moggi's computational lambda calculus, which is an extension of Plotkin's call-by-value calculus.
Our source calculus is the computational calculus, [Lambda.sub.c], of Moggi , which extends the call-by-value lambda calculus, [Lambda.sub.v], of Plotkin .
Further, we show for the first time that Moggi's computational lambda calculus [Lambda.sub.c], actually has computational content, and therefore might serve as an improvement over Plotkin's call-by-value lambda calculus [Lambda.sub.v].
Plotkin  showed, among other things, that the call-by-value CPS translation was sound but not complete, in that it preserves but does not reflect equalities.
A baker's dozen of years later, Moggi  showed, among other things, that the call-by-value monad translation is both sound and complete, in that it preserves and reflects equalities.
Let us review the traditional translation from the call-by-value calculus into the monad calculus, and see why it fails to be a reflection.
Plotkin's call-by-value calculus [Lambda.sub.Nu] is summarized in Figure 3.
while if L is not a value then the equivalence does not hold in the call-by-value calculus.
This provides an analogue of Plotkin's indifference property, which states that call-by-value and call-by-name evaluation yield the same result for terms in CPS.
which is not provable in the call-by-value calculus if L is not a value.
 were concerned with a similar problem: finding translations between call-by-value calculi and linear calculi that are both sound and complete.
 attempted to add the ([Eta].v) rule to the call-by-value calculus, and the ([Eta].-o) and ([Eta].!) rules to the linear lambda calculus, they noted that the translation from the call-by-value calculus to the linear calculus does not preserve ([Eta].v).

Site: Follow: Share:
Open / Close