Beta Reduction

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.