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.