3

It seems to be a know fact that if $M$, $N$ are $\lambda$-terms, and $M \twoheadrightarrow_{\beta\eta} N$, then $fv(N) \subseteq fv(M)$.

My problem is: is it true that if $M \twoheadrightarrow_{\beta\eta} N$ then $fv(N) = fv(M)$?

essay
  • 1,135

1 Answers1

2

No. Let $x, y$ and $z$ be three different variables. Take $M = (\lambda x . y) z$. Then $M$ $\beta$-reduces to $y$. Free variables of $M$ are $y$ and $z$, and the only free variable in $y$ is $y$.

Aleš Bizjak
  • 2,691
  • 1
    of course! now I see the mistake in my "proof" - I was assuming that I would actually get the term $N$ inside $M$ after the substituition, which does not have to happen. thank you! – essay Jun 30 '15 at 11:04