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

• sudee: [] is the standard notation for substitution, which is just a syntactic transformation. In this case there would only be one name conflict, for $z$. To carry out the substitution we need to use $\alpha$-conversion to give $z$ a different name in the right-hand side term, then replace every instance of $x$ in the term on the left.
• DanielV: @sudee $y$ also has a name conflict.
• sudee: They do have the same name but because the inner $y$ is bound by the $\lambda$-abstraction there is no ambiguity.
• joseville: Why is $z_2$ bound in $(y_1 (λ z_1 . (λ y_2 . z_2 y_2) z_1))$ if there's no $λ z_2$ anywhere? I'm using [this other math.se answer ](math.stackexchange.com/a/1559114/833760) as a guide to figure out what's bound and what's free.
• DanielV: @joseville I don't know how I messed that up, just a typo. Sorry for that. z_1 is bound and z_2 is free.