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?