call-by-need evaluation, when to evaluate arguments?

178 Views Asked by At

I want to know a point about when to evaluate arguments in the call-by-need.

I found some explanations on this link, which has the following description.


Call-by-need is a special type of non-strict evaluation in which unevaluated expressions are represented by suspensions or thunks which are passed into a function unevaluated and only evaluated when needed or forced. When the thunk is forced the representation of the thunk is updated with the computed value and is not recomputed upon further reference.

What is the meaning of "when needed or forced"?

The link also has the descriptions.

For example, the following program will not diverge since the omega combinator passed into the constant function is not used and therefore the argument is not evaluated.

$\omega = (\lambda x . x x) (\lambda x . x x)$

$test = (\lambda y . 4 ) \, \omega$


In an implementation, how do we know when to evaluate $\omega$ if $\omega$ is not evaluated on the $\beta$-reduction of $ (\lambda y . x ) \, \omega$? For me, it should evaluate and update the thunk with the result to be used later.

Let me take an example.

$( \lambda x . \lambda y. y \, x ) (2 + 2) (\lambda x. x + 1)$

=$( \lambda y. y \, A ) (\lambda x. x + 1) $

  where A = (2 + 2)

=$ B \, A $

  where  A = (2 + 2)  and B = ($\lambda x. x + 1$)

is it time to force $A = (2 + 2)$ to be $A = 4$? how about $B$? should be as following?

=$ (\lambda x. x + 1) \, A $

  where \, A = (2 + 2)  and   B = ($\lambda x. x + 1$)

=$ (\lambda x. x + 1) \, 4 $

  where \, A = 4 and B = ($\lambda x. x + 1$) 

=$ 4 + 1$

  where \, A = 4 \, and  \, B = ($\lambda x. x + 1$)  

So, when we should evaluate the argument, such as $A$ in the example?

2

There are 2 best solutions below

3
On BEST ANSWER

