How do scoping rules work in the Lambda Calculus with nested functions

Question

Let's say I have a lambda expression like this:

$$(\lambda a . (ab))(c)$$

It reduces to

$$cb$$

But let's say I have a nested function

$$(\lambda a . (\lambda x.(ax)))(b)$$

Does this reduce to

$$\lambda x.(bx)$$

or to

$$\lambda x.(ax)$$

In other words, does the lambda calculus use lexical scoping?

Also, if lexical scoping is used, what happens if the bound variable uses the same name within and without the function body? In other words, how does this get reduced?

$$(\lambda x.(x\lambda x.x))a$$

Does it reduce to

$$a\lambda x.x$$

or

$$a\lambda a.a$$

Answer 1

Everything works as it should if this were about a pure functional programming language. Yes, it is lexical scoping.

$(\lambda x.(x\lambda x.x))a = a\lambda x.x$.

Basically, $\lambda x.x = \lambda y.y$. You are defining operations as you would expect in a programming language. So you do have to be careful about cases like $\lambda x.(x\lambda x.x)$.

So $\lambda a . (\lambda x.(ax))$ is an operation which, given applied to $b$, returns $\lambda x.(bx)$.

The worst case is something like this:

$$(\lambda a.\lambda x.(ax))x$$

A naive approach would yield $\lambda x.(xx)$. The rigorous definition to deal with this is a bit nightmarish. The Wikipedia page for $\lambda$-calculus has this fairly opaque language:

The freshness condition (requiring that y is not in the free variables of r) is crucial in order to ensure that substitution does not change the meaning of functions. ... In general, failure to meet the freshness condition can be remedied by alpha-renaming with a suitable fresh variable.

Basically, we have to be careful when apply $\lambda x.E$ to an expression with a free $x$ variable in it.