<p>The answer depends on the definition of the substitution you use.</p>
<p>With the standard definition:</p>
<blockquote>
<p><span class="math-container">$(\lambda y.M)[N/x] := \lambda y.M[N/x]$</span> provided <span class="math-container">$x \neq y$</span> and <span class="math-container">$y \not\in \mathrm{FV}(N)$</span></p>
</blockquote>
<p>the reduction of your term <em>does</em> require α-conversion.</p>
<p>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...</p>
<p>If you choose some alternative definition, like adding this rule:</p>
<blockquote>
<p><span class="math-container">$(\lambda x.M)[N/x] := \lambda x.M$</span></p>
</blockquote>
<p>to the previous one, then the β-reduction normalizes in one step without α-conversion.</p>

CC BY-SA 4.0
2023-06-28T21:24:43.127Z
Btw, the downvote would be more helpful if accompanied by a comment!
sparusaurata
CC BY-SA 4.0
2023-06-28T15:23:15.850Z
2023-06-28T15:23:15.850Z
sparusaurata
<p>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?</p>

CC BY-SA 4.0
2023-06-28T15:13:31.830Z
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
<lambda-calculus>
Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?
AdrianGarciaB
# Is it necessary to apply alpha conversion in this term to perform beta reduction in lambda calculus?

(Asked by: username_0 on 2023-06-28)

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?

**Tags:** lambda-calculus
> **Comments:**
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2023-06-28. Score: 0 | Accepted answer

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.

> **Comments:**
> **username_2**: Btw, the downvote would be more helpful if accompanied by a comment!  

---

