Lambda Calculus Free Variable

Question

Here's something from Slonneger's "Syntax and Semantics of Programming Languages":

A variable may occur both bound and free in the same lambda expression: for example, in λx.yλy.yx the first occurrence of y is free and the other two are bound.

I assume the free variable is the y right after the λx. and the bound y's are the λy.y which I can sort of intuitively grasp. So ((λx.yλy.yx)a)b) would reduce to (yλy.ya)b) then to bba ? Can someone explain how this came to be? In the end it's the expression b twice. Can someone perhaps provide more examples of bound and free variables?

Answer 1

You correctly identified the first y as the free variable. Basically lambda abstractions define a scope for their bound variables. The scope overrides any other uses of the same variable names, so the same variable name can be used several times in different abstractions or as free variable.

(y(λy.ya))b can not be reduced any further. Unbound variables will never be substituted in a beta reduction.

If it was (y(λy.ya)b) you could reduce to y(ba).