title: When to rename variables in lambda calculus?
body: <p>I understand why renaming variables to avoid capture is important but, in the following example, I don't understand why it doesn't occur.</p>
  
  <pre><code>(λf.λx.f(fx))(λf.λx.fx)
  </code></pre>
  
  <p>apparently reduces to</p>
  
  <pre><code>λx.(λf.λx.fx)((λf.λx.fx)x)
  </code></pre>
  
  <p>but shouldn't <code>x</code> be renamed in either <code>(λf.λx.f(fx))</code> or <code>(λf.λx.f(fx))</code>? Don't they refer to different <code>x</code>s?</p>