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
⇒ 15It 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?