A confusion on $\beta\eta$-reduction

Question

Recently I've started exploring lambda calculus, and currently I'm tackling the next exercise:

Prove that if $M =_{\beta\eta} N$, then $FV(M) = FV(N)$,

Where $FV(P)$ stands for free variables in the term $P$. Obviously, $\eta$-conversion doesn't affect on the free variables, since $\lambda x.Mx =_\eta M$ exactly when $x \notin FV(M)$, and $FV(\lambda x.Mx) = FV(M)$ when the same condition holds.

But what about $\beta$-reduction? It's obvious, that if $M \to_\beta N$, then $FV(N) \subseteq FV(M)$. It's also known that $\beta$-reduction can eliminate free variables, as said here or here. How then it might be possible that $FV(M) = FV(N)$ for the stated condition? The simple example $(\lambda x.y)z \to_\beta y$, and thus $(\lambda x.y)z =_\beta y$ breaks the statement. Maybe there's a typo in the exercise?

Or maybe I don't quite understand the difference between $\beta$-reduction and $\beta$-equivalence: as far as I understand, if $M \to_\beta N$, then $M =_\beta N$, and the latter, the $\beta$-equivalence, just means (by Church-Rosser) that $\exists L$ such that $M \twoheadrightarrow_\beta L$ and $N \twoheadrightarrow_\beta L$. But this facts, as I suppose, can't help me to resolve the issue.

Seems obvious that there exists such $M$ and $N$, that $M \twoheadrightarrow_\beta N$, but the converse doesn't hold. And still it's said that $M =_\beta N$. Thus $\to_\beta \subset \twoheadrightarrow_\beta \subset =_\beta$ should hold. Then, again, I don't get how the statement in the exercise above holds.

Can anyone give a hint? Thanks in advance!

Answer 1

You basically answered the question yourself. Clearly, the statement is false. More precisely:

• It is true that if $M =_\eta N$ then $FV(M) = FV(N)$, for the reason you wrote in your post.

• It is false that if $M \to_\beta N$ (and so, if $M \twoheadrightarrow_\beta N$, or $M =_\beta N$, or $M =_{\beta\eta} N$) then $FV(M) = FV(N)$, for the reason you wrote in your post.

• It is true that if $M \to_\beta N$ (and more generally, if $M \twoheadrightarrow_\beta N$) then $FV(N) \subseteq FV(M)$; the proof is a straightforward induction on the definition of $M \to_\beta N$.

• If $M =_{\beta} N$ (and so, if $M =_{\beta\eta} N$) then we cannot say much about the relation between $FV(M)$ and $FV(N)$. For instance consider $M = (\lambda x.y)z$ and $N = (\lambda x.y)z'$, with $z \neq z'$: then, $M =_\beta N$ (and so $M =_{\beta\eta} N$) and $FV(M) = \{y,z\} \neq \{y,z'\} = FV(N)$, but $FV(M) \not\subseteq FV(N)$ and $FV(N) \not\subseteq FV(M)$.

There is a restriction of the $\lambda$-calculus where the statement "if $M =_{\beta\eta} N$ then $FV(M) = FV(N)$" becomes true: the $\lambda I$-calculus. This fragment of the $\lambda$-calculus is obtained by adding the constraint that in a term of the form $\lambda x. M$, necessarily $x \in FV(M)$, that is, terms such as $\lambda x.y$ are not allowed. Roughly, this fragment doesn't allow terms where one abstracts over a variable but doesn't use it. This way, the counterexamples to $FV(M) = FV(N)$ are impossible to build in the $\lambda I$-calculus. The $\lambda I$-calculus is interesting because, despite its restrictions, it is still Turing-complete.

---

As an aside comment, note that if a statement of the form "$A$ implies $B$" holds and $A'$ is a particular case of $A$, then the statement "$A'$ implies $B$" holds as well. Dually, if a statement of the form "$A$ implies $B$" fails and $A'$ is a generalization of $A$ (i.e. $A$ implies $A'$), then the statement "$A'$ implies $B$" fails as well.

Concretely, once you established that the statement "if $M \to_\beta N$ then $FV(M) = FV(N)$" is false, it automatically follows that also the statements "if $M \twoheadrightarrow_\beta N$ then $FV(M) = FV(N)$" and "if $M =_\beta N$ then $FV(M) = FV(N)$" and "if $M =_{\beta\eta} N$ then $FV(M) = FV(N)$" are false.