1

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?

Daniel
  • 732
  • You can eliminate free variables with beta reduction. Consider $(\lambda x.(\lambda y.y))z$. One place to start is "what is the definition of $\alpha$ equivalence?" – DanielV Aug 28 '17 at 00:59
  • that said, $\alpha$-conversion cannot hold $\beta$-reduction... (I hadn't realized, but now you said, some examples came into my mind). If you want to rewrite your comment as an answer, feel free – Daniel Aug 28 '17 at 02:37
  • 1
    A lambda term is almost never $\alpha$-equivalent to its $\beta$-reduction. The only exceptions are lambda terms without normal forms (though most of those are also not $\alpha$-equivalent to their $\beta$-reductions). – Derek Elkins left SE Aug 28 '17 at 02:56

1 Answers1

0

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

DanielV
  • 23,556