# Free variables of (λx.xy)x and bound variables of λxy.x

I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong.

1. Find free variables of $(\lambda x.xy)x$.
My workings: $FV((\lambda x.xy)x)=FV(\lambda x.xy) \cup FV(x)=\{y\} \cup \{x\}=\{x,y\}$.
The model answer: $FV((\lambda x.xy)x)=\{x\}$.

2. Find bound variables of $\lambda xy.x$.
My workings: A variable $y$ has its binding but since it is not present in the body of the $\lambda$-abstraction it cannot be bound and thus $BV(\lambda xy.x)=\{x\}$ only.
The model answer: $BV(\lambda xy.x)=\{x, y\}$.

• The way to read $\lambda xy.x$ is $\lambda x.\lambda y.x$. Commented Aug 21, 2012 at 18:37

1. Your answer is correct, $y$ is surely free. The model one is wrong. Maybe there was a typo and the answer was meant for $(\lambda y.xy)x$
2. It depends on the precise definition of $BV$. Often only $FV$ is defined formally, because it's more important. (Bound variables can be freely renamed in a subterm, but free variables can't.) So if $BV$ is defined as \begin{eqnarray*} BV(x) &=& \{\} \\ BV(M N) &=& BV(M)\cup BV(N) \\ BV(\lambda x.M) &=& \{x\}\cup BV(M) \\ \end{eqnarray*} then the model answer is correct. Note that this definition makes sense: If you have a term $M$ and substitute for a free variable $x$ another term $N$ with no bound variables ($BV(N)=\{\}$), you expect that $BV(M)=BV(M[x:=N])$. If you'd consider only bound variables that also appear under the $\lambda$, this property wouldn't hold.