how to represent free variables within lambda-calculus expression

260 Views Asked by At

Given I have the expression $\lambda x (y(\lambda y(xy)))$, I know that $x$ is a bound variable because of the initial $\lambda x$, but I'm not sure how I could express the $y$ since it is free before the scope of $\lambda y$ and bound within this scope.

In order to represent this free variable, should I try some kind of substitution?

For example, $$\lambda x (y\quad(\;[z/y]\; \lambda y (xy)\;)\quad)$$

$$\lambda x (y\quad(\; \lambda z (xz)\;)\quad)$$

is the right way to do it?