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?
$$(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
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)$$