# Lambda calculus free and bound variables

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

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

• [] 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. Oct 7, 2016 at 21:35
• @sudee $y$ also has a name conflict. Oct 7, 2016 at 22:15
• They do have the same name but because the inner $y$ is bound by the $\lambda$-abstraction there is no ambiguity. Oct 8, 2016 at 6:08
• Why is $𝑧_2$ bound in $(𝑦_1 (𝜆 𝑧_1 . (𝜆 𝑦_2 . 𝑧_2 𝑦_2) 𝑧_1))$ if there's no $𝜆 𝑧_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. Nov 11, 2021 at 18:40
• @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. Nov 12, 2021 at 1:03