Untyped Lambda Calculus – Why Call-by-Value is Strict

lambda

I'm currently reading Benjamin C. Pierce's “Types and Programming Languages”. Before really getting into type theory it explains lambda calculus and evaluation strategies.

I am a bit confused by the explanation of call by name vs call by value in this context.

The two strategies are explained in the following manner:

call by name

Like normal order in that it chooses the leftmost, outermost redex first, but more restrictive by not allowing reductions inside abstractions. An example:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

call by value

Only the outermost redexes are reduced and a redex is reduced only when its right-hand side has already been reduced to a value—a term that is finished computing and cannot be reduced any further. An example:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

(identical to the call by name evaluation)

Ok, so far so good. But this is followed by the following paragraph:

The call-by-value strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, non-strict (or lazy) strategies such as call-by-name and call-by-need evaluate only the arguments that are actually used.

I know what call-by-value and call-by-name means practically, from having used (among others) C and Haskell, but I cannot see why the evaluation strategy explained above leads to this in the lambda calculus. Is this an additional rule that always accompany call-by-value, or does if follow from the reduction strategy outlined above?

Especially since the reduction steps in the examples are identical, I fail to see the difference between the two strategies and would love if someone could help me gain some intuition.

Best Answer

Yes, the evaluation strategy as described leads to strict semantics, and the examples are spectacularly badly chosen to conceal the difference between the two semantics. I think it goes something like this:

id (id (λz. id z))  # strict means we evaluate the right hand side
→ id (λz. id z)     # RHS has been reduced (id (λz. id z)) → (λz. id z) by inner id 
→ λz. id z          # now we have called the outer id to obtain the final value

id (id (λz. id z))  # normal form means we call the outer id and pass RHS as a closure
→ id (λz. id z)     # outer id just returned its argument unevaluated → id (λz. id z) 
→ λz. id z          # now same thing is repeated with inner id

So the derivation steps look syntactically the same, but different things are happening. Under the lazy evaluation scheme, id doesn't actually force evaluation of its argument: it simply returns that argument itself. So not only do id x and x yield the same value, but they are actually equivalent: id x really yields x itself, and then x yields its value later when actually needed. So likewise, id (id (λz. id z)) simply yields the unevaluated right hand side (id (λz. id z)).

What's confusing in the example is that it's based on nesting the same function, which is just id, such that two different reductions both yield id (λz. id z). In one this is just a copy of the inner id expression, and in the other, it's the value of the inner expression, being passed an argument to the outer id.

Related Solutions

Python Lambda – Is It Truly Formal Lambda Calculus or Just a Namesake?

Python lambda expressions are real, formal untyped λ-calculus lambda expressions.

They fit the formal definition; they can only represent one python expression, based on variables (free or otherwise) and references to other functions (abstract symbols). Python uses parenthesis in expressions too.

You use them wherever a lambda is more suitable and convenient than a full function definition. The python def functionname(argumentlist): syntax forms a statement; in Python you cannot put statements inside of expressions, only the other way around. A lambda on the other hand, is an expression, so you can use a lambda to insert a callback function inline:

map(lambda x, y: x[y+5], [(mapping1, integerkey1), (mapping2, integerkey2)])

The above example consists only of an expression. The python map() function takes, as its first argument, a callable, which is applied to each and every element in the list given by the second argument. In the above example, using a lambda expression to define that callable is much easier than using a function statement:

def mapcallback(x, y):
    return x[y + 5]

map(mapcallback, [(mapping1, integerkey1), (mapping2, integerkey2)])

For the full function syntax I need to assign a name, put the function definition on separate lines, and use the return statement to return the result of the expression.

Programming Languages – Are Normal Order and Call-by-Name the Same?

Normal order evaluation and call-by-name evaluation are not quite the same thing. In normal order evaluation, the outermost function is evaluated before any of its arguments, and those arguments are evaluated only if needed. In call-by-name evaluation, the arguments are effectively copied into the body of the outermost function and then that function is evaluated. In both cases, the outermost function is technically evaluated before the arguments, but in pure call-by-name, the arguments are evaluated each time they are used (either zero, one, or many times). In normal order, the function arguments are evaluated at the very least only when first needed (typically zero or one times).

Thus normal order evaluation leaves open the possibility of memoizing the arguments as an optimization (sometimes called call-by-need), while call-by-name does not. Thus one could say that call-by-name evaluation is a special case of normal order evaluation. In other words, normal order evaluation refers to the general approach of evaluating a function before its arguments, while call-by-name evaluation refers to a specific technique for implementing normal order evaluation.

As an example, given f(x, y) = sqrt(x*x + y*y) we could have two ways of implementing f(a+b, c+d) with normal order evaluation:

Memoized:

t1 = a+b;
t2 = c+d;
return sqrt(t1*t1 + t2*t2);

Call-by-name:

return sqrt((a+b)*(a+b) + (c+d)*(c+d));

As you can see, if the call to f included other function calls (i.e. f(random(1,100), ask_user_for_value()) ), the two will have very different behavior. The memoized version will square a single random number and ask the user for a value only once, while the call-by-name version will multiply two random numbers and ask the user for a value twice.

To learn more about these concepts, I recommend reading the evaluation strategy Wikipedia page, and https://cs.stackexchange.com/questions/7702/applicative-order-and-normal-order-in-lambda-calculus.