[Solved]: Free variables of (λx.xy)x and bound variables of λxy.x

Problem Detail: 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}$.
Asked By : Dávid Tóth

Answered By : Petr Pudlák

  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.
Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/3274  Ask a Question  Download Related Notes/Documents

Leave a Reply