Formally, *beta reduction* (also written \(\beta\)-reduction) is the
replacement of a bound variable in a function body with a function
argument. The purpose of \(\beta\)-reduction is to compute the result
of a function by function application using specific rules.

More formally, the beta reduction rule states that a function application
of the form \((\lambda x.t)s\) reduces to the term \(t[x := s]\). The
term \(t[x := s]\) means that all instances of \(x\) in \(t\) are
replaced with \(s\). The \(\rightarrow\) syntax is used as
a shorthand for beta reduction. We can specify beta-reduction explicitly
using the notation \((\lambda x.t)s \rightarrow t[x := s]\), which means
that the beta reduction of \((\lambda x.t)s)\) is \(t[x := s]\). The
beta reduction removes the \(\lambda\) symbol and resolves to the
function’s body with the argument \(s\) substituted into the body.

For example, we can apply beta reduction to the simple identity function.
For every \(s\), \((\lambda x.x)s \rightarrow x[x := s] = s\). This
reduction resolves the function application and results in the function
body being returned. In this case, the function body is the same as the
argument \(s\), for any \(s\).

There isn’t much more to beta reduction than this blog post, yet it serves
as the foundation for applying functions and calculating results.

#### See also