patternModerate
Free variables of (λx.xy)x and bound variables of λxy.x
Viewed 0 times
boundfreevariablesandλxy
Problem
I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong.
-
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\}$.
-
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\}$.
-
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\}$.
-
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\}$.
Solution
-
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$
-
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 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$
-
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.
Context
StackExchange Computer Science Q#3274, answer score: 12
Revisions (0)
No revisions yet.