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?
Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?
1
-
$\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$– codyJun 28 at 15:13
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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 at 21:24