In your example $(\lambda y.x)\omega$, the call-by-need evaluation does not need to evaluate $\omega$ because the evaluation of $\omega$ is not needed at all in order to evaluate $(\lambda y.x)\omega$. Indeed, $\lambda y.x$ represents a constant unary function that associates $x$ with any argument, so the evaluation of the argument $\omega$ is superfluous. Call-by-need evaluation is defined in order to avoid this kind of superfluous evaluations. In other words, $(\lambda y.x)\omega$ is normal (no $\beta$-reduction step can be performed) for call-by-need evaluation, even though it contains $\beta$-redexes (but they won't be fired because they are in positions that do not require/allow to evaluate them according to the call-by-need discipline).

Note that for call-by-value evaluation $(\lambda y.x)\omega$ is a diverging term, since call-by-value evaluation has to evaluate the argument $\omega$ first (which is not a value), and $\omega$ is diverging. In particular, call-by-value evaluation cannot reduce $(\lambda y.x)\omega \to_\beta x$ because $\omega$ is not a value.

Summing up: \begin{align} \text{call-by-name:}&&&(\lambda y.x)\omega \to_\beta x \text{ and }x \text{ is normal} \\ \text{call-by-value:}&&&(\lambda y.x)\omega \to_\beta (\lambda y.x)\omega \to_\beta \dots\\ \text{call-by-need:}&&&(\lambda y.x)\omega \text{ is normal.} \end{align}

For an example of needed evaluation in call-by-need, consider the term $(\lambda y.y4)(II)$ where $I = \lambda z.z$ ($I$ represents the identity function). Here the function $\lambda y.y4$ depends on its argument and then the call-by-need (and call-by-value) discipline requires $II$ to be evaluated first. So, according to the call-by-need (and call-by-value) evaluation \begin{align} (\lambda y.y4)(II) &\to_\beta (\lambda y.y4)I \to_\beta I4 \to_\beta 4. \end{align}

Notice that according the call-by-name evaluation, \begin{align} (\lambda y.y4)(II) &\to_\beta II4 \to_\beta I4 \to_\beta 4. \end{align}

Let us consider another term, say $(\lambda x.xx)(II)$, to see the differences between call-by-name, call-by-value and call-by-need. \begin{align} \text{call-by-name:}&&(\lambda x.xx)(II) &\to_\beta (II)(II) \to_\beta I(II) \to_\beta II \to_\beta I \\ \text{call-by-value:}&&(\lambda x.xx)(II) &\to_\beta (\lambda x.xx)I \to_\beta II \to_\beta I \\ \text{call-by-need:}&&(\lambda x.xx)(II) &\to_\beta (\lambda x.xx)I \to_\beta Ix \text{ (where } x \text{ is associated with }I) \\ &&&\to_\beta x \text{ (where } x \text{ is associated with }I) \to_\beta I \end{align} Note that the call-by-value evaluation first evaluates the argument $II$ to the value $I$, then copies the value $I$ to all the occurrences of $x$. On the contrary, the call-by-need evaluation is more cautious: first it uses a thunk (i.e. a helper subroutine) to evaluate the argument $II$ to the value $I$, then it passes the address of this subroutine to the function $\lambda x.xx$ and copies its value $I$ only where is needed to continue the computation (this is the intuitive meaning of $Ix$ where $x$ is associated with $I$); in this way, when the value of the original argument $II$ is required again (in the last step of call-by-need evaluation), its value $I$ is already calculated and available.

Concerning your example $(\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1)$:

  • The call-by-need evaluation of $(\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1)$ is: \begin{align} (\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1) &\to_\text{lift} (\lambda x.(\lambda y.yx)(\lambda z.z+1))(2+2) \to_\beta (\lambda x.(\lambda z.z+1)x)(2+2) \\ &\to_\beta (\lambda x.x+1)(2+2) \to_\beta (\lambda x.x+1)4 \to_\beta 4+1 \to_\beta 5 \end{align} where the first step is the reduction rule called "lift" in Ariola's and Felleisen's paper, and "$C$" in Maraist's, Odersky's and Wadler's paper (see below for references).

  • The call-by-value evaluation of $(\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1)$ is: \begin{align} (\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1) & \to_\beta (\lambda x.\lambda y.yx)4(\lambda z.z+1) \to_\beta (\lambda y.y4)(\lambda z.z+1) \\ &\to_\beta (\lambda z.z+1)4 \to_\beta 4+1 \to_\beta 5. \end{align}

  • The call-by-name evaluation of $(\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1)$ is: \begin{align} (\lambda x.\lambda y.yx)(2+2)(\lambda z.z+1) &\to_\beta (\lambda y.y(2+2))(\lambda z.z+1) \to_\beta (\lambda z.z+1)(2+2) \\ &\to_\beta (2+2)+1 \to_\beta 4+1 \to_\beta 5. \end{align}

Disclaimer: My explanation is quite informal and technically imprecise, but I prefer to give an intuition. Actually, to see in a proper way the differences between call-by-name, call-by-value and call-by-need it is better to use a lambda-calculus with explicit substitutions and/or a linear beta-reduction (which substitutes the argument of a $\beta$-redex for only one occurrence of variable). This is the setting used in the references (which are excellent) given by Luca Bressan in his answer:

2
On

This is not really an answer, but a pointer to the existing literature.

There are at least two versions of call-by-need lambda calculus, which are presented in the following papers:

Ariola Z.M., Felleisen M. (1997) The Call-by-Need Lambda Calculus. J. Funct. Program. 7, 265-301.

Maraist J., Odersky M., Wadler P. (1998) The Call-by-Need Lambda Calculus. J. Funct. Program. 8, 275-317.

An alternative axiomatization which solves some problems of both the previous ones is given in:

Chang S., Felleisen M. (2012) The Call-by-Need Lambda Calculus, Revisited. In: Seidl H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. (Available on arXiv:1201.3907.)

I believe that an answer to your question will depend on the particular axiomatization one chooses to formalize call-by-need evaluation.