Question

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

Was it helpful?

Solution

  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.

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top