title: Beta reduction in lambda calculus: Order of evaluation important?
body: <p>Given the following lambda expression, where <code>\</code> resembles <code>lambda</code>:</p>
  
  <pre><code>(\kf.f(\c.co)km)(\x.dox)(\le.le)
  </code></pre>
  
  <p>Is it wrong if I convert <code>(\c.co)k</code> into <code>ko</code>? I did that and apparently, it was wrong. The right way to go would have been to evaluate the outer function first, meaning <code>(\f.f(\c.co)(\x.dox)m)(\le.le)</code> would have been the desired solution.</p>
  
  <p>Is that true, because I can't find any rule that could indicate that in our lecture notes? If yes, why can't I evaluate inner functions first? I've done it like this and my solution was correct, nonetheless.</p>
  
  <p>Regards.</p>