Lambda calculus free and bound variables

Question

Currently I am trying to use substitution in Lamdba Calculus but I haven't cleared up free and bound variables quite like I thought I had. For example, I have the following expression:

λx.xy where y is a free variable and x is a bound variable.

I'm unsure whether x is only bound because of λx. E.g if the expression was λx.yx, would the y be bound and the x be free? or would the x still be bound because of λx?

Here is the actual question I am trying to tackle:

(y(λz.xz)) [x := λy.zy] 

I believe that y is a free variable and within the λ-expression, z is bound and x is free. Is this correct?

Answer 1

$$(y~(\lambda ~z~.~x~z))[~x := \lambda~ y~.~z~y~]$$

That expression has a lot of variable name conflicts:

$$(y_1~(\lambda ~z_1~.~x_1~z_1))[~x_1 := \lambda~ y_2~.~z_2~y_2~]$$

which transforms to:

$$(y_1~(\lambda ~z_1~.~(\lambda~ y_2~.~z_2~y_2)~z_1))$$

Here

• $y_1$ is a free variable
• $y_2$ is a bound variable
• $z_1$ is a bound variable
• $z_2$ is a free variable

The initial expression isn't actually a valid lambda expression because of the [], so whether $x_1$ is a free or bound variable is ambiguous, since it isn't actually part of the expression. If the [] is meant to represent a beta transform, then $x_1$ was a bound variable in the expression:

$$(\lambda x_1~.~y_1~(\lambda ~z_1~.~x_1~z_1))(\lambda~ y_2~.~z_2~y_2)$$