문제

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. 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.

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top