Beta Reduction

lambda-calculus

Definition

Beta Reduction

The beta reduction relation is defined as the least congruence relation on expressions $e$ such that:

$$(\lambda x.e_1)e_2\to [e_2/x]e_1$$

where $[t/x]$ means substituting the term $t$ for each free occurrence of $x$ in $e$. If there are free variables in $e_2$ then bound variables in $e_2$ must be renamed so that substitution does not result in the free variables in $e_2$ becoming bound. This process of renaming bound variables is called alpha reduction.

Examples

Example: Identity

$$(\lambda x.x)y\stackrel{\beta }{\to }[y/x]x\stackrel{\beta }{\to }y$$

Example: Constant

$$\begin{array}{rl}(\lambda x.\lambda y.x)ab& \stackrel{\beta }{\to }((\lambda x.\lambda y.x)a)b\\ & \stackrel{\beta }{\to }(\lambda y.a)b\\ & \stackrel{\beta }{\to }a\end{array}$$

Example: Avoiding Variable Capture

Naively, one would substitute $x$ with $y$, however, there’s already a bound variable $y$. Thus, an alpha reduction must be performed:

$$\begin{array}{rl}(\lambda x.\lambda y.xy)y& \stackrel{\alpha ,\lambda y\to \lambda z}{\to }(\lambda x.\lambda z.xz)y\\ & \stackrel{\beta }{\to }\lambda z.yz\end{array}$$

Example: Nested Application

$$\begin{array}{rl}(\lambda f.\lambda x.f(fx))\underset{\mathbf{I}}{\underbrace{[\lambda y.y]}}z& \stackrel{\alpha }{\to }(\lambda f.\lambda x.f(fx))\mathbf{I}z\\ & \stackrel{\beta }{\to }(\lambda x.\mathbf{I}(\mathbf{I}x))z\\ & \stackrel{\beta }{\to }\mathbf{I}(\mathbf{I}z)\\ & \stackrel{\beta }{\to }\mathbf{I}z\\ & \stackrel{\beta }{\to }z\end{array}$$

Example: More Involved Application

$$\begin{array}{rl}(\lambda a.\lambda b.ba)(\lambda x.x)(\lambda y.z)& \stackrel{\alpha }{\to }(\lambda a.\lambda b.ba)\mathbf{I}(\lambda y.z)\\ & \stackrel{\beta }{\to }(\lambda b.b\mathbf{I})(\lambda y.z)\\ & \stackrel{\beta }{\to }(\lambda y.z)\mathbf{I}\\ & \stackrel{\beta }{\to }\mathbf{I}z\\ & \stackrel{\beta }{\to }z\end{array}$$

Example: Y Combinator Step

$$\begin{array}{rl}\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))& \stackrel{\beta }{\to }\lambda f.(\lambda x.f((\lambda x.f(xx))(\lambda x.f(xx))))\end{array}$$