is a lambda-term alpha-equivalent to its beta-reduction?

246 Views Asked by At

Let $M$ be a $\lambda$-term and $M'$ its $\beta$-reduction (any of them, including the $\beta$-normal form).

I'd like to know if

$$ M \equiv_{\alpha} M'$$

What I thought is:

After some $\beta$-reductions, some of the bound-variables of $M$ may disappear, but (I guess) the set $FV(M)$ of free-variables from $M$ wouldn't change, and one of the requiriments for $M$ to be $\alpha$-equivalent to $M'$ is that $FV(M) = FV(M')$.

One the other hand, if $M = ((\lambda x.xy)z)$, then $FV(M) = \{y, z\}$. Taking $M$ to its $\beta$-reduction, we apply a substitution $M' = [z/x](xy) = zy$, and $FV(M') = \{y, z\}$.

That said, I believe that $\beta$-reduction holds the $\alpha$-conversion. Am I right? Is $M$ always $\alpha$-equivalent to its $\beta$-reduction?

1

There are 1 best solutions below

0
On BEST ANSWER

Hint: consider $(\lambda x.(\lambda y.y))z$