3.6.1. Beta-Redexes¶

Now that we have rigorously defined substitution in the previous section, we can define a rule for evaluating a function application, which is the main operation for any $\lambda$ calculus interpreter. This rule is called $\beta$-reduction. An expression to which the rule can be applied is called a $\beta$-redex (short for $\beta$-reduction expression). So, a $\beta$-redex is formally defined as a $\lambda$ expression of a specific form, namely, an application in which the first term is a function abstraction.

For example, $(\lambda x.(x \; v) \;\; (z \; (v \; u)))$ is a $\beta$-redex because $\lambda x.(x \; v)$ is a function abstraction. On the other hand, $((\lambda x.(x \; v) \;\; y) \;\; (z \; (v \; u)))$ is not because its first term is a function application and not a function abstraction. However, the application that comprises the first term of this expression is a $\beta$-redex. This illustrates that it is possible for expressions that may not themselves be $\beta$-redexes to contain sub-expressions that are.

A critical part of analyzing how any language evaluates function calls is to examine its semantics from the perspective of $\beta$-reduction.

3.6.2. Identifying Beta-Redexes¶

The following randomized problem will help you identify $\beta$-redexes. To earn credit for it, you will have to solve it correctly three times in a row.

3.6.3. Beta-Reduction is a Substitution¶

If we have a $\beta$-redex of the form $(\lambda x.E \;\; E')$, then to $\beta$-reduce this expression means to substitute $E'$ for $x$ in $E$ using the substitution algorithm developed in the preceding section.

In other words, to evaluate a $\beta$-redex of the form

simply means to perform the following substitution:

Again, this is just the algorithm that you learned in Substitution Algorithm. Note that the result of a $\beta$-reduction is what you get by first stripping off the binding occurrence of the $\lambda$-abstraction, leaving just its body, and then substituting $E'$ for x in that body.

For example, to $\beta$-reduce $(\lambda x.(x \; v) \;\; (z \; (v \; u)))$, you would first strip off $\lambda x.$ to get $(x \; v)$ (that is, the body of the $\lambda$-abstraction), and then substitute $(z \; (v \; u))$ for $x$ in that body, yielding the expression $((z \;\; (v \;\; u)) \;\; v)$.

3.6.4. Some Beta-Reductions Require Alpha-Conversion¶

The following randomized problem will help you identify $\beta$-redexes and prepare to reduce them by determining whether an $\alpha$-conversion is needed. To earn credit for it, you will have to solve it correctly three times in a row.

3.6.5. Performing Beta-Reductions¶

The following randomized problem will provide practice performing $\beta$-reductions. To earn credit for it, you will have to solve it correctly three times in a row. Be Careful: remember that, because $\beta$-reducing uses the substitution algorithm, it may be necessary to perform an $\alpha$-conversion. For example, $\beta$-reducing $(\lambda x. \lambda u.(u \;\; x) \;\; (v \;\; u))$ yields $\lambda a.(a \;\; (v \;\; u))$, where we must do an $\alpha$-conversion to avoid capturing the free variable $u$.