In all the situations above, the beta-reduction was trigerred in the context of a sub-expression of the form</p>
<p><code>((fn [x] a) b)</code> where <code>a</code> and <code>b</code> are arbitrary expressions. Such a sub-expression is called a reducible expression or <em>redex</em>.</p>
<p>The beta reduction says that such a redex can be rewritten as expression <code>a</code> in which all the (free) occurrences of <code>x</code> are replaced by <code>b</code>.</p>
<p>This looks like a simple rule but it is