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\}$.

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

1 Answer 1

  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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.