# Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?

I am trying to prove that the expression ((λx.(λx.x))(ab)) does not require alpha conversion for beta reduction since there is no variable overlap, but how could I demonstrate this more formally?

• Proving that every $\alpha$-equivalent term ($\beta$) reduces to an $\alpha$-equivalent term should do the trick! It's a strange thing to prove though, unless this is homework.
– cody
Jun 28, 2023 at 15:13

The answer depends on the definition of the substitution you use.

With the standard definition:

$$(\lambda y.M)[N/x] := \lambda y.M[N/x]$$ provided $$x \neq y$$ and $$y \not\in \mathrm{FV}(N)$$

the reduction of your term does require α-conversion.

Similarly, if you choose the Barendregt variable convention (see 2.1.13 in the book), you aren't even allowed to write your term like you do — which seems a hygienic prohibition to me...

If you choose some alternative definition, like adding this rule:

$$(\lambda x.M)[N/x] := \lambda x.M$$

to the previous one, then the β-reduction normalizes in one step without α-conversion.

• Btw, the downvote would be more helpful if accompanied by a comment! Jun 28, 2023 at 21:24