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?

  • $\begingroup$ 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. $\endgroup$
    – cody
    Jun 28, 2023 at 15:13

1 Answer 1


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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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