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?

  • $\begingroup$ 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?" $\endgroup$ – DanielV Aug 28 '17 at 0:59
  • $\begingroup$ 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 $\endgroup$ – Daniel Aug 28 '17 at 2:37
  • 1
    $\begingroup$ 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). $\endgroup$ – Derek Elkins Aug 28 '17 at 2:56

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.