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?
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 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