Overview
Beta reduction represents the primary way that the lambda calculus represents a computation. It takes a term in the lambda calculus, and reduces (replaces) it with another term. This new term represents one step in a computation.
As an example, in normal math, one may find the following expression.
{% 2+2 %}
When doing a computation, on may replace this expression with the number {% 4 %} which we
write
{% 2+2=4 %}
To recast this in computer science, we replace the operator {% + %} with a function, as such
{% add(2,2) = 4 %}
and we assert, that whenever we see {% add(2,2) %} in a program, we can replace it with {% 4 %}.
This is called function application.
Reduction
Beta-Reduction in the lambda calculus is similar to the function application given above. A function in the lambda calculus is denoted as
{% \lambda x.M %}
Loosely, this can be interpreted as a function with a parameter named {% x %}. The body of the function is given
by the term {% M %}.
Application of the function above is written as
{% (\lambda x.M)N %}
where {% N %} is a term in the lambda calculus.
{% (\lambda x.M)N \rightarrow_{\beta} M\{x \rightarrow N \} %}
Here {% M\{x \rightarrow N \} %} means to substitue {% N %} for {% x %} in {% M %}.
This is referred to as the {% \beta-reduction \, rule %}
Example
As an example, take the function
{% (\lambda x.x) %}
Then apply this function to some lambda term N. This would mean to replace {% x %} by {% N %} in {% x %}, which just
results in {% N %}
{% (\lambda x.x)N = N %}
In particular, applying the function to itself yields
{% (\lambda x.x)\lambda x.x = \lambda x.x %}
This function is the identity function, that is, it just returns whatever is inputted into it.