Lambda calculus - evaluating these lazy parameters

Question

I'm reading about lambda calculus. From the end of section 2.1 here http://www.toves.org/books/lambda/:

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1   ⇒   (λx.λy.x × y) 3 ((λz.x + z) 2)   where x = 1
⇒   (λy.x × y) ((λz.x + z) 2)   where x = 3
⇒   x × y   where x = 3 and y = (λz.x + z) 2
⇒   x × y   where x = 3 and y = x + z and z = 2
⇒   x × y   where x = 3 and y = 5 and z = 2
⇒   15

It says

In fact, though, y should attain the value 3 rather than 5 since the first beta-reduction should plug 1 into x's spot in the expression. For this reason, a lazy parameter must preserve the current variable context with each reduction, remembering in this case that x = 3 within the expression λy.x × y but maintaining the fact that x = 1 outside the expression.

But I'm confused over the order of operations during the beta reduction. There explanation is, unfortunately, ambiguous. They could mean x should be 1 inside the (λx.λy.x × y) and then y = 3 because that's the next parameter to be passed in, and x is already set (feels wrong), or that we go my route below:

Do we agree that (λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1
is the same as (λx.(λt.λy.t × y) 3 ((λz.x + z) 2)) 1

x is a bound here? Shouldn't it be 1?

That means when we reduce this: (λt.λy.t × y) 3 ((λz.1 + z) 2)) x = 1 (λy.3 × y) ((λz.1 + z) 2)) x = 1, t = 3 3 × ((λz.1 + z) 2)) x = 1, t = 3, y = ((λz.1 + z) 2)) 3 × ((λz.1 + z) 2)) x = 1, t = 3, y = ((λz.1 + z) 2)), z = 2 3 × (1 + 2) x = 1, t = 3, y = ((λz.1 + z) 2)), z = 2 3 x 3 = 9

Is that correct? Or did I reduce it incorrectly?

Margaret Bloom Margaret Bloom · Accepted Answer · 2016-08-21T09:24:14

In the expression

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1

which you correctly rewrote as

(λx.(λt.λy.t × y) 3 ((λz.x + z) 2)) 1

the x variable is bond to the outer lambda abstraction λx.
In fact there is no possibility that the reduction of the term (λx.λy.x × y) 3 could change the term (λz.x + z) since it is in another branch of the redex tree.

The book states it clearly that 15 is the wrong outcome

The example given is a counterexample of what would happen if a Lazy evaluation had be implemented naively.

Lazy evaluation is theoretically achieved by normal order, but that is just a theoretical construction with some practical drawback.
As such, strategies like call-by-need are used instead.

The book only wanted to show a possible, abstract, implementation of said evaluation strategy.

For reference, here a complete reduction using normal order of the expression.

(\x.(\x.\y.x * y) 3 ((\z.x + z) 2)) 1


          ()
         /  \
       \x    1
        | 
       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      x z
  *
 x y



---------------------------------------

(\x.\y.x * y) 3 ((\z.1 + z) 2)


       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      1 z
  *
 x y


---------------------------------------


\y.3 * y ((\z.1 + z) 2)


       ()
      /   \
    .'     ()
   /      /  \
 \y      \z   2
  |       |
  *       +
 3 y     1 z

---------------------------------------


3 * ((\z.1 + z) 2)


     *
   /  \
  3   ()
     /  \
    \z   2
     |
     +
    1 z


---------------------------------------


3 * (1 + 2)


     *
   /  \
  3   1 + 2

---------------------------------------

3 * 3

  *
 / \
3   3

---------------------------------------

9

Lambda calculus - evaluating these lazy parameters

2 Answers

The book states it clearly that 15 is the wrong outcome