Lambda calculus - order of operations - need clarification?

[glaxaco]

In section 3.1.7, you evaluate an expression in two different ways depending on parentheses. In one case the result is λx.x, and in other case the result is λy.y, which is "a completely different result". But aren't both results the identity function, just with different names for the bound variables? I feel like I'm missing something here.

[robconery]

Yeah it's super tricky :). It has to do with the order of reduction - which I should explain more - I'll add some detail in the book but... here goes.

In the first step we resolve this because of parens:

λx.(λy.y x)
λx.(y[y:=x])
λx.x 

x is put through the identity function which resolves to just x. In the later function, however, we need to resolve λx.λy.y first. This is the constant function, which means "any function x will return λy.y. We can do this through reduction or just simple deduction by looking at it.

Does that help?

[glaxaco]

Maybe. Let me try to state it and see if this is right.

The first case resolves to "any function x will return x." The second case resolves to "any function x will return the identity function."

If that's right, so far so good, but I'm still thrown by the notation. In the second case x is both a bound variable and the input; i.e.

(λy.y)[x:=x]

If x is a bound variable, it has no meaning outside of the lambda, right? Then how can you substitute it for an x which is coming in from the outside? Is this due to a closure? Maybe I need to translate it to Javascript and run it through a REPL.

[robconery]

There is a lambda site out there that will run these things - it's kind of a pain to get through but ... yeah it's tough to make it through this. If this helps: solve it from right to left, then left to right and see if that changes your perspective.